# IsarMathLib

## A library of formalized mathematics for Isabelle/ZF theorem proving environment

theory DirectProduct_ZF imports func_ZF
begin

This theory considers the direct product of binary operations. Contributed by Seo Sanghyeon.

### Definition

In group theory the notion of direct product provides a natural way of creating a new group from two given groups.

Given $$(G,\cdot)$$ and $$(H,\circ)$$ a new operation $$(G\times H, \times )$$ is defined as $$(g, h) \times (g', h') = (g \cdot g', h \circ h')$$.

Definition

$$\text{DirectProduct}(P,Q,G,H) \equiv$$ $$\{\langle x,\langle P\langle \text{fst}(\text{fst}(x)),\text{fst}(\text{snd}(x))\rangle , Q\langle \text{snd}(\text{fst}(x)),\text{snd}(\text{snd}(x))\rangle \rangle \rangle .\$$ $$x \in (G\times H)\times (G\times H)\}$$

We define a context called direct0 which holds an assumption that $$P, Q$$ are binary operations on $$G,H$$, resp. and denotes $$R$$ as the direct product of $$(G,P)$$ and $$(H,Q)$$.

Locale direct0

assumes Pfun: $$P : G\times G\rightarrow G$$

assumes Qfun: $$Q : H\times H\rightarrow H$$

defines $$R \equiv \text{DirectProduct}(P,Q,G,H)$$

The direct product of binary operations is a binary operation.

lemma (in direct0) DirectProduct_ZF_1_L1:

shows $$R : (G\times H)\times (G\times H)\rightarrow G\times H$$proof
from Pfun, Qfun have $$\forall x\in (G\times H)\times (G\times H).\$$ $$\langle P\langle \text{fst}(\text{fst}(x)),\text{fst}(\text{snd}(x))\rangle ,Q\langle \text{snd}(\text{fst}(x)),\text{snd}(\text{snd}(x))\rangle \rangle \in G\times H$$
then show $$thesis$$ using ZF_fun_from_total , DirectProduct_def
qed

And it has the intended value.

lemma (in direct0) DirectProduct_ZF_1_L2:

shows $$\forall x\in (G\times H).\ \forall y\in (G\times H).\$$ $$R\langle x,y\rangle = \langle P\langle \text{fst}(x),\text{fst}(y)\rangle ,Q\langle \text{snd}(x),\text{snd}(y)\rangle \rangle$$ using DirectProduct_def , DirectProduct_ZF_1_L1 , ZF_fun_from_tot_val

And the value belongs to the set the operation is defined on.

lemma (in direct0) DirectProduct_ZF_1_L3:

shows $$\forall x\in (G\times H).\ \forall y\in (G\times H).\ R\langle x,y\rangle \in G\times H$$ using DirectProduct_ZF_1_L1

### Associative and commutative operations

If P and Q are both associative or commutative operations, the direct product of P and Q has the same property.

Direct product of commutative operations is commutative.

lemma (in direct0) DirectProduct_ZF_2_L1:

assumes $$P \text{ is commutative on } G$$ and $$Q \text{ is commutative on } H$$

shows $$R \text{ is commutative on } G\times H$$proof
from assms have $$\forall x\in (G\times H).\ \forall y\in (G\times H).\ R\langle x,y\rangle = R\langle y,x\rangle$$ using DirectProduct_ZF_1_L2 , IsCommutative_def
then show $$thesis$$ using IsCommutative_def
qed

Direct product of associative operations is associative.

lemma (in direct0) DirectProduct_ZF_2_L2:

assumes $$P \text{ is associative on } G$$ and $$Q \text{ is associative on } H$$

shows $$R \text{ is associative on } G\times H$$proof
have $$\forall x\in G\times H.\ \forall y\in G\times H.\ \forall z\in G\times H.\ R\langle R\langle x,y\rangle ,z\rangle =$$ $$\langle P\langle P\langle \text{fst}(x),\text{fst}(y)\rangle ,\text{fst}(z)\rangle ,Q\langle Q\langle \text{snd}(x),\text{snd}(y)\rangle ,\text{snd}(z)\rangle \rangle$$ using DirectProduct_ZF_1_L2 , DirectProduct_ZF_1_L3
moreover
have $$\forall x\in G\times H.\ \forall y\in G\times H.\ \forall z\in G\times H.\ R\langle x,R\langle y,z\rangle \rangle =$$ $$\langle P\langle \text{fst}(x),P\langle \text{fst}(y),\text{fst}(z)\rangle \rangle ,Q\langle \text{snd}(x),Q\langle \text{snd}(y),\text{snd}(z)\rangle \rangle \rangle$$ using DirectProduct_ZF_1_L2 , DirectProduct_ZF_1_L3
ultimately have $$\forall x\in G\times H.\ \forall y\in G\times H.\ \forall z\in G\times H.\ R\langle R\langle x,y\rangle ,z\rangle = R\langle x,R\langle y,z\rangle \rangle$$ using assms , IsAssociative_def
then show $$thesis$$ using DirectProduct_ZF_1_L1 , IsAssociative_def
qed
end
lemma ZF_fun_from_total:

assumes $$\forall x\in X.\ b(x) \in Y$$

shows $$\{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y$$
Definition of DirectProduct: $$\text{DirectProduct}(P,Q,G,H) \equiv$$ $$\{\langle x,\langle P\langle \text{fst}(\text{fst}(x)),\text{fst}(\text{snd}(x))\rangle , Q\langle \text{snd}(\text{fst}(x)),\text{snd}(\text{snd}(x))\rangle \rangle \rangle .\$$ $$x \in (G\times H)\times (G\times H)\}$$
lemma (in direct0) DirectProduct_ZF_1_L1: shows $$R : (G\times H)\times (G\times H)\rightarrow G\times H$$
lemma ZF_fun_from_tot_val:

assumes $$f:X\rightarrow Y$$, $$x\in X$$ and $$f = \{\langle x,b(x)\rangle .\ x\in X\}$$

shows $$f(x) = b(x)$$
lemma (in direct0) DirectProduct_ZF_1_L2: shows $$\forall x\in (G\times H).\ \forall y\in (G\times H).\$$ $$R\langle x,y\rangle = \langle P\langle \text{fst}(x),\text{fst}(y)\rangle ,Q\langle \text{snd}(x),\text{snd}(y)\rangle \rangle$$
Definition of IsCommutative: $$f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle$$
lemma (in direct0) DirectProduct_ZF_1_L3: shows $$\forall x\in (G\times H).\ \forall y\in (G\times H).\ R\langle x,y\rangle \in G\times H$$
Definition of IsAssociative: $$P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge$$ $$(\forall x \in G.\ \forall y \in G.\ \forall z \in G.\$$ $$( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle )))$$
8
16
3
3