### The Mizar article:

### Subgroup and Cosets of Subgroups

**by****Wojciech A. Trybulec**

- Received July 23, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: GROUP_2
- [ MML identifier index ]

environ vocabulary FINSET_1, REALSET1, RELAT_1, BOOLE, SUBSET_1, VECTSP_1, BINOP_1, GROUP_1, FUNCT_1, RLSUB_1, CARD_1, TARSKI, SETFAM_1, FINSUB_1, SETWISEO, ARYTM_3, GROUP_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, SETFAM_1, FINSUB_1, FINSET_1, STRUCT_0, RLVECT_1, VECTSP_1, WELLORD2, GROUP_1, CARD_1, BINOP_1, SETWISEO, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, NAT_1, MCART_1; constructors WELLORD2, GROUP_1, BINOP_1, SETWISEO, DOMAIN_1, NAT_1, PARTFUN1, MEMBERED, XBOOLE_0; clusters SUBSET_1, FINSET_1, FINSUB_1, GROUP_1, FUNCT_1, STRUCT_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions FUNCT_1, GROUP_1, TARSKI, VECTSP_1, XBOOLE_0; theorems BINOP_1, CARD_1, CARD_2, ENUMSET1, FINSET_1, FINSUB_1, FUNCT_1, FUNCT_2, GROUP_1, NAT_1, SUBSET_1, TARSKI, WELLORD2, ZFMISC_1, VECTSP_1, RLVECT_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes FUNCT_1, SETFAM_1, SETWISEO; begin reserve x for set; reserve G for non empty 1-sorted; reserve A for Subset of G; Lm1: x in A implies x is Element of G; canceled 2; theorem Th3: G is finite implies A is finite proof assume G is finite; then A c= the carrier of G & the carrier of G is finite by GROUP_1:def 13; hence thesis by FINSET_1:13; end; reserve y,y1,y2,Y,Z for set; reserve k for Nat; reserve G for Group; reserve a,g,h for Element of G; reserve A for Subset of G; definition let G,A; func A" -> Subset of G equals :Def1: {g" : g in A}; coherence proof set F = {g" : g in A}; F c= the carrier of G proof let x; assume x in F; then ex g st x = g" & g in A; hence thesis; end; hence thesis; end; end; canceled; theorem Th5: x in A" iff ex g st x = g" & g in A proof thus x in A" implies ex g st x = g" & g in A proof assume x in A"; then x in {g" : g in A} by Def1; hence thesis; end; given g such that A1: x = g" & g in A; x in {h" : h in A} by A1; hence thesis by Def1; end; theorem {g}" = {g"} proof thus {g}" c= {g"} proof let x; assume x in {g}"; then consider h such that A1: x = h" & h in {g} by Th5; h = g by A1,TARSKI:def 1; hence thesis by A1,TARSKI:def 1; end; let x; assume x in {g"}; then x = g" & g in {g} by TARSKI:def 1; hence thesis by Th5; end; theorem {g,h}" = {g",h"} proof thus {g,h}" c= {g",h"} proof let x; assume x in {g,h}"; then consider a such that A1: x = a" & a in {g,h} by Th5; a = g or a = h by A1,TARSKI:def 2; hence thesis by A1,TARSKI:def 2; end; let x; assume x in {g",h"}; then (x = g" or x = h") & g in {g,h} & h in {g,h} by TARSKI:def 2; hence thesis by Th5; end; theorem ({}(the carrier of G))" = {} proof thus ({}(the carrier of G))" c= {} proof let x; assume x in ({}(the carrier of G))"; then consider a such that x = a" and A1: a in {} (the carrier of G) by Th5; thus thesis by A1; end; thus thesis by XBOOLE_1:2; end; theorem ([#](the carrier of G))" = the carrier of G proof thus ([#](the carrier of G))" c= the carrier of G; let x; assume x in the carrier of G; then reconsider a = x as Element of G; a" in the carrier of G; then a" in [#](the carrier of G) by SUBSET_1:def 4; then a"" in ([#](the carrier of G))" by Th5; hence thesis by GROUP_1:19; end; theorem A <> {} iff A" <> {} proof thus A <> {} implies A" <> {} proof assume A1: A <> {}; consider x being Element of A; reconsider x as Element of G by A1,Lm1; x" in A" by A1,Th5; hence thesis; end; assume A2: A" <> {}; consider x being Element of A"; ex a st x = a" & a in A by A2,Th5; hence thesis; end; reserve G for non empty HGrStr,A,B,C for Subset of G; reserve a,b,g,g1,g2,h,h1,h2 for Element of G; definition let G; let A,B; func A * B -> Subset of G equals :Def2: {g * h : g in A & h in B}; coherence proof set S = {g * h : g in A & h in B}; S c= the carrier of G proof let x; assume x in S; then ex g,h st x = g * h & g in A & h in B; hence thesis; end; hence thesis; end; end; canceled; theorem Th12: x in A * B iff ex g,h st x = g * h & g in A & h in B proof thus x in A * B implies ex g,h st x = g * h & g in A & h in B proof assume x in A * B; then x in {g * h : g in A & h in B} by Def2; hence thesis; end; given g,h such that A1: x = g * h & g in A & h in B; x in {g1* g2 : g1 in A & g2 in B} by A1; hence thesis by Def2; end; theorem Th13: A <> {} & B <> {} iff A * B <> {} proof thus A <> {} & B <> {} implies A * B <> {} proof assume A1: A <> {}; consider x being Element of A; reconsider x as Element of G by A1,TARSKI:def 3; assume A2: B <> {}; consider y being Element of B; reconsider y as Element of G by A2,TARSKI:def 3; x * y in A * B by A1,A2,Th12; hence thesis; end; assume A3: A * B <> {}; consider x being Element of A * B; ex a,b st x = a * b & a in A & b in B by A3,Th12; hence thesis; end; theorem Th14: G is associative implies A * B * C = A * (B * C) proof assume A1: G is associative; thus A * B * C c= A * (B * C) proof let x; assume x in A * B * C; then consider g,h such that A2: x = g * h and A3: g in A * B and A4: h in C by Th12; consider g1,g2 such that A5: g = g1 * g2 and A6: g1 in A and A7: g2 in B by A3,Th12; x = g1 * (g2 * h) & g2 * h in B * C by A1,A2,A4,A5,A7,Th12,VECTSP_1:def 16; hence thesis by A6,Th12; end; let x; assume x in A * (B * C); then consider g,h such that A8: x = g * h and A9: g in A and A10: h in B * C by Th12; consider g1,g2 such that A11: h = g1 * g2 and A12: g1 in B and A13: g2 in C by A10,Th12; x = g * g1 * g2 & g * g1 in A * B by A1,A8,A9,A11,A12,Th12,VECTSP_1:def 16; hence thesis by A13,Th12; end; theorem for G being Group, A,B being Subset of G holds (A * B)" = B" * A" proof let G be Group, A,B be Subset of G; thus (A * B)" c= B" * A" proof let x; assume x in (A * B)"; then consider g being Element of G such that A1: x = g" & g in A * B by Th5; consider g1,g2 being Element of G such that A2: g = g1 * g2 & g1 in A & g2 in B by A1,Th12; x = g2" * g1" & g1" in A" & g2" in B" by A1,A2,Th5,GROUP_1:25; hence thesis by Th12; end; let x; assume x in B" * A"; then consider g1,g2 being Element of G such that A3: x = g1 * g2 & g1 in B" & g2 in A" by Th12; consider a being Element of G such that A4: g1 = a" & a in B by A3,Th5; consider b being Element of G such that A5: g2 = b" & b in A by A3,Th5; x = (b * a)" & b * a in A * B by A3,A4,A5,Th12,GROUP_1:25; hence thesis by Th5; end; theorem A * (B \/ C) = A * B \/ A * C proof thus A * (B \/ C) c= A * B \/ A * C proof let x; assume x in A * (B \/ C); then consider g1,g2 such that A1: x = g1 * g2 & g1 in A & g2 in B \/ C by Th12; g2 in B or g2 in C by A1,XBOOLE_0:def 2; then x in A * B or x in A * C by A1,Th12; hence thesis by XBOOLE_0:def 2; end; let x; assume A2: x in A * B \/ A * C; now per cases by A2,XBOOLE_0:def 2; suppose x in A * B; then consider g1,g2 such that A3: x = g1 * g2 & g1 in A & g2 in B by Th12 ; g2 in B \/ C by A3,XBOOLE_0:def 2; hence thesis by A3,Th12; suppose x in A * C; then consider g1,g2 such that A4: x = g1 * g2 & g1 in A & g2 in C by Th12; g2 in B \/ C by A4,XBOOLE_0:def 2; hence thesis by A4,Th12; end; hence thesis; end; theorem (A \/ B) * C = A * C \/ B * C proof thus (A \/ B) * C c= A * C \/ B * C proof let x; assume x in (A \/ B) * C; then consider g1,g2 such that A1: x = g1 * g2 & g1 in A \/ B & g2 in C by Th12; g1 in A or g1 in B by A1,XBOOLE_0:def 2; then x in A * C or x in B * C by A1,Th12; hence thesis by XBOOLE_0:def 2; end; let x; assume A2: x in A * C \/ B * C; now per cases by A2,XBOOLE_0:def 2; suppose x in A * C; then consider g1,g2 such that A3: x = g1 * g2 & g1 in A & g2 in C by Th12; g1 in A \/ B by A3,XBOOLE_0:def 2; hence thesis by A3,Th12; suppose x in B * C; then consider g1,g2 such that A4: x = g1 * g2 & g1 in B & g2 in C by Th12; g1 in A \/ B by A4,XBOOLE_0:def 2; hence thesis by A4,Th12; end; hence thesis; end; theorem A * (B /\ C) c= (A * B) /\ (A * C) proof let x; assume x in A * (B /\ C); then consider g1,g2 such that A1: x = g1 * g2 & g1 in A & g2 in B /\ C by Th12; g2 in B & g2 in C by A1,XBOOLE_0:def 3; then x in A * B & x in A * C by A1,Th12; hence thesis by XBOOLE_0:def 3; end; theorem (A /\ B) * C c= (A * C) /\ (B * C) proof let x; assume x in (A /\ B) * C; then consider g1,g2 such that A1: x = g1 * g2 & g1 in A /\ B & g2 in C by Th12; g1 in A & g1 in B by A1,XBOOLE_0:def 3; then x in A * C & x in B * C by A1,Th12; hence thesis by XBOOLE_0:def 3; end; theorem Th20: {}(the carrier of G) * A = {} & A * {}(the carrier of G) = {} proof A1: now assume A2: {}(the carrier of G) * A <> {}; consider x being Element of {}(the carrier of G) * A; consider g1,g2 such that x = g1 * g2 and A3: g1 in {}(the carrier of G) and g2 in A by A2,Th12; thus contradiction by A3; end; now assume A4: A * {}(the carrier of G) <> {}; consider x being Element of A * {}(the carrier of G); consider g1,g2 such that x = g1 * g2 and g1 in A and A5: g2 in {}(the carrier of G) by A4,Th12; thus contradiction by A5; end; hence thesis by A1; end; theorem Th21: for G being Group, A being Subset of G holds A <> {} implies [#](the carrier of G) * A = the carrier of G & A * [#](the carrier of G) = the carrier of G proof let G be Group, A be Subset of G; set B = [#](the carrier of G); assume A1: A <> {}; thus [#](the carrier of G) * A = the carrier of G proof thus [#](the carrier of G) * A c= the carrier of G; let x; assume x in the carrier of G; then reconsider a = x as Element of G; consider y being Element of A; reconsider y as Element of G by A1,Lm1; A2: (a * y") * y = a * (y" * y) by VECTSP_1:def 16 .= a * 1.G by GROUP_1:def 5 .= a by GROUP_1:def 4; a * y" in the carrier of G; then a * y" in B by SUBSET_1:def 4; hence thesis by A1,A2,Th12; end; thus A * [#](the carrier of G) c= the carrier of G; let x; assume x in the carrier of G; then reconsider a = x as Element of G; consider y being Element of A; reconsider y as Element of G by A1,Lm1; A3: y * (y" * a) = (y * y") * a by VECTSP_1:def 16 .= 1.G * a by GROUP_1:def 5 .= a by GROUP_1:def 4; y" * a in the carrier of G; then y" * a in B by SUBSET_1:def 4; hence thesis by A1,A3,Th12; end; theorem Th22: {g} * {h} = {g * h} proof thus {g} * {h} c= {g * h} proof let x; assume x in {g} * {h}; then consider g1,g2 such that A1: x = g1 * g2 and A2: g1 in {g} & g2 in {h} by Th12; g1 = g & g2 = h by A2,TARSKI:def 1; hence thesis by A1,TARSKI:def 1; end; let x; assume x in {g * h}; then x = g * h & g in {g} & h in {h} by TARSKI:def 1; hence thesis by Th12; end; theorem {g} * {g1,g2} = {g * g1,g * g2} proof thus {g} * {g1,g2} c= {g * g1,g * g2} proof let x; assume x in {g} * {g1,g2}; then consider h1,h2 such that A1: x = h1 * h2 and A2: h1 in {g} & h2 in {g1,g2} by Th12; h1 = g & (h2 = g1 or h2 = g2) by A2,TARSKI:def 1,def 2; hence thesis by A1,TARSKI:def 2; end; let x; assume x in {g * g1,g * g2}; then (x = g * g1 or x = g * g2) & g in {g} & g1 in {g1,g2} & g2 in {g1,g2 } by TARSKI:def 1,def 2; hence thesis by Th12; end; theorem {g1,g2} * {g} = {g1 * g,g2 * g} proof thus {g1,g2} * {g} c= {g1 * g,g2 * g} proof let x; assume x in {g1,g2} * {g}; then consider h1,h2 such that A1: x = h1 * h2 and A2: h1 in {g1,g2} & h2 in {g} by Th12; h2 = g & (h1 = g1 or h1 = g2) by A2,TARSKI:def 1,def 2; hence thesis by A1,TARSKI:def 2; end; let x; assume x in {g1 * g,g2 * g}; then (x = g1 * g or x = g2 * g) & g in {g} & g1 in {g1,g2} & g2 in {g1,g2 } by TARSKI:def 1,def 2; hence thesis by Th12; end; theorem {g,h} * {g1,g2} = {g * g1, g * g2, h * g1, h * g2} proof set A = {g,h} * {g1,g2}; set B = {g * g1, g * g2, h * g1, h * g2}; thus A c= B proof let x; assume x in A; then consider h1,h2 such that A1: x = h1 * h2 and A2: h1 in {g,h} & h2 in {g1,g2} by Th12; (h1 = g or h1 = h) & (h2 = g1 or h2 = g2) by A2,TARSKI:def 2; hence thesis by A1,ENUMSET1:19; end; let x; assume x in B; then (x = g * g1 or x = g * g2 or x = h * g1 or x = h * g2) & g in {g,h} & h in {g,h} & g1 in {g1,g2} & g2 in {g1,g2} by ENUMSET1:18,TARSKI:def 2; hence thesis by Th12; end; theorem Th26: for G being Group, A being Subset of G holds (for g1,g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A) & (for g being Element of G st g in A holds g" in A) implies A * A = A proof let G be Group, A be Subset of G such that A1: for g1,g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A and A2: for g being Element of G st g in A holds g" in A; thus A * A c= A proof let x; assume x in A * A; then ex g1,g2 being Element of G st x = g1 * g2 & g1 in A & g2 in A by Th12; hence thesis by A1; end; let x; assume A3: x in A; then reconsider a = x as Element of G; a" in A by A2,A3; then a" * a in A by A1,A3; then 1.G in A & 1.G * a = a by GROUP_1:def 4,def 5; hence thesis by A3,Th12; end; theorem Th27: for G being Group, A being Subset of G holds (for g being Element of G st g in A holds g" in A) implies A" = A proof let G be Group, A be Subset of G; assume A1: for g being Element of G st g in A holds g" in A; thus A" c= A proof let x; assume x in A"; then ex g being Element of G st x = g" & g in A by Th5; hence thesis by A1; end; let x; assume A2: x in A; then reconsider a = x as Element of G; a" in A & x = a"" by A1,A2,GROUP_1:19; hence thesis by Th5; end; theorem (for a,b st a in A & b in B holds a * b = b * a) implies A * B = B * A proof assume A1: for a,b st a in A & b in B holds a * b = b * a; thus A * B c= B * A proof let x; assume x in A * B; then consider a,b such that A2: x = a * b & a in A & b in B by Th12; x = b * a by A1,A2; hence thesis by A2,Th12; end; let x; assume x in B * A; then consider b,a such that A3: x = b * a & b in B & a in A by Th12; x = a * b by A1,A3; hence thesis by A3,Th12; end; Lm2: for A be commutative Group, a, b be Element of A holds a * b = b * a; theorem Th29: G is commutative Group implies A * B = B * A proof assume A1: G is commutative Group; thus A * B c= B * A proof let x; assume x in A * B; then consider g,h such that A2: x = g * h and A3: g in A & h in B by Th12; x = h * g by A1,A2,Lm2; hence thesis by A3,Th12; end; let x; assume x in B * A; then consider g,h such that A4: x = g * h and A5: g in B & h in A by Th12; x = h * g by A1,A4,Lm2; hence thesis by A5,Th12; end; theorem for G being commutative Group, A,B being Subset of G holds (A * B)" = A" * B" proof let G be commutative Group, A,B be Subset of G; thus (A * B)" c= A" * B" proof let x; assume x in (A * B)"; then consider g being Element of G such that A1: x = g" & g in A * B by Th5; consider g1,g2 being Element of G such that A2: g = g1 * g2 & g1 in A & g2 in B by A1,Th12; x = g1" * g2" & g1" in A" & g2" in B" by A1,A2,Th5,GROUP_1:94; hence thesis by Th12; end; let x; assume x in A" * B"; then consider g1,g2 being Element of G such that A3: x = g1 * g2 & g1 in A" & g2 in B" by Th12; consider a being Element of G such that A4: g1 = a" & a in A by A3,Th5; consider b being Element of G such that A5: g2 = b" & b in B by A3,Th5; x = (a * b)" & a * b in A * B by A3,A4,A5,Th12,GROUP_1:94; hence thesis by Th5; end; definition let G,g,A; func g * A -> Subset of G equals :Def3: {g} * A; correctness; func A * g -> Subset of G equals :Def4: A * {g}; correctness; end; canceled 2; theorem Th33: x in g * A iff ex h st x = g * h & h in A proof thus x in g * A implies ex h st x = g * h & h in A proof assume x in g * A; then x in {g} * A by Def3; then consider g1,g2 such that A1: x = g1 * g2 & g1 in {g} & g2 in A by Th12; g1 = g by A1,TARSKI:def 1; hence thesis by A1; end; given h such that A2: x = g * h & h in A; g in {g} by TARSKI:def 1; then x in {g} * A by A2,Th12; hence thesis by Def3; end; theorem Th34: x in A * g iff ex h st x = h * g & h in A proof thus x in A * g implies ex h st x = h * g & h in A proof assume x in A * g; then x in A * {g} by Def4; then consider g1,g2 such that A1: x = g1 * g2 & g1 in A & g2 in {g} by Th12; g2 = g by A1,TARSKI:def 1; hence thesis by A1; end; given h such that A2: x = h * g & h in A; g in {g} by TARSKI:def 1; then x in A * {g} by A2,Th12; hence thesis by Def4; end; theorem G is associative implies g * A * B = g * (A * B) proof assume A1: G is associative; thus g * A * B = {g} * A * B by Def3 .= {g} * (A * B) by A1,Th14 .= g * (A * B) by Def3; end; theorem G is associative implies A * g * B = A * (g * B) proof assume A1: G is associative; thus A * g * B = A * {g} * B by Def4 .= A *({g} * B) by A1,Th14 .= A * (g * B) by Def3; end; theorem G is associative implies A * B * g = A * (B * g) proof assume A1: G is associative; thus A * B * g = A * B * {g} by Def4 .= A * (B * {g}) by A1,Th14 .= A * (B * g) by Def4; end; theorem Th38: G is associative implies g * h * A = g * (h * A) proof assume A1: G is associative; thus g * h * A = {g * h} * A by Def3 .= {g} * {h} * A by Th22 .= {g} * ({h} * A) by A1,Th14 .= g * ({h} * A) by Def3 .= g * (h * A) by Def3; end; theorem Th39: G is associative implies g * A * h = g * (A * h) proof assume A1: G is associative; thus g * A * h = g * A * {h} by Def4 .= {g} * A * {h} by Def3 .= {g} * (A * {h}) by A1,Th14 .= g * (A * {h}) by Def3 .= g * (A * h) by Def4; end; theorem Th40: G is associative implies A * g * h = A * (g * h) proof assume A1: G is associative; thus A * g * h = A * g * {h} by Def4 .= A * {g} * {h} by Def4 .= A * ({g} * {h}) by A1,Th14 .= A * {g * h} by Th22 .= A * (g * h) by Def4; end; theorem {}(the carrier of G) * a = {} & a * {}(the carrier of G) = {} proof {}(the carrier of G) * a = {}(the carrier of G) * {a} & a * {}(the carrier of G) = {a} * {}(the carrier of G) by Def3,Def4; hence thesis by Th20; end; reserve G for Group-like (non empty HGrStr); reserve h,g,g1,g2 for Element of G; reserve A for Subset of G; theorem Th42: for G being Group, a being Element of G holds [#](the carrier of G) * a = the carrier of G & a * [#](the carrier of G) = the carrier of G proof let G be Group, a be Element of G; [#](the carrier of G) * a = [#](the carrier of G) * {a} & a * [#](the carrier of G) = {a} * [#](the carrier of G) & {a} <> {} by Def3,Def4; hence thesis by Th21; end; theorem Th43: 1.G * A = A & A * 1.G = A proof thus 1.G * A = A proof thus 1.G * A c= A proof let x; assume x in 1.G * A; then ex h st x = 1.G * h & h in A by Th33; hence thesis by GROUP_1:def 4; end; let x; assume A1: x in A; then reconsider a = x as Element of G; 1.G * a = a by GROUP_1:def 4; hence thesis by A1,Th33; end; thus A * 1.G c= A proof let x; assume x in A * 1.G; then ex h st x = h * 1.G & h in A by Th34; hence thesis by GROUP_1:def 4; end; let x; assume A2: x in A; then reconsider a = x as Element of G; a * 1.G = a by GROUP_1:def 4; hence thesis by A2,Th34; end; theorem Th44: G is commutative Group implies g * A = A * g proof assume A1: G is commutative Group; thus g * A = {g} * A by Def3 .= A * {g} by A1,Th29 .= A * g by Def4; end; definition let G be Group-like (non empty HGrStr); mode Subgroup of G -> Group-like (non empty HGrStr) means :Def5: the carrier of it c= the carrier of G & the mult of it = (the mult of G) | [:the carrier of it,the carrier of it:]; existence proof take G; dom(the mult of G) = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1; hence thesis by RELAT_1:97; end; end; reserve H for Subgroup of G; reserve h,h1,h2 for Element of H; canceled 3; theorem Th48: G is finite implies H is finite proof assume G is finite; then the carrier of H c= the carrier of G & the carrier of G is finite by Def5,GROUP_1:def 13; hence the carrier of H is finite by FINSET_1:13; end; theorem Th49: x in H implies x in G proof assume x in H; then x in the carrier of H & the carrier of H c= the carrier of G by Def5,RLVECT_1:def 1; hence thesis by RLVECT_1:def 1; end; theorem Th50: h in G proof h in H by RLVECT_1:def 1; hence thesis by Th49; end; theorem Th51: h is Element of G proof h in G by Th50; hence thesis by RLVECT_1:def 1; end; theorem Th52: h1 = g1 & h2 = g2 implies h1 * h2 = g1 * g2 proof assume A1: h1 = g1 & h2 = g2; set A = [:the carrier of H,the carrier of H:]; A2: h1 * h2 = (the mult of H).(h1,h2) by VECTSP_1:def 10 .= ((the mult of G) | A).(h1,h2) by Def5 .= ((the mult of G) | A).[h1,h2] by BINOP_1:def 1; g1 * g2 = (the mult of G).(g1,g2) by VECTSP_1:def 10 .= (the mult of G).[g1,g2] by BINOP_1:def 1; hence thesis by A1,A2,FUNCT_1:72; end; definition let G be Group; cluster -> associative Subgroup of G; coherence proof let H be Subgroup of G; let x, y, z be Element of H; A1: x in the carrier of H & y in the carrier of H & z in the carrier of H & x*y in the carrier of H & y*z in the carrier of H; the carrier of H c= the carrier of G by Def5; then reconsider a = x, b = y, c = z, ab = x*y, bc = y*z as Element of G by A1; thus x*y*z = ab*c by Th52 .= a*b*c by Th52 .= a*(b*c) by VECTSP_1:def 16 .= a*bc by Th52 .= x*(y*z) by Th52; end; end; reserve G,G1,G2,G3 for Group; reserve a,a1,a2,b,b1,b2,g,g1,g2 for Element of G; reserve A,B for Subset of G; reserve I,H,H1,H2,H3 for Subgroup of G; reserve h,h1,h2 for Element of H; theorem Th53: 1.H = 1.G proof consider h; reconsider g = h, g' = 1.H as Element of G by Th51; h * 1.H = h by GROUP_1:def 4; then g * g' = g by Th52; hence thesis by GROUP_1:15; end; theorem 1.H1 = 1.H2 proof thus 1.H1 = 1.G by Th53 .= 1.H2 by Th53; end; theorem Th55: 1.G in H proof 1.H in H by RLVECT_1:def 1; hence thesis by Th53; end; theorem 1.H1 in H2 proof 1.H1 = 1.G by Th53; hence thesis by Th55; end; theorem Th57: h = g implies h" = g" proof assume A1: h = g; reconsider g' = h" as Element of G by Th51; h * h" = 1.H by GROUP_1:def 5; then g * g' = 1.H by A1,Th52 .= 1.G by Th53; hence thesis by GROUP_1:20; end; theorem inverse_op(H) = inverse_op(G) | the carrier of H proof A1: dom(inverse_op(H)) = the carrier of H & dom(inverse_op(G)) = the carrier of G & the carrier of H c= the carrier of G by Def5,FUNCT_2:def 1; then A2: (the carrier of G) /\ (the carrier of H) = the carrier of H by XBOOLE_1: 28; now let x; assume x in dom(inverse_op(H)); then reconsider a = x as Element of H; reconsider b = a as Element of G by Th51; thus inverse_op(H).x = a" by GROUP_1:def 6 .= b" by Th57 .= inverse_op(G).x by GROUP_1:def 6; end; hence thesis by A1,A2,FUNCT_1:68; end; theorem Th59: g1 in H & g2 in H implies g1 * g2 in H proof assume g1 in H & g2 in H; then reconsider h1 = g1, h2 = g2 as Element of H by RLVECT_1:def 1; h1 * h2 in H by RLVECT_1:def 1; hence thesis by Th52; end; theorem Th60: g in H implies g" in H proof assume g in H; then reconsider h = g as Element of H by RLVECT_1:def 1; h" in H by RLVECT_1:def 1; hence thesis by Th57; end; definition let G; cluster strict Subgroup of G; existence proof set H = HGrStr (#the carrier of G, the mult of G#); A1: now let g1,g2 be Element of G; let h1,h2 be Element of H; assume A2: g1 = h1 & g2 = h2; A3: h1 * h2 = (the mult of G).(h1,h2) by VECTSP_1:def 10 .= (the mult of G).[h1,h2] by BINOP_1:def 1; g1 * g2 = (the mult of G).(g1,g2) by VECTSP_1:def 10 .= (the mult of G).[g1,g2] by BINOP_1:def 1; hence g1 * g2 = h1 * h2 by A2,A3; end; H is Group-like proof reconsider t = 1.G as Element of H; take t; let a be Element of H; reconsider x = a as Element of G; thus a * t = x * 1.G by A1 .= a by GROUP_1:def 4; thus t * a = 1.G * x by A1 .= a by GROUP_1:def 4; reconsider s = x" as Element of H; take s; thus a * s = x * x" by A1 .= t by GROUP_1:def 5; thus s * a = x" * x by A1 .= t by GROUP_1:def 5; end; then reconsider H as Group-like (non empty HGrStr); the mult of H = (the mult of G) | [:the carrier of H,the carrier of H:] by FUNCT_2:40; then H is Subgroup of G by Def5; hence thesis; end; end; theorem Th61: A <> {} & (for g1,g2 st g1 in A & g2 in A holds g1 * g2 in A) & (for g st g in A holds g" in A) implies ex H being strict Subgroup of G st the carrier of H = A proof assume that A1: A <> {} and A2: for g1,g2 st g1 in A & g2 in A holds g1 * g2 in A and A3: for g st g in A holds g" in A; reconsider D = A as non empty set by A1; set o = (the mult of G) | [:A,A:]; dom o = dom(the mult of G) /\ [:A,A:] & dom(the mult of G) = [:the carrier of G,the carrier of G:] & [:A,A:] c= [:the carrier of G,the carrier of G:] by FUNCT_2:def 1,RELAT_1:90; then A4: dom o = [:A,A:] by XBOOLE_1:28; rng o c= A proof let x; assume x in rng o; then consider y such that A5: y in dom o and A6: o.y = x by FUNCT_1:def 5; consider y1,y2 such that A7: [y1,y2] = y by A5,ZFMISC_1:102; A8: y1 in A & y2 in A by A4,A5,A7,ZFMISC_1:106; reconsider y1,y2 as Element of G by A5,A7,ZFMISC_1:106 ; x = (the mult of G).y by A5,A6,FUNCT_1:70 .= (the mult of G).(y1,y2) by A7,BINOP_1:def 1 .= y1 * y2 by VECTSP_1:def 10; hence thesis by A2,A8; end; then reconsider o as BinOp of D by A4,FUNCT_2:def 1,RELSET_1:11; set H = HGrStr (# D,o #); A9: now let g1,g2; let h1,h2 be Element of H; assume A10: g1 = h1 & g2 = h2; A11: h1 * h2 = ((the mult of G) | [:A,A:]).(h1,h2) by VECTSP_1:def 10 .= ((the mult of G) | [:A,A:]).[h1,h2] by BINOP_1:def 1; g1 * g2 = (the mult of G).(g1,g2) by VECTSP_1:def 10 .= (the mult of G).[g1,g2] by BINOP_1:def 1; hence g1 * g2 = h1 * h2 by A10,A11,FUNCT_1:72; end; H is Group-like proof consider a being Element of H; reconsider x = a as Element of G by Lm1; x" in A by A3; then x * x" in A by A2; then reconsider t = 1.G as Element of H by GROUP_1:def 5; take t; let a be Element of H; reconsider x = a as Element of G by Lm1; thus a * t = x * 1.G by A9 .= a by GROUP_1:def 4; thus t * a = 1.G * x by A9 .= a by GROUP_1:def 4; reconsider s = x" as Element of H by A3; take s; thus a * s = x * x" by A9 .= t by GROUP_1:def 5; thus s * a = x" * x by A9 .= t by GROUP_1:def 5; end; then reconsider H as Group-like (non empty HGrStr); reconsider H as strict Subgroup of G by Def5; take H; thus thesis; end; theorem Th62: G is commutative Group implies H is commutative proof assume A1: G is commutative Group; thus for h1,h2 holds h1 * h2 = h2 * h1 proof let h1,h2; reconsider g1 = h1, g2 = h2 as Element of G by Th51; thus h1 * h2 = g1 * g2 by Th52 .= g2 * g1 by A1,Lm2 .= h2 * h1 by Th52; end; end; definition let G be commutative Group; cluster -> commutative Subgroup of G; coherence by Th62; end; theorem Th63: G is Subgroup of G proof dom(the mult of G) = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1; hence the carrier of G c= the carrier of G & the mult of G = (the mult of G) | [:the carrier of G,the carrier of G:] by RELAT_1:97; end; theorem Th64: G1 is Subgroup of G2 & G2 is Subgroup of G1 implies the HGrStr of G1 = the HGrStr of G2 proof assume that A1: G1 is Subgroup of G2 and A2: G2 is Subgroup of G1; set A = the carrier of G1; set B = the carrier of G2; set f = the mult of G1; set g = the mult of G2; A3: A c= B & B c= A by A1,A2,Def5; then A4: A = B by XBOOLE_0:def 10; f = g | [:A,A:] by A1,Def5 .= (f | [:B,B:]) | [:A,A:] by A2,Def5 .= f | [:B,B:] by A4,RELAT_1:101 .= g by A2,Def5; hence thesis by A3,XBOOLE_0:def 10; end; theorem Th65: G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3 proof assume that A1: G1 is Subgroup of G2 and A2: G2 is Subgroup of G3; set A = the carrier of G1; set B = the carrier of G2; set C = the carrier of G3; set h = the mult of G3; A3: A c= B & B c= C by A1,A2,Def5; then A4: A c= C by XBOOLE_1:1; A5: [:A,A:] c= [:B,B:] by A3,ZFMISC_1:119; the mult of G1 = (the mult of G2) | [:A,A:] by A1,Def5 .= (h | [:B,B:]) | [:A,A:] by A2,Def5 .= h | [:A,A:] by A5,FUNCT_1:82; hence thesis by A4,Def5; end; theorem Th66: the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2 proof set A = the carrier of H1; set B = the carrier of H2; set h = the mult of G; assume A1:the carrier of H1 c= the carrier of H2; hence the carrier of H1 c= the carrier of H2; the mult of H1 = h | [:A,A:] & the mult of H2 = h | [:B,B:] & [:A,A:] c= [:B,B:] by A1,Def5,ZFMISC_1:119; hence thesis by FUNCT_1:82; end; theorem Th67: (for g st g in H1 holds g in H2) implies H1 is Subgroup of H2 proof assume A1: for g st g in H1 holds g in H2; the carrier of H1 c= the carrier of H2 proof let x; assume x in the carrier of H1; then reconsider g = x as Element of H1; reconsider g as Element of G by Th51; g in H1 by RLVECT_1:def 1; then g in H2 by A1; hence thesis by RLVECT_1:def 1; end; hence thesis by Th66; end; theorem Th68: the carrier of H1 = the carrier of H2 implies the HGrStr of H1 = the HGrStr of H2 proof assume the carrier of H1 = the carrier of H2; then H1 is Subgroup of H2 & H2 is Subgroup of H1 by Th66; hence thesis by Th64; end; theorem Th69: (for g holds g in H1 iff g in H2) implies the HGrStr of H1 = the HGrStr of H2 proof assume for g holds g in H1 iff g in H2; then H1 is Subgroup of H2 & H2 is Subgroup of H1 by Th67; hence thesis by Th64; end; definition let G; let H1,H2 be strict Subgroup of G; redefine pred H1 = H2 means for g holds g in H1 iff g in H2; compatibility by Th69; end; theorem Th70: for G being strict Group, H being strict Subgroup of G holds the carrier of H = the carrier of G implies H = G proof let G be strict Group, H be strict Subgroup of G; G is Subgroup of G by Th63; hence thesis by Th68; end; theorem Th71: (for g being Element of G holds g in H) implies the HGrStr of H = the HGrStr of G proof assume for g being Element of G holds g in H; then A1: for g be Element of G holds ( g in H implies g in G) &( g in G implies g in H) by RLVECT_1:def 1; G is Subgroup of G by Th63; hence thesis by A1,Th69; end; definition let G; func (1).G -> strict Subgroup of G means :Def7: the carrier of it = {1.G}; existence proof A1: now let g1,g2; assume g1 in {1.G} & g2 in {1.G}; then g1 = 1.G & g2 = 1.G by TARSKI:def 1; then g1 * g2 = 1.G by GROUP_1:def 4; hence g1 * g2 in {1.G} by TARSKI:def 1; end; now let g; assume g in {1.G}; then g = 1.G by TARSKI:def 1; then g" = 1.G by GROUP_1:16; hence g" in {1.G} by TARSKI:def 1; end; hence thesis by A1,Th61; end; uniqueness by Th68; end; definition let G; func (Omega).G -> strict Subgroup of G equals :Def8: the HGrStr of G; coherence proof set H = the HGrStr of G; H is Group-like proof A1: now let f,g be Element of H, f',g' be Element of G such that A2: f = f' & g = g'; thus f * g = (the mult of H).(f,g) by VECTSP_1:def 10 .= f' * g' by A2,VECTSP_1:def 10; end; consider e' being Element of G such that A3: for h being Element of G holds h * e' = h & e' * h = h & ex g being Element of G st h * g = e' & g * h = e' by GROUP_1:def 3; reconsider e = e' as Element of H; take e; let h be Element of H; reconsider h' = h as Element of G; h' * e' = h' & e' * h' = h' by A3; hence h * e = h & e * h = h by A1; consider g' being Element of G such that A4: h' * g' = e' & g' * h' = e' by A3; reconsider g = g' as Element of H; take g; thus h * g = e & g * h = e by A1,A4; end; then reconsider H as Group-like (non empty HGrStr); H is Subgroup of G proof thus the carrier of H c= the carrier of G; dom(the mult of G) = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1; hence the mult of H = (the mult of G) | [:the carrier of H,the carrier of H:] by RELAT_1:97; end; hence thesis; end; end; canceled 3; theorem Th75: (1).H = (1).G proof (1).H is Subgroup of G & the carrier of (1).H = {1.H} & the carrier of (1).G = {1.G} & 1.H = 1.G by Def7,Th53,Th65; hence thesis by Th68; end; theorem (1).H1 = (1).H2 proof thus (1).H1 = (1).G by Th75 .= (1).H2 by Th75; end; theorem Th77: (1).G is Subgroup of H proof (1).G = (1).H by Th75; hence thesis; end; theorem Th78: for G being strict Group, H being Subgroup of G holds H is Subgroup of (Omega).G by Def8; theorem for G being strict Group holds G is Subgroup of (Omega).G proof let G be strict Group; G is Subgroup of G by Th63; hence thesis by Def8; end; theorem Th80: (1).G is finite proof the carrier of (1).G = {1.G} & {1.G} is finite by Def7; hence thesis by GROUP_1:def 13; end; definition let X be non empty set; cluster finite non empty Subset of X; existence proof consider x being Element of X; take {x}; thus thesis; end; end; theorem Th81: ord (1).G = 1 proof (1).G is finite & the carrier of (1).G = {1.G} & card{1.G} = 1 by Def7,Th80,CARD_1:79; hence thesis by GROUP_1:def 14; end; theorem Th82: for H being strict Subgroup of G holds H is finite & ord H = 1 implies H = (1).G proof let H be strict Subgroup of G; assume H is finite; then consider B being finite set such that A1: B = the carrier of H & ord H = card B by GROUP_1:def 14; assume ord H = 1; then consider x such that A2: the carrier of H = {x} by A1,CARD_2:60; 1.G in H by Th55; then 1.G in the carrier of H by RLVECT_1:def 1; then x = 1.G by A2,TARSKI:def 1; hence thesis by A2,Def7; end; theorem Ord H <=` Ord G proof the carrier of H c= the carrier of G & Ord H = Card(the carrier of H) & Ord G = Card(the carrier of G) by Def5,GROUP_1:def 12; hence thesis by CARD_1:27; end; theorem G is finite implies ord H <= ord G proof assume A1: G is finite; then H is finite by Th48; then consider C being finite set such that A2: C = the carrier of H & ord H = card C by GROUP_1:def 14; consider B being finite set such that A3: B = the carrier of G & ord G = card B by A1,GROUP_1:def 14; the carrier of H c= the carrier of G by Def5; hence thesis by A2,A3,CARD_1:80; end; theorem for G being strict Group, H being strict Subgroup of G holds G is finite & ord G = ord H implies H = G proof let G be strict Group, H be strict Subgroup of G; assume that A1: G is finite and A2: ord G = ord H; A3: H is finite by A1,Th48; consider B being finite set such that A4: B = the carrier of G & ord G = card B by A1,GROUP_1:def 14; consider C being finite set such that A5: C = the carrier of H & ord H = card C by A3,GROUP_1:def 14; A6: the carrier of H c= the carrier of G by Def5; the carrier of H = the carrier of G proof assume the carrier of H <> the carrier of G; then the carrier of H c< the carrier of G by A6,XBOOLE_0:def 8; hence thesis by A2,A4,A5,CARD_2:67; end; hence thesis by Th70; end; definition let G,H; func carr(H) -> Subset of G equals :Def9: the carrier of H; coherence by Def5; end; canceled; theorem Th87: carr(H) <> {} proof the carrier of H <> {}; hence thesis by Def9; end; theorem Th88: x in carr(H) iff x in H proof (x in carr(H) iff x in the carrier of H) & (x in H iff x in the carrier of H) by Def9,RLVECT_1:def 1; hence thesis; end; theorem Th89: g1 in carr(H) & g2 in carr(H) implies g1 * g2 in carr(H) proof assume g1 in carr(H) & g2 in carr(H); then g1 in H & g2 in H by Th88; then g1 * g2 in H by Th59; hence thesis by Th88; end; theorem Th90: g in carr(H) implies g" in carr(H) proof assume g in carr(H); then g in H by Th88; then g" in H by Th60; hence thesis by Th88; end; theorem carr(H) * carr(H) = carr(H) proof A1: g1 in carr(H) & g2 in carr(H) implies g1 * g2 in carr(H) by Th89; g in carr(H) implies g" in carr(H) by Th90; hence thesis by A1,Th26; end; theorem carr(H)" = carr H proof g in carr H implies g" in carr H by Th90; hence thesis by Th27; end; theorem Th93: (carr H1 * carr H2 = carr H2 * carr H1 implies ex H being strict Subgroup of G st the carrier of H = carr H1 * carr H2) & ((ex H st the carrier of H = carr H1 * carr H2) implies carr H1 * carr H2 = carr H2 * carr H1) proof thus carr(H1) * carr(H2) = carr(H2) * carr(H1) implies ex H being strict Subgroup of G st the carrier of H = carr(H1) * carr(H2) proof assume A1: carr H1 * carr H2 = carr H2 * carr H1; carr H1 <> {} & carr H2 <> {} by Th87; then A2: carr H1 * carr H2 <> {} by Th13; A3: now let g1,g2; assume that A4: g1 in carr(H1) * carr(H2) and A5: g2 in carr(H1) * carr(H2); consider a1,b1 such that A6: g1 = a1 * b1 & a1 in carr(H1) & b1 in carr(H2) by A4,Th12; consider a2,b2 such that A7: g2 = a2 * b2 & a2 in carr H1 & b2 in carr H2 by A5,Th12; A8: g1 * g2 = a1 * b1 * a2 * b2 by A6,A7,VECTSP_1:def 16 .= a1 * (b1 * a2) * b2 by VECTSP_1:def 16; b1 * a2 in carr H1 * carr H2 by A1,A6,A7,Th12; then consider a,b such that A9: b1 * a2 = a * b & a in carr H1 & b in carr H2 by Th12; A10: g1 * g2 = a1 * a * b * b2 by A8,A9,VECTSP_1:def 16 .= a1 * a * (b * b2) by VECTSP_1:def 16; a1 * a in carr H1 & b * b2 in carr H2 by A6,A7,A9,Th89; hence g1 * g2 in carr H1 * carr H2 by A10,Th12; end; now let g; assume A11: g in carr H1 * carr H2; then consider a,b such that A12: g = a * b & a in carr H1 & b in carr H2 by Th12; consider b1,a1 such that A13: a * b = b1 * a1 & b1 in carr H2 & a1 in carr H1 by A1,A11,A12,Th12 ; A14: g" = a1" * b1" by A12,A13,GROUP_1:25; a1" in carr H1 & b1" in carr H2 by A13,Th90; hence g" in carr H1 * carr H2 by A14,Th12; end; hence thesis by A2,A3,Th61; end; given H such that A15: the carrier of H = carr H1 * carr H2; thus carr H1 * carr H2 c= carr H2 * carr H1 proof let x; assume A16: x in carr H1 * carr H2; then reconsider y = x as Element of G; x in carr H by A15,A16,Def9; then y" in carr H by Th90; then y" in carr H1 * carr H2 by A15,Def9; then consider a,b such that A17: y" = a * b & a in carr H1 & b in carr H2 by Th12; A18: y = y"" by GROUP_1:19 .= b" * a" by A17,GROUP_1:25; a" in carr H1 & b" in carr H2 by A17,Th90; hence thesis by A18,Th12; end; let x; assume A19: x in carr H2 * carr H1; then reconsider y = x as Element of G; consider a,b such that A20: x = a * b & a in carr H2 & b in carr H1 by A19,Th12; now assume not y" in carr H; then A21: not y" in the carrier of H by Def9; y" = b" * a" & a" in carr H2 & b" in carr H1 by A20,Th90,GROUP_1:25; hence contradiction by A15,A21,Th12; end; then y"" in carr H by Th90; then x in carr H by GROUP_1:19; hence thesis by A15,Def9; end; theorem G is commutative Group implies ex H being strict Subgroup of G st the carrier of H = carr(H1) * carr(H2) proof assume G is commutative Group; then carr(H1) * carr(H2) = carr(H2) * carr(H1) by Th29; hence thesis by Th93; end; definition let G,H1,H2; func H1 /\ H2 -> strict Subgroup of G means :Def10: the carrier of it = carr(H1) /\ carr(H2); existence proof set A = carr(H1) /\ carr(H2); 1.G in H1 & 1.G in H2 by Th55; then 1.G in the carrier of H1 & 1.G in the carrier of H2 by RLVECT_1:def 1 ; then 1.G in carr(H1) & 1.G in carr(H2) by Def9; then A1: A <> {} by XBOOLE_0:def 3; A2: now let g1,g2; assume g1 in A & g2 in A; then g1 in carr(H1) & g2 in carr(H1) & g1 in carr(H2) & g2 in carr(H2) by XBOOLE_0:def 3; then g1 * g2 in carr(H1) & g1 * g2 in carr(H2) by Th89; hence g1 * g2 in A by XBOOLE_0:def 3; end; now let g; assume g in A; then g in carr(H1) & g in carr(H2) by XBOOLE_0:def 3; then g" in carr(H1) & g" in carr(H2) by Th90; hence g" in A by XBOOLE_0:def 3; end; hence thesis by A1,A2,Th61; end; uniqueness by Th68; end; canceled 2; theorem Th97: (for H being Subgroup of G st H = H1 /\ H2 holds the carrier of H = (the carrier of H1) /\ (the carrier of H2)) & for H being strict Subgroup of G holds the carrier of H = (the carrier of H1) /\ (the carrier of H2) implies H = H1 /\ H2 proof thus for H being Subgroup of G st H = H1 /\ H2 holds the carrier of H = (the carrier of H1) /\ (the carrier of H2) proof let H be Subgroup of G; assume H = H1 /\ H2; hence the carrier of H = carr(H1) /\ carr(H2) by Def10 .= (the carrier of H1) /\ carr(H2) by Def9 .= (the carrier of H1) /\ (the carrier of H2) by Def9 ; end; let H be strict Subgroup of G; assume A1: the carrier of H = (the carrier of H1) /\ (the carrier of H2); the carrier of H1 = carr(H1) & the carrier of H2 = carr(H2) by Def9; hence thesis by A1,Def10; end; theorem Th98: carr(H1 /\ H2) = carr(H1) /\ carr(H2) proof thus carr(H1 /\ H2) = the carrier of H1 /\ H2 by Def9 .= carr(H1) /\ carr(H2) by Def10; end; theorem Th99: x in H1 /\ H2 iff x in H1 & x in H2 proof thus x in H1 /\ H2 implies x in H1 & x in H2 proof assume x in H1 /\ H2; then x in the carrier of H1 /\ H2 by RLVECT_1:def 1; then x in carr(H1) /\ carr(H2) by Def10; then x in carr(H1) & x in carr(H2) by XBOOLE_0:def 3; hence thesis by Th88; end; assume x in H1 & x in H2; then x in carr(H2) & x in carr(H1) by Th88; then x in carr(H1) /\ carr(H2) by XBOOLE_0:def 3; then x in carr(H1 /\ H2) by Th98; hence thesis by Th88; end; theorem for H being strict Subgroup of G holds H /\ H = H proof let H be strict Subgroup of G; the carrier of H /\ H = carr(H) /\ carr(H) by Def10 .= the carrier of H by Def9; hence thesis by Th68; end; theorem Th101: H1 /\ H2 = H2 /\ H1 proof the carrier of H1 /\ H2 = carr(H2) /\ carr(H1) by Def10 .= the carrier of H2 /\ H1 by Def10; hence thesis by Th68; end; definition let G,H1,H2; redefine func H1 /\ H2; commutativity by Th101; end; theorem H1 /\ H2 /\ H3 = H1 /\ (H2 /\ H3) proof the carrier of H1 /\ H2 /\ H3 = carr(H1 /\ H2) /\ carr(H3) by Def10 .= (the carrier of H1 /\ H2) /\ carr(H3) by Def9 .= carr(H1) /\ carr(H2) /\ carr(H3) by Def10 .= carr(H1) /\ (carr(H2) /\ carr(H3)) by XBOOLE_1:16 .= carr(H1) /\ (the carrier of H2 /\ H3) by Def10 .= carr(H1) /\ carr(H2 /\ H3) by Def9 .= the carrier of H1 /\ (H2 /\ H3) by Def10; hence thesis by Th68; end; Lm3: for H1 being strict Subgroup of G holds H1 is Subgroup of H2 iff H1 /\ H2 = H1 proof let H1 be strict Subgroup of G; thus H1 is Subgroup of H2 implies H1 /\ H2 = H1 proof assume H1 is Subgroup of H2; then the carrier of H1 c= the carrier of H2 by Def5; then (the carrier of H1) /\ (the carrier of H2) = the carrier of H1 & the carrier of H1 /\ H2 = carr(H1) /\ carr (H2) & carr(H1) = the carrier of H1 & carr(H2) = the carrier of H2 by Def9,Def10, XBOOLE_1:28; hence thesis by Th68; end; assume H1 /\ H2 = H1; then the carrier of H1 = carr(H1) /\ carr(H2) by Def10 .= (the carrier of H1) /\ carr(H2) by Def9 .= (the carrier of H1) /\ (the carrier of H2) by Def9; then the carrier of H1 c= the carrier of H2 by XBOOLE_1:17; hence thesis by Th66; end; theorem (1).G /\ H = (1).G & H /\ (1).G = (1).G proof A1: (1).G is Subgroup of H by Th77; hence (1).G /\ H = (1).G by Lm3; thus thesis by A1,Lm3; end; theorem Th104: for G being strict Group, H being strict Subgroup of G holds H /\ (Omega).G = H & (Omega).G /\ H = H proof let G be strict Group,H be strict Subgroup of G; A1: H is Subgroup of (Omega).G by Th78; hence H /\ (Omega).G = H by Lm3; thus thesis by A1,Lm3; end; theorem for G being strict Group holds (Omega).G /\ (Omega).G = G proof let G be strict Group; thus (Omega).G /\ (Omega).G = (Omega).G by Th104 .= G by Def8; end; Lm4: H1 /\ H2 is Subgroup of H1 proof the carrier of H1 /\ H2 = (the carrier of H1) /\ (the carrier of H2) & (the carrier of H1) /\ (the carrier of H2) c= the carrier of H1 by Th97,XBOOLE_1: 17; hence thesis by Th66; end; theorem H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 by Lm4; theorem for H1 being strict Subgroup of G holds H1 is Subgroup of H2 iff H1 /\ H2 = H1 by Lm3; theorem H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 proof assume A1: H1 is Subgroup of H2; H1 /\ H3 is Subgroup of H1 by Lm4; hence thesis by A1,Th65; end; theorem H1 is Subgroup of H2 & H1 is Subgroup of H3 implies H1 is Subgroup of H2 /\ H3 proof assume A1: H1 is Subgroup of H2 & H1 is Subgroup of H3; now let g; assume g in H1; then g in H2 & g in H3 by A1,Th49; hence g in H2 /\ H3 by Th99; end; hence thesis by Th67; end; theorem H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3 proof assume H1 is Subgroup of H2; then the carrier of H1 c= the carrier of H2 by Def5; then (the carrier of H1) /\ (the carrier of H3) c= (the carrier of H2) /\ (the carrier of H3) by XBOOLE_1:26; then the carrier of H1 /\ H3 c= (the carrier of H2) /\ (the carrier of H3) by Th97; then the carrier of H1 /\ H3 c= the carrier of H2 /\ H3 by Th97; hence thesis by Th66; end; theorem H1 is finite or H2 is finite implies H1 /\ H2 is finite proof assume A1: H1 is finite or H2 is finite; H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 by Lm4; hence thesis by A1,Th48; end; definition let G,H,A; func A * H -> Subset of G equals :Def11: A * carr H; correctness; func H * A -> Subset of G equals :Def12: carr H * A; correctness; end; canceled 2; theorem x in A * H iff ex g1,g2 st x = g1 * g2 & g1 in A & g2 in H proof thus x in A * H implies ex g1,g2 st x = g1 * g2 & g1 in A & g2 in H proof assume x in A * H; then x in A * carr H by Def11; then consider g1,g2 such that A1: x = g1 * g2 & g1 in A & g2 in carr H by Th12; g2 in H by A1,Th88; hence thesis by A1; end; given g1,g2 such that A2: x = g1 * g2 & g1 in A & g2 in H; g2 in carr H by A2,Th88; then x in A * carr H by A2,Th12; hence thesis by Def11; end; theorem x in H * A iff ex g1,g2 st x = g1 * g2 & g1 in H & g2 in A proof thus x in H * A implies ex g1,g2 st x = g1 * g2 & g1 in H & g2 in A proof assume x in H * A; then x in carr H * A by Def12; then consider g1,g2 such that A1: x = g1 * g2 & g1 in carr H & g2 in A by Th12; g1 in H by A1,Th88; hence thesis by A1; end; given g1,g2 such that A2: x = g1 * g2 & g1 in H & g2 in A; g1 in carr H by A2,Th88; then x in carr H * A by A2,Th12; hence thesis by Def12; end; theorem Th116: A * B * H = A * (B * H) proof thus A * B * H = A * B * carr H by Def11 .= A * (B * carr H) by Th14 .= A * (B * H) by Def11; end; theorem Th117: A * H * B = A * (H * B) proof thus A * H * B = A * carr H * B by Def11 .= A * (carr H * B) by Th14 .= A * (H * B) by Def12; end; theorem Th118: H * A * B = H * (A * B) proof thus H * A * B = carr H * A * B by Def12 .= carr H * (A * B) by Th14 .= H * (A * B) by Def12; end; theorem A * H1 * H2 = A * (H1 * carr H2) proof thus A * H1 * H2 = A * H1 * carr H2 by Def11 .= A * (H1 * carr H2) by Th117; end; theorem H1 * A * H2 = H1 * (A * H2) proof thus H1 * A * H2 = carr H1 * A * H2 by Def12 .= carr H1 * (A * H2) by Th116 .= H1 * (A * H2) by Def12; end; theorem H1 * carr(H2) * A = H1 * (H2 * A) proof thus H1 * carr(H2) * A = H1 * (carr H2 * A) by Th118 .= H1 * (H2 * A) by Def12; end; theorem G is commutative Group implies A * H = H * A proof assume A1: G is commutative Group; thus A * H = A * carr H by Def11 .= carr H * A by A1,Th29 .= H * A by Def12; end; definition let G,H,a; func a * H -> Subset of G equals :Def13: a * carr(H); correctness; func H * a -> Subset of G equals :Def14: carr(H) * a; correctness; end; canceled 2; theorem Th125: x in a * H iff ex g st x = a * g & g in H proof thus x in a * H implies ex g st x = a * g & g in H proof assume x in a * H; then x in a * carr(H) by Def13; then consider g such that A1: x = a * g & g in carr(H) by Th33; take g; thus thesis by A1,Th88; end; given g such that A2: x = a * g & g in H; g in carr(H) by A2,Th88; then x in a * carr(H) by A2,Th33; hence thesis by Def13; end; theorem Th126: x in H * a iff ex g st x = g * a & g in H proof thus x in H * a implies ex g st x = g * a & g in H proof assume x in H * a; then x in carr(H) * a by Def14; then consider g such that A1: x = g * a & g in carr(H) by Th34; take g; thus thesis by A1,Th88; end; given g such that A2: x = g * a & g in H; g in carr(H) by A2,Th88; then x in carr(H) * a by A2,Th34; hence thesis by Def14; end; theorem Th127: a * b * H = a * (b * H) proof thus a * b * H = a * b * carr(H) by Def13 .= a * (b * carr(H)) by Th38 .= a * (b * H) by Def13; end; theorem Th128: a * H * b = a * (H * b) proof thus a * H * b = a * carr(H) * b by Def13 .= a * (carr(H) * b) by Th39 .= a * (H * b) by Def14; end; theorem Th129: H * a * b = H * (a * b) proof thus H * a * b = carr(H) * a * b by Def14 .= carr(H) * (a * b) by Th40 .= H * (a * b) by Def14; end; theorem Th130: a in a * H & a in H * a proof 1.G in H & a * 1.G = a & 1.G * a = a by Th55,GROUP_1:def 4; hence thesis by Th125,Th126; end; canceled; theorem Th132: 1.G * H = carr(H) & H * 1.G = carr(H) proof thus 1.G * H = 1.G * carr(H) by Def13 .= carr(H) by Th43; thus H * 1.G = carr(H) * 1.G by Def14 .= carr(H) by Th43; end; theorem Th133: (1).G * a = {a} & a * (1).G = {a} proof A1: the carrier of (1).G = {1.G} & the carrier of (1).G = carr((1).G) by Def7, Def9; hence (1).G * a = {1.G} * a by Def14 .= {1.G} * {a} by Def4 .= {1.G * a} by Th22 .= {a} by GROUP_1:def 4; thus a * (1).G = a * {1.G} by A1,Def13 .= {a} * {1.G} by Def3 .= {a * 1.G} by Th22 .= {a} by GROUP_1:def 4; end; theorem Th134: a * (Omega).G = the carrier of G & (Omega).G * a = the carrier of G proof the carrier of (Omega).G = carr((Omega).G) & (Omega). G = the HGrStr of G & [#](the carrier of G) = the carrier of G & [#](the carrier of G) * a = the carrier of G & a * [#](the carrier of G) = the carrier of G & a * (Omega).G = a * carr((Omega).G) & carr((Omega).G) * a = (Omega). G * a by Def8,Def9,Def13,Def14,Th42,SUBSET_1:def 4; hence thesis; end; theorem G is commutative Group implies a * H = H * a proof assume A1: G is commutative Group; thus a * H = a * carr(H) by Def13 .= carr(H) * a by A1,Th44 .= H * a by Def14; end; theorem Th136: a in H iff a * H = carr(H) proof thus a in H implies a * H = carr(H) proof assume A1: a in H; thus a * H c= carr(H) proof let x; assume x in a * H; then consider g such that A2: x = a * g and A3: g in H by Th125; a * g in H by A1,A3,Th59; hence thesis by A2,Th88; end; let x; assume x in carr(H); then A4: x in H by Th88; then x in G by Th49; then reconsider b = x as Element of G by RLVECT_1:def 1; a" in H by A1,Th60; then A5: a" * b in H by A4,Th59; a * (a" * b) = a * a" * b by VECTSP_1:def 16 .= 1.G * b by GROUP_1:def 5 .= x by GROUP_1:def 4; hence thesis by A5,Th125; end; assume A6: a * H = carr(H); a * 1.G = a & 1.G in H by Th55,GROUP_1:def 4; then a in carr(H) by A6,Th125; hence thesis by Th88; end; theorem Th137: a * H = b * H iff b" * a in H proof thus a * H = b * H implies b" * a in H proof assume A1: a * H = b * H; b" * a * H = b" * (a * H) by Th127 .= b" * b * H by A1,Th127 .= 1.G * H by GROUP_1:def 5 .= carr(H) by Th132; hence thesis by Th136; end; assume A2: b" * a in H; thus a * H = 1.G * (a * H) by Th43 .= 1.G * a * H by Th127 .= b * b" * a * H by GROUP_1:def 5 .= b * (b" * a) * H by VECTSP_1:def 16 .= b * ((b" * a) * H) by Th127 .= b * carr(H) by A2,Th136 .= b * H by Def13; end; theorem Th138: a * H = b * H iff a * H meets b * H proof a * H <> {} by Th130; hence a * H = b * H implies a * H meets b * H by XBOOLE_1:66; assume a * H meets b * H; then consider x such that A1: x in a * H and A2: x in b * H by XBOOLE_0:3; reconsider x as Element of G by A2; consider g such that A3: x = a * g & g in H by A1,Th125; consider h being Element of G such that A4: x = b * h & h in H by A2,Th125; a = b * h * g" by A3,A4,GROUP_1:22 .= b * (h * g") by VECTSP_1:def 16; then A5: b" * a = h * g" by GROUP_1:21; g" in H by A3,Th60; then b" * a in H by A4,A5,Th59; hence thesis by Th137; end; theorem Th139: a * b * H c= (a * H) * (b * H) proof let x; assume x in a * b * H; then consider g such that A1: x = a * b * g and A2: g in H by Th125; A3: x = a * 1.G * b * g by A1,GROUP_1:def 4 .= (a * 1.G) * (b * g) by VECTSP_1:def 16; 1.G in H by Th55; then a * 1.G in a * H & b * g in b * H by A2,Th125; hence thesis by A3,Th12; end; theorem carr(H) c= (a * H) * (a" * H) & carr(H) c= (a" * H) * (a * H) proof A1: a * a" * H = 1.G * H by GROUP_1:def 5 .= carr(H) by Th132; a" * a * H = 1.G * H by GROUP_1:def 5 .= carr(H) by Th132; hence thesis by A1,Th139; end; theorem a |^ 2 * H c= (a * H) * (a * H) proof a |^ 2 * H = a * a * H by GROUP_1:45; hence thesis by Th139; end; theorem Th142: a in H iff H * a = carr(H) proof thus a in H implies H * a = carr(H) proof assume A1: a in H; thus H * a c= carr(H) proof let x; assume x in H * a; then consider g such that A2: x = g * a and A3: g in H by Th126; g * a in H by A1,A3,Th59; hence thesis by A2,Th88; end; let x; assume x in carr(H); then A4: x in H by Th88; then x in G by Th49; then reconsider b = x as Element of G by RLVECT_1:def 1; a" in H by A1,Th60; then A5: b * a" in H by A4,Th59; (b * a") * a = b * (a" * a) by VECTSP_1:def 16 .= b * 1.G by GROUP_1:def 5 .= x by GROUP_1:def 4; hence thesis by A5,Th126; end; assume A6: H * a = carr(H); 1.G * a = a & 1.G in H by Th55,GROUP_1:def 4; then a in carr(H) by A6,Th126; hence thesis by Th88; end; theorem Th143: H * a = H * b iff b * a" in H proof thus H * a = H * b implies b * a" in H proof assume A1: H * a = H * b; carr(H) = carr(H) * 1.G by Th43 .= H * 1.G by Def14 .= H * (a * a") by GROUP_1:def 5 .= H * b * a" by A1,Th129 .= H * (b * a") by Th129; hence thesis by Th142; end; assume A2: b * a" in H; thus H * a = carr(H) * a by Def14 .= H * (b * a") * a by A2,Th142 .= H * (b * a" * a) by Th129 .= H * (b * (a" * a)) by VECTSP_1:def 16 .= H * (b * (1.G)) by GROUP_1:def 5 .= H * b by GROUP_1:def 4; end; theorem H * a = H * b iff H * a meets H * b proof H * a <> {} by Th130; hence H * a = H * b implies H * a meets H * b by XBOOLE_1:66; assume H * a meets H * b; then consider x such that A1: x in H * a and A2: x in H * b by XBOOLE_0:3; reconsider x as Element of G by A2; consider g such that A3: x = g * a & g in H by A1,Th126; consider h being Element of G such that A4: x = h * b & h in H by A2,Th126; a = g" * (h * b) by A3,A4,GROUP_1:21 .= g" * h * b by VECTSP_1:def 16; then A5: a * b" = g" * h by GROUP_1:22; g" in H by A3,Th60; then a * b" in H by A4,A5,Th59; hence thesis by Th143; end; theorem Th145: H * a * b c= (H * a) * (H * b) proof let x; assume x in H * a * b; then x in H * (a * b) by Th129; then consider g such that A1: x = g * (a * b) and A2: g in H by Th126; 1.G in H by Th55; then A3: 1.G * b in H * b & g * a in H * a by A2,Th126; x = g * a * b by A1,VECTSP_1:def 16 .= g * a * (1.G * b) by GROUP_1:def 4; hence thesis by A3,Th12; end; theorem carr(H) c= (H * a) * (H * a") & carr(H) c= (H * a") * (H * a) proof A1: H * a * a" = H * (a * a") by Th129 .= H * 1.G by GROUP_1:def 5 .= carr(H) by Th132; H * a"* a = H * (a"* a) by Th129 .= H * 1.G by GROUP_1:def 5 .= carr(H) by Th132; hence thesis by A1,Th145; end; theorem H * (a |^ 2) c= (H * a) * (H * a) proof a |^ 2 = a * a & H * a * a = H * (a * a) by Th129,GROUP_1:45; hence thesis by Th145; end; theorem a * (H1 /\ H2) = (a * H1) /\ (a * H2) proof thus a * (H1 /\ H2) c= (a * H1) /\ (a * H2) proof let x; assume x in a * (H1 /\ H2); then consider g such that A1: x = a * g and A2: g in H1 /\ H2 by Th125; g in H1 & g in H2 by A2,Th99; then x in a * H1 & x in a * H2 by A1,Th125; hence thesis by XBOOLE_0:def 3; end; let x; assume x in (a * H1) /\ (a * H2); then A3: x in a * H1 & x in a * H2 by XBOOLE_0:def 3; then consider g such that A4: x = a * g and A5: g in H1 by Th125; consider g1 such that A6: x = a * g1 and A7: g1 in H2 by A3,Th125; g = g1 by A4,A6,GROUP_1:14; then g in H1 /\ H2 by A5,A7,Th99; hence thesis by A4,Th125; end; theorem (H1 /\ H2) * a = (H1 * a) /\ (H2 * a) proof thus (H1 /\ H2) * a c= (H1 * a) /\ (H2 * a) proof let x; assume x in (H1 /\ H2) * a; then consider g such that A1: x = g * a and A2: g in H1 /\ H2 by Th126; g in H1 & g in H2 by A2,Th99; then x in H1 * a & x in H2 * a by A1,Th126; hence thesis by XBOOLE_0:def 3; end; let x; assume x in (H1 * a) /\ (H2 * a); then A3: x in H1 * a & x in H2 * a by XBOOLE_0:def 3; then consider g such that A4: x = g * a and A5: g in H1 by Th126; consider g1 such that A6: x = g1 * a and A7: g1 in H2 by A3,Th126; g = g1 by A4,A6,GROUP_1:14; then g in H1 /\ H2 by A5,A7,Th99; hence thesis by A4,Th126; end; theorem ex H1 being strict Subgroup of G st the carrier of H1 = a * H2 * a" proof set A = a * H2 * a"; A1: a * H2 <> {} by Th130; consider x being Element of a * H2; reconsider x as Element of G by A1,Lm1; A2: x * a" in A by A1,Th34; A3: now let g1,g2; assume that A4: g1 in A and A5: g2 in A; consider g such that A6: g1 = g * a" and A7: g in a * H2 by A4,Th34; A = a * (H2 * a") by Th128; then consider b such that A8: g2 = a * b and A9: b in H2 * a" by A5, Th33; consider h being Element of G such that A10: g = a * h and A11: h in H2 by A7,Th125; consider c being Element of G such that A12: b = c * a" and A13: c in H2 by A9,Th126; A14: g1 * g2 = (a * h) * (a" * (a * (c * a"))) by A6,A8,A10,A12, VECTSP_1:def 16 .= (a * h) * (a" * a * (c * a")) by VECTSP_1:def 16 .= (a * h) * (1.G * (c * a")) by GROUP_1:def 5 .= (a * h) * (c * a") by GROUP_1:def 4 .= a * h * c * a" by VECTSP_1:def 16 .= a * (h * c) * a" by VECTSP_1:def 16; h * c in H2 by A11,A13,Th59; then a * (h * c) in a * H2 by Th125; hence g1 * g2 in A by A14,Th34; end; now let g; assume g in A; then consider g1 such that A15: g = g1 * a" and A16: g1 in a * H2 by Th34; consider g2 such that A17: g1 = a * g2 and A18: g2 in H2 by A16,Th125; A19: g" = a"" * (a * g2)" by A15,A17,GROUP_1:25 .= a * (a * g2)" by GROUP_1:19 .= a * (g2" * a") by GROUP_1:25; g2" in H2 by A18,Th60; then g2" * a" in H2 * a" by Th126; then g" in a * (H2 * a") by A19,Th33; hence g" in A by Th128; end; hence thesis by A2,A3,Th61; end; theorem Th151: a * H,b * H are_equipotent proof defpred P[set,set] means ex g1 st $1 = g1 & $2 = b * a" * g1; A1: for x,y1,y2 st x in a * H & P[x,y1] & P[x,y2] holds y1 = y2; A2: for x st x in a * H ex y st P[x,y] proof let x; assume x in a * H; then reconsider g = x as Element of G; reconsider y = b * a" * g as set; take y; take g; thus thesis; end; consider f being Function such that A3: dom f = a * H and A4: for x st x in a * H holds P[x,f.x] from FuncEx(A1,A2); A5: rng f = b * H proof thus rng f c= b * H proof let x; assume x in rng f; then consider y such that A6: y in dom f and A7: f.y = x by FUNCT_1:def 5; consider g such that A8: y = g and A9: x = b * a" * g by A3,A4,A6,A7 ; consider g1 such that A10: g = a * g1 and A11: g1 in H by A3,A6,A8,Th125; x = b * a" * a * g1 by A9,A10,VECTSP_1:def 16 .= b * (a" * a) * g1 by VECTSP_1:def 16 .= b * 1.G * g1 by GROUP_1:def 5 .= b * g1 by GROUP_1:def 4; hence thesis by A11,Th125; end; let x; assume x in b * H; then consider g such that A12: x = b * g and A13: g in H by Th125; A14: a * g in dom f by A3,A13,Th125; then ex g1 st g1 = a * g & f.(a * g) = b * a" * g1 by A3,A4; then f.(a * g) = b * a" * a * g by VECTSP_1:def 16 .= b * (a" * a) * g by VECTSP_1:def 16 .= b * 1.G * g by GROUP_1:def 5 .= x by A12,GROUP_1:def 4; hence thesis by A14,FUNCT_1:def 5; end; f is one-to-one proof let x,y; assume that A15: x in dom f and A16: y in dom f and A17: f.x = f.y; A18: ex g1 st x = g1 & f.x = b * a" * g1 by A3,A4,A15; ex g2 st y = g2 & f.y = b * a" * g2 by A3,A4,A16; hence x = y by A17,A18,GROUP_1:14; end; hence thesis by A3,A5,WELLORD2:def 4; end; theorem Th152: a * H,H * b are_equipotent proof defpred P[set,set] means ex g1 st $1 = g1 & $2 = a" * g1 * b; A1: for x,y1,y2 st x in a * H & P[x,y1] & P[x,y2] holds y1 = y2; A2: for x st x in a * H ex y st P[x,y] proof let x; assume x in a * H; then reconsider g = x as Element of G; reconsider y = a" * g * b as set; take y; take g; thus thesis; end; consider f being Function such that A3: dom f = a * H and A4: for x st x in a * H holds P[x,f.x] from FuncEx(A1,A2); A5: rng f = H * b proof thus rng f c= H * b proof let x; assume x in rng f; then consider y such that A6: y in dom f and A7: f.y = x by FUNCT_1:def 5; consider g such that A8: y = g and A9: x = a" * g * b by A3,A4,A6,A7 ; consider g1 such that A10: g = a * g1 and A11: g1 in H by A3,A6,A8,Th125; x = a" * a * g1 * b by A9,A10,VECTSP_1:def 16 .= 1.G * g1 * b by GROUP_1:def 5 .= g1 * b by GROUP_1:def 4; hence thesis by A11,Th126; end; let x; assume x in H * b; then consider g such that A12: x = g * b and A13: g in H by Th126; A14: a * g in dom f by A3,A13,Th125; then ex g1 st g1 = a * g & f.(a * g) = a" * g1 * b by A3,A4; then f.(a * g) = a" * a * g * b by VECTSP_1:def 16 .= 1.G * g * b by GROUP_1:def 5 .= x by A12,GROUP_1:def 4; hence thesis by A14,FUNCT_1:def 5; end; f is one-to-one proof let x,y; assume that A15: x in dom f and A16: y in dom f and A17: f.x = f.y; consider g1 such that A18: x = g1 and A19: f.x = a" * g1 * b by A3,A4, A15; consider g2 such that A20: y = g2 and A21: f.y = a" * g2 * b by A3,A4, A16; a" * g1 = a" * g2 by A17,A19,A21,GROUP_1:14; hence x = y by A18,A20,GROUP_1:14; end; hence thesis by A3,A5,WELLORD2:def 4; end; theorem Th153: H * a,H * b are_equipotent proof H * a,b * H are_equipotent & b * H,H * b are_equipotent by Th152; hence thesis by WELLORD2:22; end; theorem Th154: carr(H),a * H are_equipotent & carr(H),H * a are_equipotent proof carr(H) = 1.G * H & carr(H) = H * 1.G by Th132; hence thesis by Th151,Th153; end; theorem Ord(H) = Card(a * H) & Ord(H) = Card(H * a) proof A1: carr(H),a * H are_equipotent by Th154; thus Ord(H) = Card(the carrier of H) by GROUP_1:def 12 .= Card(carr(H)) by Def9 .= Card(a * H) by A1,CARD_1:21; A2: carr(H),H * a are_equipotent by Th154; thus Ord(H) = Card(the carrier of H) by GROUP_1:def 12 .= Card(carr(H)) by Def9 .= Card(H * a) by A2,CARD_1:21; end; theorem Th156: H is finite implies ex B,C being finite set st B = a * H & C = H * a & ord H = card B & ord H = card C proof assume H is finite; then consider D being finite set such that A1: D = the carrier of H & ord H = card D by GROUP_1:def 14; A2: carr(H) is finite & carr(H),a * H are_equipotent & carr(H),H * a are_equipotent by A1,Def9,Th154; then reconsider B = a * H, C = H * a, E = carr H as finite set by CARD_1:68; take B,C; ord H = card E by A1,Def9; hence thesis by A2,CARD_1:81; end; scheme SubFamComp{A() -> set, F1() -> Subset-Family of A(), F2() -> Subset-Family of A(), P[set]}: F1() = F2() provided A1: for X being Subset of A() holds X in F1() iff P[X] and A2: for X being Subset of A() holds X in F2() iff P[X] proof thus F1() c= F2() proof let x; assume A3: x in F1(); then reconsider X = x as Subset of A(); P[X] by A1,A3; hence thesis by A2; end; let x; assume A4: x in F2(); then reconsider X = x as Subset of A(); P[X] by A2,A4; hence thesis by A1; end; definition let G,H; func Left_Cosets H -> Subset-Family of G means :Def15: A in it iff ex a st A = a * H; existence proof defpred P[set] means ex a st $1 = a * H; ex F be Subset-Family of G st for A being Subset of G holds A in F iff P[A] from SubFamEx; hence thesis; end; uniqueness proof let F1,F2 be Subset-Family of G; defpred P[set] means ex a st $1 = a * H; assume A1: for A holds A in F1 iff P[A]; assume A2: for A holds A in F2 iff P[A]; thus thesis from SubFamComp(A1,A2); end; func Right_Cosets H -> Subset-Family of G means :Def16: A in it iff ex a st A = H * a; existence proof defpred P[set] means ex a st $1 = H * a; ex F be Subset-Family of G st for A being Subset of G holds A in F iff P[A] from SubFamEx; hence thesis; end; uniqueness proof let F1,F2 be Subset-Family of G; defpred P[set] means ex a st $1 = H * a; assume A3: for A holds A in F1 iff P[A]; assume A4: for A holds A in F2 iff P[A]; thus thesis from SubFamComp(A3,A4); end; end; canceled 7; theorem Th164: G is finite implies Right_Cosets H is finite & Left_Cosets H is finite proof assume G is finite; then the carrier of G is finite by GROUP_1:def 13; then bool(the carrier of G) is finite & Right_Cosets H c= bool(the carrier of G) & Left_Cosets H c= bool(the carrier of G) by FINSET_1:24; hence thesis by FINSET_1:13; end; theorem carr H in Left_Cosets H & carr H in Right_Cosets H proof carr H = 1.G * H & carr H = H * 1.G by Th132; hence thesis by Def15,Def16; end; theorem Th166: Left_Cosets H, Right_Cosets H are_equipotent proof defpred P[set,set] means ex g st $1 = g * H & $2 = H * g"; A1: for x,y1,y2 being set st x in Left_Cosets H & P[x,y1] & P[x,y2] holds y1 = y2 proof let x,y1,y2; assume x in Left_Cosets H; given a such that A2: x = a * H and A3: y1 = H * a"; given b such that A4: x = b * H and A5: y2 = H * b"; b" * a in H by A2,A4,Th137; then b" * a"" in H by GROUP_1:19; hence y1 = y2 by A3,A5,Th143; end; A6: for x st x in Left_Cosets H ex y st P[x,y] proof let x; assume x in Left_Cosets H; then consider g such that A7: x = g * H by Def15; reconsider y = H * g" as set; take y; take g; thus thesis by A7; end; consider f being Function such that A8: dom f = Left_Cosets H and A9: for x st x in Left_Cosets H holds P[x,f.x] from FuncEx(A1,A6); A10: rng f = Right_Cosets H proof thus rng f c= Right_Cosets H proof let x; assume x in rng f; then consider y such that A11: y in dom f and A12: f.y = x by FUNCT_1:def 5; ex g st y = g * H & f.y = H * g" by A8,A9,A11; hence thesis by A12,Def16; end; let x; assume A13: x in Right_Cosets H; then reconsider A = x as Subset of G; consider g such that A14: A = H * g by A13,Def16; A15: g" * H in Left_Cosets H by Def15; then A16: f.(g" * H) in rng f by A8,FUNCT_1:def 5; consider a such that A17: g" * H = a * H and A18: f.(g" * H) = H * a" by A9, A15; a" * g" in H by A17,Th137; hence thesis by A14,A16,A18,Th143; end; f is one-to-one proof let x,y; assume that A19: x in dom f and A20: y in dom f and A21: f.x = f.y; consider a such that A22: x = a * H and A23: f.x = H * a" by A8,A9,A19 ; consider b such that A24: y = b * H and A25: f.y = H * b" by A8,A9,A20 ; b" * a"" in H by A21,A23,A25,Th143; then b" * a in H by GROUP_1:19; hence thesis by A22,A24,Th137; end; hence thesis by A8,A10,WELLORD2:def 4; end; theorem Th167: union Left_Cosets H = the carrier of G & union Right_Cosets H = the carrier of G proof thus union Left_Cosets H = the carrier of G proof thus union Left_Cosets H c= the carrier of G; let x; assume x in the carrier of G; then reconsider a = x as Element of G; consider h; reconsider g = h as Element of G by Th51; A1: h in H by RLVECT_1:def 1; a = a * 1.G by GROUP_1:def 4 .= a * (g" * g) by GROUP_1:def 5 .= a * g" * g by VECTSP_1:def 16; then a in a * g" * H & a * g" * H in Left_Cosets H by A1,Def15,Th125; hence thesis by TARSKI:def 4; end; thus union Right_Cosets H c= the carrier of G; let x; assume x in the carrier of G; then reconsider a = x as Element of G; consider h; reconsider g = h as Element of G by Th51; A2: h in H by RLVECT_1:def 1; a = 1.G * a by GROUP_1:def 4 .= g * g" * a by GROUP_1:def 5 .= g * (g" * a) by VECTSP_1:def 16; then a in H * (g" * a) & H * (g" * a) in Right_Cosets H by A2,Def16, Th126 ; hence thesis by TARSKI:def 4; end; theorem Th168: Left_Cosets (1).G = {{a} : not contradiction} proof set A = {{a} : not contradiction}; thus Left_Cosets (1).G c= A proof let x; assume A1: x in Left_Cosets (1).G; then reconsider X = x as Subset of G; consider g such that A2: X = g * (1).G by A1,Def15; x = {g} by A2,Th133; hence thesis; end; let x; assume x in A; then consider a such that A3: x = {a}; a * (1).G = {a} by Th133; hence thesis by A3,Def15; end; theorem Right_Cosets (1).G = {{a} : not contradiction} proof set A = {{a} : not contradiction}; thus Right_Cosets (1).G c= A proof let x; assume A1: x in Right_Cosets (1).G; then reconsider X = x as Subset of G; consider g such that A2: X = (1).G * g by A1,Def16; x = {g} by A2,Th133; hence thesis; end; let x; assume x in A; then consider a such that A3: x = {a}; (1).G * a = {a} by Th133; hence thesis by A3,Def16; end; theorem for H being strict Subgroup of G holds Left_Cosets H = {{a} : not contradiction} implies H = (1).G proof let H be strict Subgroup of G; assume A1: Left_Cosets H = {{a} : not contradiction}; A2: the carrier of H c= {1.G} proof let x; assume x in the carrier of H; then reconsider h = x as Element of H; A3: h in H by RLVECT_1:def 1; reconsider h as Element of G by Th51; consider a; 1.G in H by Th55; then A4: a * 1.G in a * H & a * h in a * H & a * H in Left_Cosets H by A3,Def15,Th125; then consider b such that A5: a * H = {b} by A1; a * 1.G = b & a * h = b by A4,A5,TARSKI:def 1; then h = 1.G by GROUP_1:14; hence thesis by TARSKI:def 1; end; 1.G in H by Th55; then 1.G in the carrier of H by RLVECT_1:def 1; then {1.G} c= the carrier of H by ZFMISC_1:37; then {1.G} = the carrier of H by A2,XBOOLE_0:def 10; hence thesis by Def7; end; theorem for H being strict Subgroup of G holds Right_Cosets H = {{a} : not contradiction} implies H = (1).G proof let H be strict Subgroup of G; assume A1: Right_Cosets H = {{a} : not contradiction}; A2: the carrier of H c= {1.G} proof let x; assume x in the carrier of H; then reconsider h = x as Element of H; A3: h in H by RLVECT_1:def 1; reconsider h as Element of G by Th51; consider a; 1.G in H by Th55; then A4: 1.G * a in H * a & h * a in H * a & H * a in Right_Cosets H by A3,Def16,Th126; then consider b such that A5: H * a = {b} by A1; 1.G * a = b & h * a = b by A4,A5,TARSKI:def 1; then h = 1.G by GROUP_1:14; hence thesis by TARSKI:def 1; end; 1.G in H by Th55; then 1.G in the carrier of H by RLVECT_1:def 1; then {1.G} c= the carrier of H by ZFMISC_1:37; then {1.G} = the carrier of H by A2,XBOOLE_0:def 10; hence thesis by Def7; end; theorem Th172: Left_Cosets (Omega).G = {the carrier of G} & Right_Cosets (Omega).G = {the carrier of G} proof consider a; a * (Omega).G = the carrier of G & (Omega). G * a = the carrier of G by Th134; then the carrier of G in Left_Cosets (Omega).G & the carrier of G in Right_Cosets(Omega).G by Def15,Def16; then A1: {the carrier of G} c= Left_Cosets (Omega).G & {the carrier of G} c= Right_Cosets(Omega).G by ZFMISC_1:37; A2: Left_Cosets (Omega).G c= {the carrier of G} proof let x; assume A3: x in Left_Cosets (Omega).G; then reconsider X = x as Subset of G; consider a such that A4: X = a * (Omega).G by A3,Def15; a * (Omega).G = the carrier of G by Th134; hence thesis by A4,TARSKI:def 1; end; Right_Cosets (Omega).G c= {the carrier of G} proof let x; assume A5: x in Right_Cosets (Omega).G; then reconsider X = x as Subset of G; consider a such that A6: X = (Omega).G * a by A5,Def16; (Omega).G * a = the carrier of G by Th134; hence thesis by A6,TARSKI:def 1; end; hence thesis by A1,A2,XBOOLE_0:def 10; end; theorem Th173: for G being strict Group, H being strict Subgroup of G holds Left_Cosets H = {the carrier of G} implies H = G proof let G be strict Group, H be strict Subgroup of G; assume Left_Cosets H = {the carrier of G}; then A1: the carrier of G in Left_Cosets H by TARSKI:def 1; then reconsider T = the carrier of G as Subset of G; consider a being Element of G such that A2: T = a * H by A1,Def15; now let g be Element of G; ex b being Element of G st a * g = a * b & b in H by A2,Th125; hence g in H by GROUP_1:14; end; hence thesis by Th71; end; theorem for G being strict Group, H being strict Subgroup of G holds Right_Cosets H = {the carrier of G} implies H = G proof let G be strict Group, H be strict Subgroup of G; assume Right_Cosets H = {the carrier of G}; then A1: the carrier of G in Right_Cosets H by TARSKI:def 1; then reconsider T = the carrier of G as Subset of G; consider a being Element of G such that A2: T = H * a by A1,Def16; now let g be Element of G; ex b being Element of G st g * a = b * a & b in H by A2,Th126; hence g in H by GROUP_1:14; end; hence thesis by Th71; end; definition let G,H; func Index H -> Cardinal equals :Def17: Card Left_Cosets H; correctness; end; theorem Index H = Card Left_Cosets H & Index H = Card Right_Cosets H proof thus A1: Index H = Card Left_Cosets H by Def17; Left_Cosets(H), Right_Cosets(H) are_equipotent by Th166; hence thesis by A1,CARD_1:21; end; definition let G,H; assume A1: Left_Cosets(H) is finite; func index H -> Nat means :Def18: ex B being finite set st B = Left_Cosets H & it = card B; existence proof reconsider B = Left_Cosets(H) as finite set by A1; take card B, B; thus thesis; end; uniqueness; end; theorem Left_Cosets H is finite implies (ex B being finite set st B = Left_Cosets H & index H = card B) & ex C being finite set st C = Right_Cosets H & index H = card C proof assume A1: Left_Cosets H is finite; then reconsider B = Left_Cosets H as finite set; hereby take B; thus B = Left_Cosets H & index H = card B by Def18; end; A2: B = Left_Cosets H & index H = card B by Def18; A3: Left_Cosets(H), Right_Cosets(H) are_equipotent by Th166; then reconsider C = Right_Cosets H as finite set by A1,CARD_1:68; take C; thus thesis by A2,A3,CARD_1:81; end; definition let D be non empty set; let d be Element of D; redefine func {d} -> Element of Fin D; coherence proof thus {d} is Element of Fin D by FINSUB_1:def 5; end; end; Lm5: for X being finite set st (for Y st Y in X ex B being finite set st B = Y & card B = k & for Z st Z in X & Y <> Z holds Y,Z are_equipotent & Y misses Z) ex C being finite set st C = union X & card C = k * card X proof let X be finite set; per cases; suppose A1: X = {}; assume for Y st Y in X ex B being finite set st B = Y & card B = k & for Z st Z in X & Y <> Z holds Y,Z are_equipotent & Y misses Z; reconsider E = {} as finite set; take E; thus thesis by A1,CARD_1:78,ZFMISC_1:2; suppose X <> {}; then reconsider D = X as non empty set; defpred P[Element of Fin D] means (for Y st Y in $1 ex B being finite set st B = Y & card B = k & for Z st Z in $1 & Y <> Z holds Y,Z are_equipotent & Y misses Z) implies ex C being finite set st C = union $1 & card C = k * card $1; A2: P[{}.D] by CARD_1:78,ZFMISC_1:2; A3: for S being Element of Fin D, s being Element of D st P[S] & not s in S holds P[S \/ {s}] proof let S be Element of Fin D, s be Element of D; assume that A4: (for Y st Y in S ex B being finite set st B = Y & card B = k & for Z st Z in S & Y <> Z holds Y,Z are_equipotent & Y misses Z) implies ex C being finite set st C = union S & card C = k * card S and A5: not s in S and A6: for Y st Y in S \/ {s} ex B being finite set st B = Y & card B = k & for Z st Z in S \/ {s} & Y <> Z holds Y,Z are_equipotent & Y misses Z; now let Y; assume A7: Y in S; s in {s} by TARSKI:def 1; then Y in S \/ {s} & s in S \/ {s} & s <> Y by A5,A7,XBOOLE_0:def 2; then ex B being finite set st B = Y & card B = k & for Z st Z in S \/ {s} & Y <> Z holds Y,Z are_equipotent & Y misses Z by A6; hence Y is finite; end; then reconsider D1 = union S as finite set by FINSET_1:25; A8: union{s} = s by ZFMISC_1:31; s in {s} by TARSKI:def 1; then s in S \/ {s} by XBOOLE_0:def 2; then consider B being finite set such that A9: B = s & card B = k & for Z st Z in S \/ {s} & s <> Z holds s,Z are_equipotent & s misses Z by A6; reconsider T = s as finite set by A9; A10: now assume union S meets union{s}; then consider x being set such that A11: x in union S & x in union{s} by XBOOLE_0:3; consider Y such that A12: x in Y and A13: Y in S by A11,TARSKI:def 4; consider Z such that A14: x in Z and A15: Z in {s} by A11,TARSKI:def 4; A16: Z <> Y & Z in S \/ {s} & Y in S \/ {s} by A5,A13,A15,TARSKI:def 1,XBOOLE_0:def 2; then consider B being finite set such that A17: B = Y & card B = k & for Z st Z in S \/ {s} & Y <> Z holds Y,Z are_equipotent & Y misses Z by A6; Y misses Z by A16,A17; hence contradiction by A12,A14,XBOOLE_0:3; end; A18: union(S \/ {s}) = D1 \/ T by A8,ZFMISC_1:96; then reconsider D2 = union(S \/ {s}) as finite set; take D2; thus D2 = union(S \/ {s}); A19: now let Y,Z; assume Y in S; then Y in S \/ {s} by XBOOLE_0:def 2; then consider B being finite set such that A20: B = Y & card B = k & for Z st Z in S \/ {s} & Y <> Z holds Y,Z are_equipotent & Y misses Z by A6; take B; thus B = Y & card B = k by A20; let Z; assume that A21: Z in S and A22: Y <> Z; Z in S \/ {s} by A21,XBOOLE_0:def 2; hence Y,Z are_equipotent & Y misses Z by A20,A22; end; A23: card(S \/ {s}) = card S + 1 by A5,CARD_2:54; thus card D2 = k * card S + k * 1 by A4,A8,A9,A10,A18,A19,CARD_2:53 .= k * card(S \/ {s}) by A23,XCMPLX_1:8; end; A24: for B being Element of Fin D holds P[B] from FinSubInd1(A2,A3); X is Element of Fin D by FINSUB_1:def 5; hence thesis by A24; end; :: Lagrange Theorem theorem Th177: G is finite implies ord G = ord H * index H proof assume A1: G is finite; then reconsider C = Left_Cosets H as finite set by Th164; consider B being finite set such that A2: B = the carrier of G & ord G = card B by A1,GROUP_1:def 14; A3: union Left_Cosets H = the carrier of G & ord G = card B by A2,Th167; now let X be set; assume A4: X in C; then reconsider x = X as Subset of G; consider a such that A5: x = a * H by A4,Def15; x is finite by A1,Th3; then reconsider B = X as finite set; take B; thus B = X; H is finite by A1,Th48; then ex B,C being finite set st B = a * H & C = H * a & ord H = card B & ord H = card C by Th156; hence card B = ord H by A5; let Y; assume that A6: Y in C and A7: X <> Y; reconsider y = Y as Subset of G by A6; consider b such that A8: y = b * H by A6,Def15; thus X,Y are_equipotent by A5,A8,Th151; thus X misses Y by A5,A7,A8,Th138; end; then ex D being finite set st D = union C & card D = ord H * card C by Lm5 ; hence thesis by A2,A3,Def18; end; theorem G is finite implies ord H divides ord G proof assume G is finite; then ord G = ord H * index H by Th177; hence thesis by NAT_1:def 3; end; reserve J for Subgroup of H; theorem G is finite & I = J implies index I = index J * index H proof assume that A1: G is finite and A2: I = J; A3: ord G = ord H * index H & ord G = ord I * index I by A1,Th177; H is finite by A1,Th48; then ord H = ord J * index J by Th177; then ord I * (index J * index H) = ord I * index I & ord I <> 0 by A1,A2,A3,GROUP_1:90,XCMPLX_1:4; hence thesis by XCMPLX_1:5; end; theorem index (Omega).G = 1 proof Left_Cosets (Omega).G = {the carrier of G} by Th172; hence index (Omega).G = card{the carrier of G} by Def18 .= 1 by CARD_1:79; end; theorem for G being strict Group, H being strict Subgroup of G holds Left_Cosets H is finite & index H = 1 implies H = G proof let G be strict Group, H be strict Subgroup of G; assume that A1: Left_Cosets H is finite and A2: index H = 1; reconsider B = Left_Cosets H as finite set by A1; card B = 1 by A2,Def18; then consider x such that A3: Left_Cosets H = {x} by CARD_2:60; union {x} = x & union Left_Cosets H = the carrier of G by Th167,ZFMISC_1:31; hence thesis by A3,Th173; end; theorem Index (1).G = Ord G proof deffunc F(set) = {$1}; consider f being Function such that A1: dom f = the carrier of G and A2: for x st x in the carrier of G holds f.x = F(x) from Lambda; A3: rng f = Left_Cosets (1).G proof thus rng f c= Left_Cosets (1).G proof let x; assume x in rng f; then consider y such that A4: y in dom f and A5: f.y = x by FUNCT_1:def 5; reconsider y as Element of G by A1,A4; x = {y} by A2,A5; then x in {{a} : not contradiction}; hence thesis by Th168; end; let x; assume x in Left_Cosets (1).G; then x in {{a} : not contradiction} by Th168; then consider a such that A6: x = {a}; f.a = {a} by A2; hence thesis by A1,A6,FUNCT_1:def 5; end; f is one-to-one proof let x,y; assume A7: x in dom f & y in dom f & f.x = f.y; then f.y = {y} & f.x = {x} by A1,A2; hence thesis by A7,ZFMISC_1:6; end; then A8: the carrier of G,Left_Cosets (1).G are_equipotent by A1,A3,WELLORD2:def 4; thus Index (1).G = Card Left_Cosets (1).G by Def17 .= Card(the carrier of G) by A8,CARD_1:21 .= Ord G by GROUP_1:def 12; end; theorem G is finite implies index (1).G = ord G proof assume G is finite; hence ord G = ord (1).G * index (1).G by Th177 .= 1 * index (1).G by Th81 .= index (1).G; end; theorem Th184: for H being strict Subgroup of G holds G is finite & index H = ord G implies H = (1).G proof let H be strict Subgroup of G; assume A1: G is finite & index H = ord G; then 1 * ord G = ord H * ord G & ord G <> 0 by Th177,GROUP_1:90; then ord H = 1 & H is finite by A1,Th48,XCMPLX_1:5; hence thesis by Th82; end; theorem for H being strict Subgroup of G holds Left_Cosets H is finite & Index H = Ord G implies G is finite & H = (1).G proof let H be strict Subgroup of G; assume that A1: Left_Cosets H is finite and A2: Index H = Ord G; A3: Index H = Card Left_Cosets H & Ord G = Card(the carrier of G) & Ord G <=` Index H by A2,Def17,GROUP_1:def 12; then the carrier of G is finite by A1,CARD_2:68; hence A4: G is finite by GROUP_1:def 13; then consider C being finite set such that A5: C = the carrier of G & ord G = card C by GROUP_1:def 14; consider B being finite set such that A6: B = Left_Cosets H & index H = card B by A1,Def18; thus thesis by A2,A3,A4,A5,A6,Th184; end; :: :: Auxiliary theorems. :: theorem for X being finite set st (for Y st Y in X ex B being finite set st B = Y & card B = k & for Z st Z in X & Y <> Z holds Y,Z are_equipotent & Y misses Z) ex C being finite set st C = union X & card C = k * card X by Lm5;

Back to top