''theory'' Group_ZF ''imports'' [[Monoid_ZF]]
''begin
''
This theory file covers basics of group theory.
!Definition and basic properties of groups
In this section we define the notion of a group and set up the notation for discussing groups. We prove some basic theorems about groups.
To define a group we take a monoid and add a requirement that the right inverse needs to exist for every element of the group.
''Definition
'' $ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$
We define the group inverse as the set $\{\langle x,y \rangle \in G\times G: x\cdot y = e \}$, where $e$ is the neutral element of the group. This set (which can be written as $(\cdot)^{-1}\{ e\}$) is a certain relation on the group (carrier). Since, as we show later, for every $x\in G$ there is exactly one $y\in G$ such that $x \cdot y = e$ this relation is in fact a function from $G$ to $G$.
''Definition
'' $ GroupInv(G,f) \equiv \{\langle x,y\rangle \in G\times G.\ f\langle x,y\rangle = TheNeutralElement(G,f)\}$
We will use the miltiplicative notation for groups. The neutral element is denoted $1$.
''Locale '' group0
''fixes '' $ G$
''fixes '' $ P$
''assumes '' groupAssum: $ \text{IsAgroup}(G,P)$
''fixes '' $ neut$
''defines '' $ 1 \equiv TheNeutralElement(G,P)$
''fixes '' $ groper$
''defines '' $ a \cdot b \equiv P\langle a,b\rangle $
''fixes '' $ inv$
''defines '' $ x^{-1} \equiv GroupInv(G,P)(x)$
First we show a lemma that says that we can use theorems proven in the //monoid0// context (locale).
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L1</nowiki>:
'' shows '' $ monoid0(G,P)$ ''using '' <nowiki>groupAssum</nowiki> , +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$=== , <nowiki>monoid0_def</nowiki>
In some strange cases Isabelle has difficulties with applying the definition of a group. The next lemma defines a rule to be applied in such cases.
''lemma'' <nowiki>definition_of_group</nowiki>:
'' assumes '' $ \text{IsAmonoid}(G,f)$ ''and '' $ \forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)$ '' shows '' $ \text{IsAgroup}(G,f)$ ''using '' <nowiki>assms</nowiki> , +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$===
A technical lemma that allows to use $1$ as the neutral element of the group without referencing a list of lemmas and definitions.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>:
'' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ''using '' +++^[group0_2_L1 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L1</nowiki>: '' shows '' $ monoid0(G,P)$ === , +++^[unit_is_neutral | Monoid_ZF ]... ''lemma'' ''(in '' monoid0 '') '' <nowiki>unit_is_neutral</nowiki>: ''assumes '' $ e = TheNeutralElement(G,f)$ '' shows '' $ e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g)$ ===
The group is closed under the group operation. Used all the time, useful to have handy.
''lemma'' ''(in '' group0 '') '' <nowiki>group_op_closed</nowiki>:
'' assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\cdot b \in G$ ''using '' <nowiki>assms</nowiki> , +++^[group0_2_L1 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L1</nowiki>: '' shows '' $ monoid0(G,P)$ === , +++^[group0_1_L1 | Monoid_ZF ]... ''lemma'' ''(in '' monoid0 '') '' <nowiki>group0_1_L1</nowiki>: ''assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\oplus b \in G$ ===
The group operation is associative. This is another technical lemma that allows to shorten the list of referenced lemmas in some proofs.
''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>:
'' assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ''using '' <nowiki>groupAssum</nowiki> , <nowiki>assms</nowiki> , +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$=== , +++^[IsAmonoid_def | Monoid_ZF ]... Definition of <nowiki>IsAmonoid</nowiki>:
$ \text{IsAmonoid}(G,f) \equiv $
$ f \text{ is associative on } G \wedge $
$ (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g))))$=== , +++^[IsAssociative_def | func_ZF ]... Definition of <nowiki>IsAssociative</nowiki>:
$ P \text{ is associative on } G \equiv P \in 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 )))$=== , +++^[group_op_closed | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_op_closed</nowiki>: ''assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\cdot b \in G$ ===
The group operation maps $G\times G$ into $G$. It is conveniet to have this fact easily accessible in the //group0// context.
''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assocA</nowiki>:
'' shows '' $ P : G\times G\rightarrow G$ ''using '' <nowiki>groupAssum</nowiki> , +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$=== , +++^[IsAmonoid_def | Monoid_ZF ]... Definition of <nowiki>IsAmonoid</nowiki>:
$ \text{IsAmonoid}(G,f) \equiv $
$ f \text{ is associative on } G \wedge $
$ (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g))))$=== , +++^[IsAssociative_def | func_ZF ]... Definition of <nowiki>IsAssociative</nowiki>:
$ P \text{ is associative on } G \equiv P \in 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 )))$===
The definition of a group requires the existence of the right inverse. We show that this is also the left inverse.
''theorem'' ''(in '' group0 '') '' <nowiki>group0_2_T1</nowiki>:
'' assumes '' A1: $ g\in G$ ''and '' A2: $ b\in G$ ''and '' A3: $ g\cdot b = 1 $ '' shows '' $ b\cdot g = 1 $+++[proof ]>
''from '' A2, groupAssum ''obtain '' $ c$ ''where '' I: $ c \in G \wedge b\cdot c = 1 $ ''using '' +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$===
''then '' ''have'' $ c\in G$
''have'' $ 1 \in G$ ''using '' +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''with '' A1, A2, I ''have'' $ b\cdot g = b\cdot (g\cdot (b\cdot c))$ ''using '' +++^[group_op_closed | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_op_closed</nowiki>: ''assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\cdot b \in G$ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ === , +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''also'' ''from '' A1, A2, $ c\in G$ ''have'' $ b\cdot (g\cdot (b\cdot c)) = b\cdot (g\cdot b\cdot c)$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''also'' ''from '' A3, A2, I ''have'' $ b\cdot (g\cdot b\cdot c)= 1 $ ''using '' +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''finally '' ''show'' $ b\cdot g = 1 $
''qed'' ===
For every element of a group there is only one inverse.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L4</nowiki>:
'' assumes '' A1: $ x\in G$ '' shows '' $ \exists !y.\ y\in G \wedge x\cdot y = 1 $+++[proof ]>
''from '' A1, groupAssum ''show'' $ \exists y.\ y\in G \wedge x\cdot y = 1 $ ''using '' +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$===
''fix '' $ y$ $ n$
''assume '' A2: $ y\in G \wedge x\cdot y = 1 $ ''and '' A3: $ n\in G \wedge x\cdot n = 1 $
''show'' $ y=n$+++[proof ]>
''from '' A1, A2 ''have'' T1: $ y\cdot x = 1 $ ''using '' +++^[group0_2_T1 | Group_ZF ]... ''theorem'' ''(in '' group0 '') '' <nowiki>group0_2_T1</nowiki>: ''assumes '' $ g\in G$ ''and'' $ b\in G$ ''and'' $ g\cdot b = 1 $ '' shows '' $ b\cdot g = 1 $ ===
''from '' A2, A3 ''have'' $ y = y\cdot (x\cdot n)$ ''using '' +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''also'' ''from '' A1, A2, A3 ''have'' $ \ldots = (y\cdot x)\cdot n$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''also'' ''from '' T1, A3 ''have'' $ \ldots = n$ ''using '' +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''finally '' ''show'' $ y=n$
''qed'' ===
''qed'' ===
The group inverse is a function that maps G into G.
''theorem'' <nowiki>group0_2_T2</nowiki>:
'' assumes '' A1: $ \text{IsAgroup}(G,f)$ '' shows '' $ GroupInv(G,f) : G\rightarrow G$+++[proof ]>
''have'' $ GroupInv(G,f) \subseteq G\times G$ ''using '' +++^[GroupInv_def | Group_ZF ]... Definition of <nowiki>GroupInv</nowiki>:
$ GroupInv(G,f) \equiv \{\langle x,y\rangle \in G\times G.\ f\langle x,y\rangle = TheNeutralElement(G,f)\}$===
''moreover'' ''from '' A1 ''have'' $ \forall x\in G.\ \exists !y.\ y\in G \wedge \langle x,y\rangle \in GroupInv(G,f)$ ''using '' <nowiki>group0_def</nowiki> , +++^[group0_2_L4 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L4</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ \exists !y.\ y\in G \wedge x\cdot y = 1 $ === , +++^[GroupInv_def | Group_ZF ]... Definition of <nowiki>GroupInv</nowiki>:
$ GroupInv(G,f) \equiv \{\langle x,y\rangle \in G\times G.\ f\langle x,y\rangle = TheNeutralElement(G,f)\}$===
''ultimately '' ''show'' $ thesis$ ''using '' <nowiki>func1_1_L11</nowiki>
''qed'' ===
We can think about the group inverse (the function) as the inverse image of the neutral element. Recall that in Isabelle $ f^{-1}(A)$ denotes the inverse image of the set $A$.
''theorem'' ''(in '' group0 '') '' <nowiki>group0_2_T3</nowiki>:
'' shows '' $ P^{-1}\{1 \} = GroupInv(G,P)$+++[proof ]>
''from '' groupAssum ''have'' $ P : G\times G \rightarrow G$ ''using '' +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$=== , +++^[IsAmonoid_def | Monoid_ZF ]... Definition of <nowiki>IsAmonoid</nowiki>:
$ \text{IsAmonoid}(G,f) \equiv $
$ f \text{ is associative on } G \wedge $
$ (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g))))$=== , +++^[IsAssociative_def | func_ZF ]... Definition of <nowiki>IsAssociative</nowiki>:
$ P \text{ is associative on } G \equiv P \in 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 )))$===
''then '' ''show'' $ P^{-1}\{1 \} = GroupInv(G,P)$ ''using '' <nowiki>func1_1_L14</nowiki> , +++^[GroupInv_def | Group_ZF ]... Definition of <nowiki>GroupInv</nowiki>:
$ GroupInv(G,f) \equiv \{\langle x,y\rangle \in G\times G.\ f\langle x,y\rangle = TheNeutralElement(G,f)\}$===
''qed'' ===
The inverse is in the group.
''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>:
'' assumes '' A1: $ x\in G$ '' shows '' $ x^{-1}\in G$+++[proof ]>
''from '' groupAssum ''have'' $ GroupInv(G,P) : G\rightarrow G$ ''using '' +++^[group0_2_T2 | Group_ZF ]... ''theorem'' <nowiki>group0_2_T2</nowiki>: ''assumes '' $ \text{IsAgroup}(G,f)$ '' shows '' $ GroupInv(G,f) : G\rightarrow G$ ===
''with '' A1 ''show'' $ thesis$ ''using '' <nowiki>apply_type</nowiki>
''qed'' ===
The notation for the inverse means what it is supposed to mean.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>:
'' assumes '' A1: $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $+++[proof ]>
''from '' groupAssum ''have'' $ GroupInv(G,P) : G\rightarrow G$ ''using '' +++^[group0_2_T2 | Group_ZF ]... ''theorem'' <nowiki>group0_2_T2</nowiki>: ''assumes '' $ \text{IsAgroup}(G,f)$ '' shows '' $ GroupInv(G,f) : G\rightarrow G$ ===
''with '' A1 ''have'' $ \langle x,x^{-1}\rangle \in GroupInv(G,P)$ ''using '' <nowiki>apply_Pair</nowiki>
''then '' ''show'' $ x\cdot x^{-1} = 1 $ ''using '' +++^[GroupInv_def | Group_ZF ]... Definition of <nowiki>GroupInv</nowiki>:
$ GroupInv(G,f) \equiv \{\langle x,y\rangle \in G\times G.\ f\langle x,y\rangle = TheNeutralElement(G,f)\}$===
''with '' A1 ''show'' $ x^{-1}\cdot x = 1 $ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group0_2_T1 | Group_ZF ]... ''theorem'' ''(in '' group0 '') '' <nowiki>group0_2_T1</nowiki>: ''assumes '' $ g\in G$ ''and'' $ b\in G$ ''and'' $ g\cdot b = 1 $ '' shows '' $ b\cdot g = 1 $ ===
''qed'' ===
The next two lemmas state that unless we multiply by the neutral element, the result is always different than any of the operands.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L7</nowiki>:
'' assumes '' A1: $ a\in G$ ''and '' A2: $ b\in G$ ''and '' A3: $ a\cdot b = a$ '' shows '' $ b=1 $+++[proof ]>
''from '' A3 ''have'' $ a^{-1} \cdot (a\cdot b) = a^{-1}\cdot a$
''with '' A1, A2 ''show'' $ thesis$ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ === , +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''qed'' ===
See the comment to //group0_2_L7//.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L8</nowiki>:
'' assumes '' A1: $ a\in G$ ''and '' A2: $ b\in G$ ''and '' A3: $ a\cdot b = b$ '' shows '' $ a=1 $+++[proof ]>
''from '' A3 ''have'' $ (a\cdot b)\cdot b^{-1} = b\cdot b^{-1}$
''with '' A1, A2 ''have'' $ a\cdot (b\cdot b^{-1}) = b\cdot b^{-1}$ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''with '' A1, A2 ''show'' $ thesis$ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''qed'' ===
The inverse of the neutral element is the neutral element.
''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_one</nowiki>:
'' shows '' $ 1 ^{-1} = 1 $ ''using '' +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ === , +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L7 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L7</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ ''and'' $ a\cdot b = a$ '' shows '' $ b=1 $ ===
if $a^{-1} = 1$, then $a=1$.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L8A</nowiki>:
'' assumes '' A1: $ a\in G$ ''and '' A2: $ a^{-1} = 1 $ '' shows '' $ a = 1 $+++[proof ]>
''from '' A1 ''have'' $ a\cdot a^{-1} = 1 $ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ ===
''with '' A1, A2 ''show'' $ a = 1 $ ''using '' +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''qed'' ===
If $a$ is not a unit, then its inverse is not a unit either.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L8B</nowiki>:
'' assumes '' $ a\in G$ ''and '' $ a \neq 1 $ '' shows '' $ a^{-1} \neq 1 $ ''using '' <nowiki>assms</nowiki> , +++^[group0_2_L8A | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L8A</nowiki>: ''assumes '' $ a\in G$ ''and'' $ a^{-1} = 1 $ '' shows '' $ a = 1 $ ===
If $a^{-1}$ is not a unit, then a is not a unit either.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L8C</nowiki>:
'' assumes '' $ a\in G$ ''and '' $ a^{-1} \neq 1 $ '' shows '' $ a\neq 1 $ ''using '' <nowiki>assms</nowiki> , +++^[group0_2_L8A | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L8A</nowiki>: ''assumes '' $ a\in G$ ''and'' $ a^{-1} = 1 $ '' shows '' $ a = 1 $ === , +++^[group_inv_of_one | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_one</nowiki>: '' shows '' $ 1 ^{-1} = 1 $ ===
If a product of two elements of a group is equal to the neutral element then they are inverses of each other.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L9</nowiki>:
'' assumes '' A1: $ a\in G$ ''and '' A2: $ b\in G$ ''and '' A3: $ a\cdot b = 1 $ '' shows '' $ a = b^{-1}$ ''and '' $ b = a^{-1}$+++[proof ]>
''from '' A3 ''have'' $ a\cdot b\cdot b^{-1} = 1 \cdot b^{-1}$
''with '' A1, A2 ''have'' $ a\cdot (b\cdot b^{-1}) = 1 \cdot b^{-1}$ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''with '' A1, A2 ''show'' $ a = b^{-1}$ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''from '' A3 ''have'' $ a^{-1}\cdot (a\cdot b) = a^{-1}\cdot 1 $
''with '' A1, A2 ''show'' $ b = a^{-1}$ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ === , +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''qed'' ===
It happens quite often that we know what is (have a meta-function for) the right inverse in a group. The next lemma shows that the value of the group inverse (function) is equal to the right inverse (meta-function).
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L9A</nowiki>:
'' assumes '' A1: $ \forall g\in G.\ b(g) \in G \wedge g\cdot b(g) = 1 $ '' shows '' $ \forall g\in G.\ b(g) = g^{-1}$+++[proof ]>
''fix '' $ g$
''assume '' $ g\in G$
''moreover'' ''from '' A1, $ g\in G$ ''have'' $ b(g) \in G$
''moreover'' ''from '' A1, $ g\in G$ ''have'' $ g\cdot b(g) = 1 $
''ultimately '' ''show'' $ b(g) = g^{-1}$ '' by (rule '' +++^[group0_2_L9 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L9</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ ''and'' $ a\cdot b = 1 $ '' shows '' $ a = b^{-1}$ ''and'' $ b = a^{-1}$ === '')''
''qed'' ===
What is the inverse of a product?
''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_two</nowiki>:
'' assumes '' A1: $ a\in G$ ''and '' A2: $ b\in G$ '' shows '' $ b^{-1}\cdot a^{-1} = (a\cdot b)^{-1}$+++[proof ]>
''from '' A1, A2 ''have'' $ b^{-1}\in G$, $ a^{-1}\in G$, $ a\cdot b\in G$, $ b^{-1}\cdot a^{-1} \in G$ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group_op_closed | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_op_closed</nowiki>: ''assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\cdot b \in G$ ===
''from '' A1, A2, $ b^{-1}\cdot a^{-1} \in G$ ''have'' $ a\cdot b\cdot (b^{-1}\cdot a^{-1}) = a\cdot (b\cdot (b^{-1}\cdot a^{-1}))$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''moreover'' ''from '' A2, $ b^{-1}\in G$, $ a^{-1}\in G$ ''have'' $ b\cdot (b^{-1}\cdot a^{-1}) = b\cdot b^{-1}\cdot a^{-1}$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''moreover'' ''from '' A2, $ a^{-1}\in G$ ''have'' $ b\cdot b^{-1}\cdot a^{-1} = a^{-1}$ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''ultimately '' ''have'' $ a\cdot b\cdot (b^{-1}\cdot a^{-1}) = a\cdot a^{-1}$
''with '' A1 ''have'' $ a\cdot b\cdot (b^{-1}\cdot a^{-1}) = 1 $ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ ===
''with '' $ a\cdot b \in G$, $ b^{-1}\cdot a^{-1} \in G$ ''show'' $ b^{-1}\cdot a^{-1} = (a\cdot b)^{-1}$ ''using '' +++^[group0_2_L9 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L9</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ ''and'' $ a\cdot b = 1 $ '' shows '' $ a = b^{-1}$ ''and'' $ b = a^{-1}$ ===
''qed'' ===
What is the inverse of a product of three elements?
''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_three</nowiki>:
'' assumes '' A1: $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (a\cdot b)^{-1}$, $ (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (b^{-1}\cdot a^{-1})$, $ (a\cdot b\cdot c)^{-1} = c^{-1}\cdot b^{-1}\cdot a^{-1}$+++[proof ]>
''from '' A1 ''have'' T: $ a\cdot b \in G$, $ a^{-1} \in G$, $ b^{-1} \in G$, $ c^{-1} \in G$ ''using '' +++^[group_op_closed | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_op_closed</nowiki>: ''assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\cdot b \in G$ === , +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ ===
''with '' A1 ''show'' $ (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (a\cdot b)^{-1}$ ''and '' $ (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (b^{-1}\cdot a^{-1})$ ''using '' +++^[group_inv_of_two | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_two</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ '' shows '' $ b^{-1}\cdot a^{-1} = (a\cdot b)^{-1}$ ===
''with '' T ''show'' $ (a\cdot b\cdot c)^{-1} = c^{-1}\cdot b^{-1}\cdot a^{-1}$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''qed'' ===
The inverse of the inverse is the element.
''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_inv</nowiki>:
'' assumes '' $ a\in G$ '' shows '' $ a = (a^{-1})^{-1}$ ''using '' <nowiki>assms</nowiki> , +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L9 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L9</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ ''and'' $ a\cdot b = 1 $ '' shows '' $ a = b^{-1}$ ''and'' $ b = a^{-1}$ ===
If $a^{-1}\cdot b=1$, then $a=b$.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L11</nowiki>:
'' assumes '' A1: $ a\in G$, $ b\in G$ ''and '' A2: $ a^{-1}\cdot b = 1 $ '' shows '' $ a=b$+++[proof ]>
''from '' A1, A2 ''have'' $ a^{-1} \in G$, $ b\in G$, $ a^{-1}\cdot b = 1 $ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ ===
''then '' ''have'' $ b = (a^{-1})^{-1}$ '' by (rule '' +++^[group0_2_L9 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L9</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ ''and'' $ a\cdot b = 1 $ '' shows '' $ a = b^{-1}$ ''and'' $ b = a^{-1}$ === '')''
''with '' A1 ''show'' $ a=b$ ''using '' +++^[group_inv_of_inv | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_inv</nowiki>: ''assumes '' $ a\in G$ '' shows '' $ a = (a^{-1})^{-1}$ ===
''qed'' ===
If $a\cdot b^{-1}=1$, then $a=b$.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L11A</nowiki>:
'' assumes '' A1: $ a\in G$, $ b\in G$ ''and '' A2: $ a\cdot b^{-1} = 1 $ '' shows '' $ a=b$+++[proof ]>
''from '' A1, A2 ''have'' $ a \in G$, $ b^{-1}\in G$, $ a\cdot b^{-1} = 1 $ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ ===
''then '' ''have'' $ a = (b^{-1})^{-1}$ '' by (rule '' +++^[group0_2_L9 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L9</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ ''and'' $ a\cdot b = 1 $ '' shows '' $ a = b^{-1}$ ''and'' $ b = a^{-1}$ === '')''
''with '' A1 ''show'' $ a=b$ ''using '' +++^[group_inv_of_inv | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_inv</nowiki>: ''assumes '' $ a\in G$ '' shows '' $ a = (a^{-1})^{-1}$ ===
''qed'' ===
If if the inverse of $b$ is different than $a$, then the inverse of $a$ is different than $b$.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L11B</nowiki>:
'' assumes '' A1: $ a\in G$ ''and '' A2: $ b^{-1} \neq a$ '' shows '' $ a^{-1} \neq b$+++[proof ]>
''{ '' ''assume '' $ a^{-1} = b$
''then '' ''have'' $ (a^{-1})^{-1} = b^{-1}$
''with '' A1, A2 ''have'' $ False$ ''using '' +++^[group_inv_of_inv | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_inv</nowiki>: ''assumes '' $ a\in G$ '' shows '' $ a = (a^{-1})^{-1}$ ===
'' }''
''then '' ''show'' $ a^{-1} \neq b$
''qed'' ===
What is the inverse of $ab^{-1}$ ?
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L12</nowiki>:
'' assumes '' A1: $ a\in G$, $ b\in G$ '' shows '' $ (a\cdot b^{-1})^{-1} = b\cdot a^{-1}$, $ (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a$+++[proof ]>
''from '' A1 ''have'' $ (a\cdot b^{-1})^{-1} = (b^{-1})^{-1}\cdot a^{-1}$ ''and '' $ (a^{-1}\cdot b)^{-1} = b^{-1}\cdot (a^{-1})^{-1}$ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group_inv_of_two | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_two</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ '' shows '' $ b^{-1}\cdot a^{-1} = (a\cdot b)^{-1}$ ===
''with '' A1 ''show'' $ (a\cdot b^{-1})^{-1} = b\cdot a^{-1}$, $ (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a$ ''using '' +++^[group_inv_of_inv | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_inv</nowiki>: ''assumes '' $ a\in G$ '' shows '' $ a = (a^{-1})^{-1}$ ===
''qed'' ===
A couple useful rearrangements with three elements: we can insert a $b\cdot b^{-1}$ between two group elements (another version) and one about a product of an element and inverse of a product, and two others.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L14A</nowiki>:
'' assumes '' A1: $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1})$, $ a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c)$, $ a\cdot (b\cdot c)^{-1} = a\cdot c^{-1}\cdot b^{-1}$, $ a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1}$, $ (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1}$, $ a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a$, $ a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b$+++[proof ]>
''from '' A1 ''have'' T: $ a^{-1} \in G$, $ b^{-1}\in G$, $ c^{-1}\in G$, $ a^{-1}\cdot b \in G$, $ a\cdot b^{-1} \in G$, $ a\cdot b \in G$, $ c\cdot b^{-1} \in G$, $ b\cdot c \in G$ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group_op_closed | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_op_closed</nowiki>: ''assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\cdot b \in G$ ===
''from '' A1, T ''have'' $ a\cdot c^{-1} = a\cdot (b^{-1}\cdot b)\cdot c^{-1}$, $ a^{-1}\cdot c = a^{-1}\cdot (b\cdot b^{-1})\cdot c$ ''using '' +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ === , +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ ===
''with '' A1, T ''show'' $ a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1})$, $ a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c)$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''from '' A1 ''have'' $ a\cdot (b\cdot c)^{-1} = a\cdot (c^{-1}\cdot b^{-1})$ ''using '' +++^[group_inv_of_two | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_two</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ '' shows '' $ b^{-1}\cdot a^{-1} = (a\cdot b)^{-1}$ ===
''with '' A1, T ''show'' $ a\cdot (b\cdot c)^{-1} =a\cdot c^{-1}\cdot b^{-1}$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''from '' A1, T ''show'' $ a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1}$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''from '' A1, T ''show'' $ (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1}$ ''using '' +++^[group_inv_of_three | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_three</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (a\cdot b)^{-1}$,
$ (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (b^{-1}\cdot a^{-1})$,
$ (a\cdot b\cdot c)^{-1} = c^{-1}\cdot b^{-1}\cdot a^{-1}$ === , +++^[group_inv_of_inv | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_inv</nowiki>: ''assumes '' $ a\in G$ '' shows '' $ a = (a^{-1})^{-1}$ ===
''from '' T ''have'' $ a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a\cdot b\cdot (c^{-1}\cdot (c\cdot b^{-1}))$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''also'' ''from '' A1, T ''have'' $ \ldots = a\cdot b\cdot b^{-1}$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ === , +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''also'' ''from '' A1, T ''have'' $ \ldots = a\cdot (b\cdot b^{-1})$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''also'' ''from '' A1 ''have'' $ \ldots = a$ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''finally '' ''show'' $ a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a$
''from '' A1, T ''have'' $ a\cdot (b\cdot c)\cdot c^{-1} = a\cdot (b\cdot (c\cdot c^{-1}))$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''also'' ''from '' A1, T ''have'' $ \ldots = a\cdot b$ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''finally '' ''show'' $ a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b$
''qed'' ===
Another lemma about rearranging a product of four group elements.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L15</nowiki>:
'' assumes '' A1: $ a\in G$, $ b\in G$, $ c\in G$, $ d\in G$ '' shows '' $ (a\cdot b)\cdot (c\cdot d)^{-1} = a\cdot (b\cdot d^{-1})\cdot a^{-1}\cdot (a\cdot c^{-1})$+++[proof ]>
''from '' A1 ''have'' T1: $ d^{-1}\in G$, $ c^{-1}\in G$, $ a\cdot b\in G$, $ a\cdot (b\cdot d^{-1})\in G$ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group_op_closed | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_op_closed</nowiki>: ''assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\cdot b \in G$ ===
''with '' A1 ''have'' $ (a\cdot b)\cdot (c\cdot d)^{-1} = (a\cdot b)\cdot (d^{-1}\cdot c^{-1})$ ''using '' +++^[group_inv_of_two | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_two</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ '' shows '' $ b^{-1}\cdot a^{-1} = (a\cdot b)^{-1}$ ===
''also'' ''from '' A1, T1 ''have'' $ \ldots = a\cdot (b\cdot d^{-1})\cdot c^{-1}$ ''using '' +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''also'' ''from '' A1, T1 ''have'' $ \ldots = a\cdot (b\cdot d^{-1})\cdot a^{-1}\cdot (a\cdot c^{-1})$ ''using '' +++^[group0_2_L14A | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L14A</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1})$,
$ a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c)$,
$ a\cdot (b\cdot c)^{-1} = a\cdot c^{-1}\cdot b^{-1}$,
$ a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1}$,
$ (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1}$,
$ a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a$, $ a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b$ ===
''finally '' ''show'' $ thesis$
''qed'' ===
We can cancel an element with its inverse that is written next to it.
''lemma'' ''(in '' group0 '') '' <nowiki>inv_cancel_two</nowiki>:
'' assumes '' A1: $ a\in G$, $ b\in G$ '' shows '' $ a\cdot b^{-1}\cdot b = a$, $ a\cdot b\cdot b^{-1} = a$, $ a^{-1}\cdot (a\cdot b) = b$, $ a\cdot (a^{-1}\cdot b) = b$+++[proof ]>
''from '' A1 ''have'' $ a\cdot b^{-1}\cdot b = a\cdot (b^{-1}\cdot b)$, $ a\cdot b\cdot b^{-1} = a\cdot (b\cdot b^{-1})$, $ a^{-1}\cdot (a\cdot b) = a^{-1}\cdot a\cdot b$, $ a\cdot (a^{-1}\cdot b) = a\cdot a^{-1}\cdot b$ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''with '' A1 ''show'' $ a\cdot b^{-1}\cdot b = a$, $ a\cdot b\cdot b^{-1} = a$, $ a^{-1}\cdot (a\cdot b) = b$, $ a\cdot (a^{-1}\cdot b) = b$ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''qed'' ===
Another lemma about cancelling with two group elements.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L16A</nowiki>:
'' assumes '' A1: $ a\in G$, $ b\in G$ '' shows '' $ a\cdot (b\cdot a)^{-1} = b^{-1}$+++[proof ]>
''from '' A1 ''have'' $ (b\cdot a)^{-1} = a^{-1}\cdot b^{-1}$, $ b^{-1} \in G$ ''using '' +++^[group_inv_of_two | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_inv_of_two</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ '' shows '' $ b^{-1}\cdot a^{-1} = (a\cdot b)^{-1}$ === , +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ ===
''with '' A1 ''show'' $ a\cdot (b\cdot a)^{-1} = b^{-1}$ ''using '' +++^[inv_cancel_two | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inv_cancel_two</nowiki>: ''assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\cdot b^{-1}\cdot b = a$,
$ a\cdot b\cdot b^{-1} = a$, $ a^{-1}\cdot (a\cdot b) = b$, $ a\cdot (a^{-1}\cdot b) = b$ ===
''qed'' ===
Adding a neutral element to a set that is closed under the group operation results in a set that is closed under the group operation.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L17</nowiki>:
'' assumes '' $ H\subseteq G$ ''and '' $ H \text{ is closed under } P$ '' shows '' $ (H \cup \{1 \}) \text{ is closed under } P$ ''using '' <nowiki>assms</nowiki> , +++^[IsOpClosed_def | func_ZF ]... Definition of <nowiki>IsOpClosed</nowiki>:
$ A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A$=== , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
We can put an element on the other side of an equation.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L18</nowiki>:
'' assumes '' A1: $ a\in G$, $ b\in G$, $ c\in G$ ''and '' A2: $ c = a\cdot b$ '' shows '' $ c\cdot b^{-1} = a$, $ a^{-1}\cdot c = b$+++[proof ]>
''from '' A2, A1 ''have'' $ c\cdot b^{-1} = a\cdot (b\cdot b^{-1})$, $ a^{-1}\cdot c = (a^{-1}\cdot a)\cdot b$ ''using '' +++^[inverse_in_group | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inverse_in_group</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x^{-1}\in G$ === , +++^[group_oper_assoc | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group_oper_assoc</nowiki>: ''assumes '' $ a\in G$, $ b\in G$, $ c\in G$ '' shows '' $ a\cdot (b\cdot c) = a\cdot b\cdot c$ ===
''moreover'' ''from '' A1 ''have'' $ a\cdot (b\cdot b^{-1}) = a$, $ (a^{-1}\cdot a)\cdot b = b$ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
''ultimately '' ''show'' $ c\cdot b^{-1} = a$, $ a^{-1}\cdot c = b$
''qed'' ===
Multiplying different group elements by the same factor results in different group elements.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L19</nowiki>:
'' assumes '' A1: $ a\in G$, $ b\in G$, $ c\in G$ ''and '' A2: $ a\neq b$ '' shows '' $ a\cdot c \neq b\cdot c$ ''and '' $ c\cdot a \neq c\cdot b$+++[proof ]>
''{ '' ''assume '' $ a\cdot c = b\cdot c \vee c\cdot a =c\cdot b$
''then '' ''have'' $ a\cdot c\cdot c^{-1} = b\cdot c\cdot c^{-1} \vee c^{-1}\cdot (c\cdot a) = c^{-1}\cdot (c\cdot b)$
''with '' A1, A2 ''have'' $ False$ ''using '' +++^[inv_cancel_two | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>inv_cancel_two</nowiki>: ''assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\cdot b^{-1}\cdot b = a$,
$ a\cdot b\cdot b^{-1} = a$, $ a^{-1}\cdot (a\cdot b) = b$, $ a\cdot (a^{-1}\cdot b) = b$ ===
'' }''
''then '' ''show'' $ a\cdot c \neq b\cdot c$ ''and '' $ c\cdot a \neq c\cdot b$
''qed'' ===
!Subgroups
There are two common ways to define subgroups. One requires that the group operation is closed in the subgroup. The second one defines subgroup as a subset of a group which is itself a group under the group operations. We use the second approach because it results in shorter definition.
The rest of this section is devoted to proving the equivalence of these two definitions of the notion of a subgroup.
A pair $(H,P)$ is a subgroup if $H$ forms a group with the operation $P$ restricted to $H\times H$. It may be surprising that we don't require $H$ to be a subset of $G$. This however can be inferred from the definition if the pair $(G,P)$ is a group, see lemma //group0_3_L2//.
''Definition
'' $ IsAsubgroup(H,P) \equiv \text{IsAgroup}(H, restrict(P,H\times H))$
Formally the group operation in a subgroup is different than in the group as they have different domains. Of course we want to use the original operation with the associated notation in the subgroup. The next couple of lemmas will allow for that. The next lemma states that the neutral element of a subgroup is in the subgroup and it is both right and left neutral there. The notation is very ugly because we don't want to introduce a separate notation for the subgroup operation.
''lemma'' <nowiki>group0_3_L1</nowiki>:
'' assumes '' A1: $ IsAsubgroup(H,f)$ ''and '' A2: $ n = TheNeutralElement(H,restrict(f,H\times H))$ '' shows '' $ n \in H$, $ \forall h\in H.\ restrict(f,H\times H)\langle n,h \rangle = h$, $ \forall h\in H.\ restrict(f,H\times H)\langle h,n\rangle = h$+++[proof ]>
''let '' $ b = restrict(f,H\times H)$
''let '' $ e = TheNeutralElement(H,restrict(f,H\times H))$
''from '' A1 ''have'' $ group0(H,b)$ ''using '' +++^[IsAsubgroup_def | Group_ZF ]... Definition of <nowiki>IsAsubgroup</nowiki>:
$ IsAsubgroup(H,P) \equiv \text{IsAgroup}(H, restrict(P,H\times H))$=== , <nowiki>group0_def</nowiki>
''then '' ''have'' I: $ e \in H \wedge (\forall h\in H.\ (b\langle e,h \rangle = h \wedge b\langle h,e\rangle = h))$ '' by (rule '' +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ === '')''
''with '' A2 ''show'' $ n \in H$
''from '' A2, I ''show'' $ \forall h\in H.\ b\langle n,h\rangle = h$ ''and '' $ \forall h\in H.\ b\langle h,n\rangle = h$
''qed'' ===
A subgroup is contained in the group.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L2</nowiki>:
'' assumes '' A1: $ IsAsubgroup(H,P)$ '' shows '' $ H \subseteq G$+++[proof ]>
''fix '' $ h$
''assume '' $ h\in H$
''let '' $ b = restrict(P,H\times H)$
''let '' $ n = TheNeutralElement(H,restrict(P,H\times H))$
''from '' A1 ''have'' $ b \in H\times H\rightarrow H$ ''using '' +++^[IsAsubgroup_def | Group_ZF ]... Definition of <nowiki>IsAsubgroup</nowiki>:
$ IsAsubgroup(H,P) \equiv \text{IsAgroup}(H, restrict(P,H\times H))$=== , +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$=== , +++^[IsAmonoid_def | Monoid_ZF ]... Definition of <nowiki>IsAmonoid</nowiki>:
$ \text{IsAmonoid}(G,f) \equiv $
$ f \text{ is associative on } G \wedge $
$ (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g))))$=== , +++^[IsAssociative_def | func_ZF ]... Definition of <nowiki>IsAssociative</nowiki>:
$ P \text{ is associative on } G \equiv P \in 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 )))$===
''moreover'' ''from '' A1, $ h\in H$ ''have'' $ \langle n,h\rangle \in H\times H$ ''using '' +++^[group0_3_L1 | Group_ZF ]... ''lemma'' <nowiki>group0_3_L1</nowiki>: ''assumes '' $ IsAsubgroup(H,f)$ ''and'' $ n = TheNeutralElement(H,restrict(f,H\times H))$ '' shows '' $ n \in H$, $ \forall h\in H.\ restrict(f,H\times H)\langle n,h \rangle = h$,
$ \forall h\in H.\ restrict(f,H\times H)\langle h,n\rangle = h$ ===
''moreover'' ''from '' A1, $ h\in H$ ''have'' $ h = b\langle n,h \rangle $ ''using '' +++^[group0_3_L1 | Group_ZF ]... ''lemma'' <nowiki>group0_3_L1</nowiki>: ''assumes '' $ IsAsubgroup(H,f)$ ''and'' $ n = TheNeutralElement(H,restrict(f,H\times H))$ '' shows '' $ n \in H$, $ \forall h\in H.\ restrict(f,H\times H)\langle n,h \rangle = h$,
$ \forall h\in H.\ restrict(f,H\times H)\langle h,n\rangle = h$ ===
''ultimately '' ''have'' $ \langle \langle n,h\rangle ,h\rangle \in b$ ''using '' <nowiki>func1_1_L5A</nowiki>
''then '' ''have'' $ \langle \langle n,h\rangle ,h\rangle \in P$ ''using '' <nowiki>restrict_subset</nowiki>
''moreover'' ''from '' groupAssum ''have'' $ P:G\times G\rightarrow G$ ''using '' +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$=== , +++^[IsAmonoid_def | Monoid_ZF ]... Definition of <nowiki>IsAmonoid</nowiki>:
$ \text{IsAmonoid}(G,f) \equiv $
$ f \text{ is associative on } G \wedge $
$ (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g))))$=== , +++^[IsAssociative_def | func_ZF ]... Definition of <nowiki>IsAssociative</nowiki>:
$ P \text{ is associative on } G \equiv P \in 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 )))$===
''ultimately '' ''show'' $ h\in G$ ''using '' <nowiki>func1_1_L5</nowiki>
''qed'' ===
The group's neutral element (denoted $1$ in the group0 context) is a neutral element for the subgroup with respect to the group action.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L3</nowiki>:
'' assumes '' $ IsAsubgroup(H,P)$ '' shows '' $ \forall h\in H.\ 1 \cdot h = h \wedge h\cdot 1 = h$ ''using '' <nowiki>assms</nowiki> , <nowiki>groupAssum</nowiki> , +++^[group0_3_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L2</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ '' shows '' $ H \subseteq G$ === , +++^[group0_2_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L2</nowiki>: '' shows '' $ 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$ ===
The neutral element of a subgroup is the same as that of the group.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L4</nowiki>:
'' assumes '' A1: $ IsAsubgroup(H,P)$ '' shows '' $ TheNeutralElement(H,restrict(P,H\times H)) = 1 $+++[proof ]>
''let '' $ n = TheNeutralElement(H,restrict(P,H\times H))$
''from '' A1 ''have'' $ n \in H$ ''using '' +++^[group0_3_L1 | Group_ZF ]... ''lemma'' <nowiki>group0_3_L1</nowiki>: ''assumes '' $ IsAsubgroup(H,f)$ ''and'' $ n = TheNeutralElement(H,restrict(f,H\times H))$ '' shows '' $ n \in H$, $ \forall h\in H.\ restrict(f,H\times H)\langle n,h \rangle = h$,
$ \forall h\in H.\ restrict(f,H\times H)\langle h,n\rangle = h$ ===
''with '' groupAssum, A1 ''have'' $ n\in G$ ''using '' +++^[group0_3_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L2</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ '' shows '' $ H \subseteq G$ ===
''with '' A1, $ n \in H$ ''show'' $ thesis$ ''using '' +++^[group0_3_L1 | Group_ZF ]... ''lemma'' <nowiki>group0_3_L1</nowiki>: ''assumes '' $ IsAsubgroup(H,f)$ ''and'' $ n = TheNeutralElement(H,restrict(f,H\times H))$ '' shows '' $ n \in H$, $ \forall h\in H.\ restrict(f,H\times H)\langle n,h \rangle = h$,
$ \forall h\in H.\ restrict(f,H\times H)\langle h,n\rangle = h$ === , <nowiki>restrict_if</nowiki> , +++^[group0_2_L7 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L7</nowiki>: ''assumes '' $ a\in G$ ''and'' $ b\in G$ ''and'' $ a\cdot b = a$ '' shows '' $ b=1 $ ===
''qed'' ===
The neutral element of the group (denoted $1$ in the group0 context) belongs to every subgroup.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L5</nowiki>:
'' assumes '' A1: $ IsAsubgroup(H,P)$ '' shows '' $ 1 \in H$+++[proof ]>
''from '' A1 ''show'' $ 1 \in H$ ''using '' +++^[group0_3_L1 | Group_ZF ]... ''lemma'' <nowiki>group0_3_L1</nowiki>: ''assumes '' $ IsAsubgroup(H,f)$ ''and'' $ n = TheNeutralElement(H,restrict(f,H\times H))$ '' shows '' $ n \in H$, $ \forall h\in H.\ restrict(f,H\times H)\langle n,h \rangle = h$,
$ \forall h\in H.\ restrict(f,H\times H)\langle h,n\rangle = h$ === , +++^[group0_3_L4 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L4</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ '' shows '' $ TheNeutralElement(H,restrict(P,H\times H)) = 1 $ ===
''qed'' ===
Subgroups are closed with respect to the group operation.
''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L6</nowiki>:
'' assumes '' A1: $ IsAsubgroup(H,P)$ ''and '' A2: $ a\in H$, $ b\in H$ '' shows '' $ a\cdot b \in H$+++[proof ]>
''let '' $ f = restrict(P,H\times H)$
''from '' A1 ''have'' $ monoid0(H,f)$ ''using '' +++^[IsAsubgroup_def | Group_ZF ]... Definition of <nowiki>IsAsubgroup</nowiki>:
$ IsAsubgroup(H,P) \equiv \text{IsAgroup}(H, restrict(P,H\times H))$=== , +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$=== , <nowiki>monoid0_def</nowiki>
''with '' A2 ''have'' $ f (\langle a,b\rangle ) \in H$ ''using '' +++^[group0_1_L1 | Monoid_ZF ]... ''lemma'' ''(in '' monoid0 '') '' <nowiki>group0_1_L1</nowiki>: ''assumes '' $ a\in G$, $ b\in G$ '' shows '' $ a\oplus b \in G$ ===
''with '' A2 ''show'' $ a\cdot b \in H$ ''using '' <nowiki>restrict_if</nowiki>
''qed'' ===
A preliminary lemma that we need to show that taking the inverse in the subgroup is the same as taking the inverse in the group.
''lemma'' <nowiki>group0_3_L7A</nowiki>:
'' assumes '' A1: $ \text{IsAgroup}(G,f)$ ''and '' A2: $ IsAsubgroup(H,f)$ ''and '' A3: $ g = restrict(f,H\times H)$ '' shows '' $ GroupInv(G,f) \cap H\times H = GroupInv(H,g)$+++[proof ]>
''let '' $ e = TheNeutralElement(G,f)$
''let '' $ e_1 = TheNeutralElement(H,g)$
''from '' A1 ''have'' $ group0(G,f)$ ''using '' <nowiki>group0_def</nowiki>
''from '' A2, A3 ''have'' $ group0(H,g)$ ''using '' +++^[IsAsubgroup_def | Group_ZF ]... Definition of <nowiki>IsAsubgroup</nowiki>:
$ IsAsubgroup(H,P) \equiv \text{IsAgroup}(H, restrict(P,H\times H))$=== , <nowiki>group0_def</nowiki>
''from '' $ group0(G,f)$, A2, A3 ''have'' $ GroupInv(G,f) = f^{-1}\text{ e_1 }$ ''using '' +++^[group0_3_L4 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L4</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ '' shows '' $ TheNeutralElement(H,restrict(P,H\times H)) = 1 $ === , +++^[group0_2_T3 | Group_ZF ]... ''theorem'' ''(in '' group0 '') '' <nowiki>group0_2_T3</nowiki>: '' shows '' $ P^{-1}\{1 \} = GroupInv(G,P)$ ===
''moreover'' ''have'' $ g^{-1}\text{ e_1 } = f^{-1}\text{ e_1 } \cap H\times H$+++[proof ]>
''from '' A1 ''have'' $ f \in G\times G\rightarrow G$ ''using '' +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$=== , +++^[IsAmonoid_def | Monoid_ZF ]... Definition of <nowiki>IsAmonoid</nowiki>:
$ \text{IsAmonoid}(G,f) \equiv $
$ f \text{ is associative on } G \wedge $
$ (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g))))$=== , +++^[IsAssociative_def | func_ZF ]... Definition of <nowiki>IsAssociative</nowiki>:
$ P \text{ is associative on } G \equiv P \in 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 )))$===
''moreover'' ''from '' A2, $ group0(G,f)$ ''have'' $ H\times H \subseteq G\times G$ ''using '' +++^[group0_3_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L2</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ '' shows '' $ H \subseteq G$ ===
''ultimately '' ''show'' $ g^{-1}\text{ e_1 } = f^{-1}\text{ e_1 } \cap H\times H$ ''using '' <nowiki>A3</nowiki> , <nowiki>func1_2_L1</nowiki>
''qed'' ===
''moreover'' ''from '' A3, $ group0(H,g)$ ''have'' $ GroupInv(H,g) = g^{-1}\text{ e_1 }$ ''using '' +++^[group0_2_T3 | Group_ZF ]... ''theorem'' ''(in '' group0 '') '' <nowiki>group0_2_T3</nowiki>: '' shows '' $ P^{-1}\{1 \} = GroupInv(G,P)$ ===
''ultimately '' ''show'' $ thesis$
''qed'' ===
Using the lemma above we can show the actual statement: taking the inverse in the subgroup is the same as taking the inverse in the group.
''theorem'' ''(in '' group0 '') '' <nowiki>group0_3_T1</nowiki>:
'' assumes '' A1: $ IsAsubgroup(H,P)$ ''and '' A2: $ g = restrict(P,H\times H)$ '' shows '' $ GroupInv(H,g) = restrict(GroupInv(G,P),H)$+++[proof ]>
''from '' groupAssum ''have'' $ GroupInv(G,P) : G\rightarrow G$ ''using '' +++^[group0_2_T2 | Group_ZF ]... ''theorem'' <nowiki>group0_2_T2</nowiki>: ''assumes '' $ \text{IsAgroup}(G,f)$ '' shows '' $ GroupInv(G,f) : G\rightarrow G$ ===
''moreover'' ''from '' A1, A2 ''have'' $ GroupInv(H,g) : H\rightarrow H$ ''using '' +++^[IsAsubgroup_def | Group_ZF ]... Definition of <nowiki>IsAsubgroup</nowiki>:
$ IsAsubgroup(H,P) \equiv \text{IsAgroup}(H, restrict(P,H\times H))$=== , +++^[group0_2_T2 | Group_ZF ]... ''theorem'' <nowiki>group0_2_T2</nowiki>: ''assumes '' $ \text{IsAgroup}(G,f)$ '' shows '' $ GroupInv(G,f) : G\rightarrow G$ ===
''moreover'' ''from '' A1 ''have'' $ H \subseteq G$ ''using '' +++^[group0_3_L2 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L2</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ '' shows '' $ H \subseteq G$ ===
''moreover'' ''from '' groupAssum, A1, A2 ''have'' $ GroupInv(G,P) \cap H\times H = GroupInv(H,g)$ ''using '' +++^[group0_3_L7A | Group_ZF ]... ''lemma'' <nowiki>group0_3_L7A</nowiki>: ''assumes '' $ \text{IsAgroup}(G,f)$ ''and'' $ IsAsubgroup(H,f)$ ''and'' $ g = restrict(f,H\times H)$ '' shows '' $ GroupInv(G,f) \cap H\times H = GroupInv(H,g)$ ===
''ultimately '' ''show'' $ thesis$ ''using '' <nowiki>func1_2_L3</nowiki>
''qed'' ===
A sligtly weaker, but more convenient in applications, reformulation of the above theorem.
''theorem'' ''(in '' group0 '') '' <nowiki>group0_3_T2</nowiki>:
'' assumes '' $ IsAsubgroup(H,P)$ ''and '' $ g = restrict(P,H\times H)$ '' shows '' $ \forall h\in H.\ GroupInv(H,g)(h) = h^{-1}$ ''using '' <nowiki>assms</nowiki> , +++^[group0_3_T1 | Group_ZF ]... ''theorem'' ''(in '' group0 '') '' <nowiki>group0_3_T1</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ ''and'' $ g = restrict(P,H\times H)$ '' shows '' $ GroupInv(H,g) = restrict(GroupInv(G,P),H)$ === , <nowiki>restrict_if</nowiki>
Subgroups are closed with respect to taking the group inverse.
''theorem'' ''(in '' group0 '') '' <nowiki>group0_3_T3A</nowiki>:
'' assumes '' A1: $ IsAsubgroup(H,P)$ ''and '' A2: $ h\in H$ '' shows '' $ h^{-1}\in H$+++[proof ]>
''let '' $ g = restrict(P,H\times H)$
''from '' A1 ''have'' $ GroupInv(H,g) \in H\rightarrow H$ ''using '' +++^[IsAsubgroup_def | Group_ZF ]... Definition of <nowiki>IsAsubgroup</nowiki>:
$ IsAsubgroup(H,P) \equiv \text{IsAgroup}(H, restrict(P,H\times H))$=== , +++^[group0_2_T2 | Group_ZF ]... ''theorem'' <nowiki>group0_2_T2</nowiki>: ''assumes '' $ \text{IsAgroup}(G,f)$ '' shows '' $ GroupInv(G,f) : G\rightarrow G$ ===
''with '' A2 ''have'' $ GroupInv(H,g)(h) \in H$ ''using '' <nowiki>apply_type</nowiki>
''with '' A1, A2 ''show'' $ h^{-1}\in H$ ''using '' +++^[group0_3_T2 | Group_ZF ]... ''theorem'' ''(in '' group0 '') '' <nowiki>group0_3_T2</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ ''and'' $ g = restrict(P,H\times H)$ '' shows '' $ \forall h\in H.\ GroupInv(H,g)(h) = h^{-1}$ ===
''qed'' ===
The next theorem states that a nonempty subset of a group $G$ that is closed under the group operation and taking the inverse is a subgroup of the group.
''theorem'' ''(in '' group0 '') '' <nowiki>group0_3_T3</nowiki>:
'' assumes '' A1: $ H\neq 0$ ''and '' A2: $ H\subseteq G$ ''and '' A3: $ H \text{ is closed under } P$ ''and '' A4: $ \forall x\in H.\ x^{-1} \in H$ '' shows '' $ IsAsubgroup(H,P)$+++[proof ]>
''let '' $ g = restrict(P,H\times H)$
''let '' $ n = TheNeutralElement(H,g)$
''from '' A3 ''have'' I: $ \forall x\in H.\ \forall y\in H.\ x\cdot y \in H$ ''using '' +++^[IsOpClosed_def | func_ZF ]... Definition of <nowiki>IsOpClosed</nowiki>:
$ A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A$===
''from '' A1 ''obtain '' $ x$ ''where '' $ x\in H$
''with '' A4, I, A2 ''have'' $ 1 \in H$ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ ===
''with '' A3, A2 ''have'' T2: $ \text{IsAmonoid}(H,g)$ ''using '' +++^[group0_2_L1 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L1</nowiki>: '' shows '' $ monoid0(G,P)$ === , +++^[group0_1_T1 | Monoid_ZF ]... ''theorem'' ''(in '' monoid0 '') '' <nowiki>group0_1_T1</nowiki>: ''assumes '' $ H \text{ is closed under } f$ ''and'' $ H\subseteq G$ ''and'' $ TheNeutralElement(G,f) \in H$ '' shows '' $ \text{IsAmonoid}(H,restrict(f,H\times H))$ ===
''moreover'' ''have'' $ \forall h\in H.\ \exists b\in H.\ g\langle h,b\rangle = n$+++[proof ]>
''fix '' $ h$
''assume '' $ h\in H$
''with '' A4, A2 ''have'' $ h\cdot h^{-1} = 1 $ ''using '' +++^[group0_2_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_2_L6</nowiki>: ''assumes '' $ x\in G$ '' shows '' $ x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 $ ===
''moreover'' ''from '' groupAssum, A2, A3, $ 1 \in H$ ''have'' $ 1 = n$ ''using '' +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$=== , +++^[group0_1_L6 | Monoid_ZF ]... ''lemma'' <nowiki>group0_1_L6</nowiki>: ''assumes '' $ \text{IsAmonoid}(G,f)$ ''and'' $ H \text{ is closed under } f$ ''and'' $ H\subseteq G$ ''and'' $ TheNeutralElement(G,f) \in H$ '' shows '' $ TheNeutralElement(H,restrict(f,H\times H)) = TheNeutralElement(G,f)$ ===
''moreover'' ''from '' A4, $ h\in H$ ''have'' $ g\langle h,h^{-1}\rangle = h\cdot h^{-1}$ ''using '' <nowiki>restrict_if</nowiki>
''ultimately '' ''have'' $ g\langle h,h^{-1}\rangle = n$
''with '' A4, $ h\in H$ ''show'' $ \exists b\in H.\ g\langle h,b\rangle = n$
''qed'' ===
''ultimately '' ''show'' $ IsAsubgroup(H,P)$ ''using '' +++^[IsAsubgroup_def | Group_ZF ]... Definition of <nowiki>IsAsubgroup</nowiki>:
$ IsAsubgroup(H,P) \equiv \text{IsAgroup}(H, restrict(P,H\times H))$=== , +++^[IsAgroup_def | Group_ZF ]... Definition of <nowiki>IsAgroup</nowiki>:
$ \text{IsAgroup}(G,f) \equiv $
$ (\text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = TheNeutralElement(G,f)))$===
''qed'' ===
Intersection of subgroups is a subgroup.
''lemma'' <nowiki>group0_3_L7</nowiki>:
'' assumes '' A1: $ \text{IsAgroup}(G,f)$ ''and '' A2: $ IsAsubgroup(H_1,f)$ ''and '' A3: $ IsAsubgroup(H_2,f)$ '' shows '' $ IsAsubgroup(H_1\cap H_2,restrict(f,H_1\times H_1))$+++[proof ]>
''let '' $ e = TheNeutralElement(G,f)$
''let '' $ g = restrict(f,H_1\times H_1)$
''from '' A1 ''have'' I: $ group0(G,f)$ ''using '' <nowiki>group0_def</nowiki>
''from '' A2 ''have'' $ group0(H_1,g)$ ''using '' +++^[IsAsubgroup_def | Group_ZF ]... Definition of <nowiki>IsAsubgroup</nowiki>:
$ IsAsubgroup(H,P) \equiv \text{IsAgroup}(H, restrict(P,H\times H))$=== , <nowiki>group0_def</nowiki>
''moreover'' ''have'' $ H_1\cap H_2 \neq 0$+++[proof ]>
''from '' A1, A2, A3 ''have'' $ e \in H_1\cap H_2$ ''using '' <nowiki>group0_def</nowiki> , +++^[group0_3_L5 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L5</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ '' shows '' $ 1 \in H$ ===
''thus'' $ thesis$
''qed'' ===
''moreover'' ''have'' $ H_1\cap H_2 \subseteq H_1$
''moreover'' ''from '' A2, A3, I, $ H_1\cap H_2 \subseteq H_1$ ''have'' $ H_1\cap H_2 \text{ is closed under } g$ ''using '' +++^[group0_3_L6 | Group_ZF ]... ''lemma'' ''(in '' group0 '') '' <nowiki>group0_3_L6</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ ''and'' $ a\in H$, $ b\in H$ '' shows '' $ a\cdot b \in H$ === , +++^[IsOpClosed_def | func_ZF ]... Definition of <nowiki>IsOpClosed</nowiki>:
$ A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A$=== , +++^[func_ZF_4_L7 | func_ZF ]... ''lemma'' <nowiki>func_ZF_4_L7</nowiki>: ''assumes '' $ A \text{ is closed under } f$, $ B \text{ is closed under } f$ '' shows '' $ A\cap B \text{ is closed under } f$ === , +++^[func_ZF_4_L5 | func_ZF ]... ''lemma'' <nowiki>func_ZF_4_L5</nowiki>: ''assumes '' $ A \text{ is closed under } f$ ''and'' $ A\subseteq B$ '' shows '' $ A \text{ is closed under } restrict(f,B\times B)$ ===
''moreover'' ''from '' A2, A3, I ''have'' $ \forall x \in H_1\cap H_2.\ GroupInv(H_1,g)(x) \in H_1\cap H_2$ ''using '' +++^[group0_3_T2 | Group_ZF ]... ''theorem'' ''(in '' group0 '') '' <nowiki>group0_3_T2</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ ''and'' $ g = restrict(P,H\times H)$ '' shows '' $ \forall h\in H.\ GroupInv(H,g)(h) = h^{-1}$ === , +++^[group0_3_T3A | Group_ZF ]... ''theorem'' ''(in '' group0 '') '' <nowiki>group0_3_T3A</nowiki>: ''assumes '' $ IsAsubgroup(H,P)$ ''and'' $ h\in H$ '' shows '' $ h^{-1}\in H$ ===
''ultimately '' ''show'' $ thesis$ ''using '' +++^[group0_3_T3 | Group_ZF ]... ''theorem'' ''(in '' group0 '') '' <nowiki>group0_3_T3</nowiki>: ''assumes '' $ H\neq 0$ ''and'' $ H\subseteq G$ ''and'' $ H \text{ is closed under } P$ ''and'' $ \forall x\in H.\ x^{-1} \in H$ '' shows '' $ IsAsubgroup(H,P)$ ===
''qed'' ===
''end
'' +++![Comments on Group_ZF|click to add comment] <html> <div> <iframe style="width:60%;height:500px" src="http://www.haloscan.com/comments/slawekk/Group_ZF"></iframe> </div> </html>
===