### The Mizar article:

### Classes of Conjugation. Normal Subgroups

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

- Received August 10, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: GROUP_3
- [ MML identifier index ]

environ vocabulary REALSET1, GROUP_2, INT_1, RELAT_1, GROUP_1, BINOP_1, VECTSP_1, FUNCT_1, FINSET_1, CARD_1, ABSVALUE, BOOLE, TARSKI, RLSUB_1, SETFAM_1, ARYTM_1, GROUP_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, RLVECT_1, FINSET_1, VECTSP_1, GROUP_2, DOMAIN_1, CARD_1, INT_1, GROUP_1; constructors WELLORD2, REAL_1, BINOP_1, GROUP_2, DOMAIN_1, NAT_1, MEMBERED, XBOOLE_0; clusters SUBSET_1, FUNCT_1, FINSET_1, GROUP_2, GROUP_1, STRUCT_0, RELSET_1, INT_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE, ARITHM; definitions XBOOLE_0, BINOP_1, FUNCT_1, GROUP_2, TARSKI, VECTSP_1; theorems ABSVALUE, BINOP_1, CARD_1, CARD_2, ENUMSET1, FINSET_1, FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, TARSKI, WELLORD2, ZFMISC_1, RLVECT_1, RELAT_1, VECTSP_1, SETFAM_1, XBOOLE_0, XBOOLE_1; schemes FUNCT_1, FUNCT_2, NAT_1, SUBSET_1, XBOOLE_0; begin reserve x,y,y1,y2 for set; reserve G for Group; reserve a,b,c,d,g,h for Element of G; reserve A,B,C,D for Subset of G; reserve H,H1,H2,H3 for Subgroup of G; reserve n for Nat; reserve i for Integer; theorem Th1: a * b * b" = a & a * b" * b = a & b" * b * a = a & b * b" * a = a & a * (b * b") = a & a * (b" * b) = a & b" * (b * a) = a & b * (b" * a) = a proof thus A1: a * b * b" = a * (b * b") by VECTSP_1:def 16 .= a * 1.G by GROUP_1:def 5 .= a by GROUP_1:def 4; thus A2: a * b" * b = a * (b" * b) by VECTSP_1:def 16 .= a * 1.G by GROUP_1:def 5 .= a by GROUP_1:def 4; thus A3: b" * b * a = 1.G * a by GROUP_1:def 5 .= a by GROUP_1:def 4; thus b * b" * a = 1.G * a by GROUP_1:def 5 .= a by GROUP_1:def 4; hence thesis by A1,A2,A3,VECTSP_1:def 16; end; Lm1: for A be commutative Group, a, b be Element of A holds a * b = b * a; theorem G is commutative Group iff the mult of G is commutative proof thus G is commutative Group implies the mult of G is commutative proof assume A1: G is commutative Group; let a,b; thus (the mult of G).(a,b) = a * b by VECTSP_1:def 10 .= b * a by A1,Lm1 .= (the mult of G).(b,a) by VECTSP_1:def 10; end; assume A2: the mult of G is commutative; G is commutative proof let a,b; thus a * b = (the mult of G).(a,b) by VECTSP_1:def 10 .= (the mult of G).(b,a) by A2,BINOP_1:def 2 .= b * a by VECTSP_1:def 10; end; hence thesis; end; theorem (1).G is commutative proof let a,b be Element of (1).G; a in the carrier of (1).G & b in the carrier of (1).G; then a in {1.G} & b in {1.G} by GROUP_2:def 7; then a = 1.G & b = 1.G by TARSKI:def 1; hence a * b = b * a; end; theorem Th4: A c= B & C c= D implies A * C c= B * D proof assume A1: A c= B & C c= D; let x; assume x in A * C; then consider a,c such that A2: x = a * c & a in A & c in C by GROUP_2:12; thus thesis by A1,A2,GROUP_2:12; end; theorem Th5: A c= B implies a * A c= a * B & A * a c= B * a proof a * A = {a} * A & a * B = {a} * B & A * a = A * {a} & B * a = B * {a} by GROUP_2:def 3,def 4; hence thesis by Th4; end; theorem Th6: H1 is Subgroup of H2 implies a * H1 c= a * H2 & H1 * a c= H2 * a proof assume H1 is Subgroup of H2; then the carrier of H1 c= the carrier of H2 & carr H1 = the carrier of H1 & the carrier of H2 = carr H2 & a * H1 = a * carr H1 & a * H2 = a * carr H2 & H1 * a = carr H1 * a & H2 * a = carr H2 * a by GROUP_2:def 5,def 9,def 13,def 14; hence thesis by Th5; end; theorem Th7: a * H = {a} * H proof thus a * H = a * carr H by GROUP_2:def 13 .= {a} * carr H by GROUP_2:def 3 .= {a} * H by GROUP_2:def 11; end; theorem Th8: H * a = H * {a} proof thus H * a = carr H * a by GROUP_2:def 14 .= carr H * {a} by GROUP_2:def 4 .= H * {a} by GROUP_2:def 12; end; theorem a * A * H = a * (A * H) proof thus a * A * H = {a} * A * H by GROUP_2:def 3 .= {a} * (A * H) by GROUP_2:116 .= a * (A * H) by GROUP_2:def 3; end; theorem Th10: A * a * H = A * (a * H) proof thus A * a * H = A * {a} * H by GROUP_2:def 4 .= A * ({a} * H) by GROUP_2:116 .= A * (a * H) by Th7; end; theorem a * H * A = a * (H * A) proof thus a * H * A = {a} * H * A by Th7 .= {a} * (H * A) by GROUP_2:117 .= a * (H * A) by GROUP_2:def 3; end; theorem A * H * a = A * (H * a) proof thus A * H * a = A * H * {a} by GROUP_2:def 4 .= A * (H * {a}) by GROUP_2:117 .= A * (H * a) by Th8; end; theorem H * a * A = H * (a * A) proof thus H * a * A = H * {a} * A by Th8 .= H * ({a} * A) by GROUP_2:118 .= H * (a * A) by GROUP_2:def 3; end; theorem H * A * a = H * (A * a) proof thus H * A * a = H * A * {a} by GROUP_2:def 4 .= H * (A * {a}) by GROUP_2:118 .= H * (A * a) by GROUP_2:def 4; end; theorem H1 * a * H2 = H1 * (a * H2) proof thus H1 * a * H2 = carr H1 * a * H2 by GROUP_2:def 14 .= carr H1 * (a * H2) by Th10 .= H1 * (a * H2) by GROUP_2:def 12; end; definition let G; func Subgroups G -> set means :Def1: x in it iff x is strict Subgroup of G; existence proof defpred P[set] means ex H being strict Subgroup of G st $1 = the carrier of H; consider B being set such that A1: for x holds x in B iff x in bool the carrier of G & P[x] from Separation; defpred P[set,set] means ex H being strict Subgroup of G st $2 = H & $1 = the carrier of H; A2: for x,y1,y2 st P[x,y1] & P[x,y2] holds y1 = y2 by GROUP_2:68; consider f being Function such that A3: for x,y holds [x,y] in f iff x in B & P[x,y] from GraphFunc(A2); for x holds x in B iff ex y st [x,y] in f proof let x; thus x in B implies ex y st [x,y] in f proof assume A4: x in B; then consider H being strict Subgroup of G such that A5: x = the carrier of H by A1; reconsider y = H as set; take y; thus thesis by A3,A4,A5; end; given y such that A6: [x,y] in f; thus thesis by A3,A6; end; then A7: B = dom f by RELAT_1:def 4; for y holds y in rng f iff y is strict Subgroup of G proof let y; thus y in rng f implies y is strict Subgroup of G proof assume y in rng f; then consider x such that A8: x in dom f & y = f.x by FUNCT_1:def 5; [x,y] in f by A8,FUNCT_1:def 4; then ex H being strict Subgroup of G st y = H & x = the carrier of H by A3; hence thesis; end; assume y is strict Subgroup of G; then reconsider H = y as strict Subgroup of G; reconsider x = the carrier of H as set; the carrier of H c= the carrier of G by GROUP_2:def 5; then A9: x in dom f by A1,A7; then [x,y] in f by A3,A7; then y = f.x by A9,FUNCT_1:def 4; hence thesis by A9,FUNCT_1:def 5; end; hence thesis; end; uniqueness proof let A1,A2 be set; defpred P[set] means $1 is strict Subgroup of G; assume A10: x in A1 iff P[x]; assume A11: x in A2 iff P[x]; thus thesis from Extensionality(A10,A11); end; end; definition let G; cluster Subgroups G -> non empty; coherence proof consider x being strict Subgroup of G; x in Subgroups G by Def1; hence thesis; end; end; canceled 2; theorem for G being strict Group holds G in Subgroups G proof let G be strict Group; G is Subgroup of G by GROUP_2:63; hence thesis by Def1; end; theorem Th19: G is finite implies Subgroups G is finite proof defpred P[set,set] means ex H being strict Subgroup of G st $1 = H & $2 = the carrier of H; assume A1: G is finite; A2: for x,y1,y2 st x in Subgroups G & P[x,y1] & P[x,y2] holds y1 = y2; A3: for x st x in Subgroups G ex y st P[x,y] proof let x; assume x in Subgroups G; then reconsider F = x as strict Subgroup of G by Def1; reconsider y = the carrier of F as set; take y; take F; thus thesis; end; consider f being Function such that A4: dom f = Subgroups G and A5: for x st x in Subgroups G holds P[x,f.x] from FuncEx(A2,A3); A6: rng f c= bool the carrier of G proof let x; assume x in rng f; then consider y such that A7: y in dom f & f.y = x by FUNCT_1:def 5; consider H being strict Subgroup of G such that A8: y = H & x = the carrier of H by A4,A5,A7; the carrier of H c= the carrier of G by GROUP_2:def 5; hence thesis by A8; end; f is one-to-one proof let x,y; assume that A9: x in dom f and A10: y in dom f and A11: f.x = f.y; A12: ex H1 being strict Subgroup of G st x = H1 & f.x = the carrier of H1 by A4,A5,A9; ex H2 being strict Subgroup of G st y = H2 & f.y = the carrier of H2 by A4,A5,A10; hence thesis by A11,A12,GROUP_2:68; end; then A13: Card Subgroups G <=` Card bool the carrier of G by A4,A6,CARD_1:26; the carrier of G is finite by A1,GROUP_1:def 13; then bool the carrier of G is finite by FINSET_1:24; hence thesis by A13,CARD_2:68; end; definition let G,a,b; func a |^ b -> Element of G equals :Def2: b" * a * b; correctness; end; theorem Th20: a |^ b = b" * a * b & a |^ b = b" * (a * b) proof thus a |^ b = b" * a * b by Def2; hence a |^ b = b" * (a * b) by VECTSP_1:def 16; end; theorem Th21: a |^ g = b |^ g implies a = b proof assume A1: a |^ g = b |^ g; a |^ g = g" * a * g & b |^ g = g" * b * g by Th20; then g" * a = g" * b by A1,GROUP_1:14; hence thesis by GROUP_1:14; end; theorem Th22: (1.G) |^ a = 1.G proof thus (1.G) |^ a = a" * 1.G * a by Def2 .= a" * a by GROUP_1:def 4 .= 1.G by GROUP_1:def 5; end; theorem Th23: a |^ b = 1.G implies a = 1.G proof assume a |^ b = 1.G; then 1.G = b" * a * b by Def2; then b" = b" * a by GROUP_1:20; hence thesis by GROUP_1:15; end; theorem Th24: a |^ 1.G = a proof thus a |^ 1.G = (1.G)" * (a * 1.G) by Th20 .= (1.G)" * a by GROUP_1:def 4 .= 1.G * a by GROUP_1:16 .= a by GROUP_1:def 4; end; theorem Th25: a |^ a = a proof thus a |^ a = a" * a * a by Th20 .= 1.G * a by GROUP_1:def 5 .= a by GROUP_1:def 4; end; theorem Th26: a |^ a" = a & a" |^ a = a" proof thus a |^ a" = a"" * a * a" by Th20 .= a * a * a" by GROUP_1:19 .= a by Th1; thus a" |^ a = a" * a" * a by Th20 .= a" by Th1; end; theorem Th27: a |^ b = a iff a * b = b * a proof thus a |^ b = a implies a * b = b * a proof assume a |^ b = a; then a = b" * (a * b) by Th20; hence thesis by GROUP_1:21; end; assume a * b = b * a; then a = b" * (a * b) by GROUP_1:21; hence thesis by Th20; end; theorem Th28: (a * b) |^ g = a |^ g * (b |^ g) proof thus (a * b) |^ g = g" * (a * b) * g by Def2 .= g" * (a * 1.G * b) * g by GROUP_1:def 4 .= g" * (a * (g * g") * b) * g by GROUP_1:def 5 .= g" * (a * g * g" * b) * g by VECTSP_1:def 16 .= g" * (a * g * (g" * b)) * g by VECTSP_1:def 16 .= g" * (a * g) * (g" * b) * g by VECTSP_1:def 16 .= g" * a * g * (g" * b) * g by VECTSP_1:def 16 .= a |^ g * (g" * b) * g by Def2 .= a |^ g * (g" * b * g) by VECTSP_1:def 16 .= a |^ g * (b |^ g) by Def2; end; theorem Th29: a |^ g |^ h = a |^ (g * h) proof thus a |^ g |^ h = h" * (a |^ g) * h by Def2 .= h" * (g" * a * g) * h by Def2 .= h" * (g" * a) * g * h by VECTSP_1:def 16 .= h" * g" * a * g * h by VECTSP_1:def 16 .= (g * h)" * a * g * h by GROUP_1:25 .= (g * h)" * a * (g * h) by VECTSP_1:def 16 .= a |^ (g * h) by Def2; end; theorem Th30: a |^ b |^ b" = a & a |^ b" |^ b = a proof thus a |^ b |^ b" = a |^ (b * b") by Th29 .= a |^ 1.G by GROUP_1:def 5 .= a by Th24; thus a |^ b" |^ b = a |^ (b" * b) by Th29 .= a |^ 1.G by GROUP_1:def 5 .= a by Th24; end; canceled; theorem Th32: a" |^ b = (a |^ b)" proof thus a" |^ b = b" * a" * b by Th20 .= (a * b)" * b by GROUP_1:25 .= (a * b)" * b"" by GROUP_1:19 .= (b" * (a * b))" by GROUP_1:25 .= (a |^ b)" by Th20; end; Lm2: now let G,a,b; thus a |^ 0 |^ b = (1.G) |^ b by GROUP_1:43 .= 1.G by Th22 .= (a |^ b) |^ 0 by GROUP_1:43; end; Lm3: now let n; assume A1: for G,a,b holds a |^ n |^ b = (a |^ b) |^ n; let G,a,b; thus a |^ (n + 1) |^ b = (a |^ n * a) |^ b by GROUP_1:49 .= (a |^ n |^ b) * (a |^ b) by Th28 .= ((a |^ b) |^ n) * (a |^ b) by A1 .= (a |^ b) |^ (n + 1) by GROUP_1:49; end; Lm4: for n,G,a,b holds a |^ n |^ b = (a |^ b) |^ n proof defpred P[Nat] means a |^ $1 |^ b = (a |^ b) |^ $1; A1: P[0] by Lm2; A2: for k be Nat st P[k] holds P[k+1] by Lm3; for k be Nat holds P[k] from Ind(A1,A2); hence thesis; end; theorem (a |^ n) |^ b = (a |^ b) |^ n by Lm4; theorem (a |^ i) |^ b = (a |^ b) |^ i proof per cases; suppose i >= 0; then i = abs i by ABSVALUE:def 1; hence a |^ i |^ b =(a |^ b) |^ i by Lm4; suppose A1: i < 0; hence a |^ i |^ b = (a |^ abs i)" |^ b by GROUP_1:56 .= (a |^ abs (i) |^ b)" by Th32 .= ((a |^ b) |^ abs i)" by Lm4 .= (a |^ b) |^ i by A1,GROUP_1:56; end; theorem Th35: G is commutative Group implies a |^ b = a proof assume A1: G is commutative Group; thus a |^ b = b" * a * b by Def2 .= a * b" * b by A1,Lm1 .= a by Th1; end; theorem Th36: (for a,b holds a |^ b = a) implies G is commutative proof assume A1: for a,b holds a |^ b = a; let a,b; a |^ b = a by A1; hence thesis by Th27; end; definition let G,A,B; func A |^ B -> Subset of G equals :Def3: {g |^ h : g in A & h in B}; coherence proof set X = {g |^ h : g in A & h in B}; X c= the carrier of G proof let x; assume x in X; then ex g,h st x = g |^ h & g in A & h in B; hence x in the carrier of G; end; hence thesis; end; end; canceled; theorem Th38: 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 Def3; hence thesis; end; given g,h such that A1: x = g |^ h & g in A & h in B; x in {a |^ b : a in A & b in B} by A1; hence thesis by Def3; end; theorem Th39: A |^ B <> {} iff A <> {} & B <> {} proof thus A |^ B <> {} implies A <> {} & B <> {} proof assume A1: A |^ B <> {}; consider x being Element of A |^ B; ex a,b st x = a |^ b & a in A & b in B by A1,Th38; hence thesis; end; assume A2: A <> {}; consider x being Element of A; assume A3: B <> {}; consider y being Element of B; reconsider x,y as Element of G by A2,A3,TARSKI:def 3; x |^ y in A |^ B by A2,A3,Th38; hence thesis; end; theorem Th40: A |^ B c= B" * A * B proof let x; assume x in A |^ B; then consider a,b such that A1: x = a |^ b & a in A & b in B by Th38; b" in B" by A1,GROUP_2:5; then b" * a in B" * A by A1,GROUP_2:12; then x = b" * a * b & b" * a * b in B" * A * B by A1,Th20,GROUP_2:12; hence thesis; end; theorem Th41: (A * B) |^ C c= A |^ C * (B |^ C) proof let x; assume x in (A * B) |^ C; then consider a,b such that A1: x = a |^ b & a in A * B & b in C by Th38; consider g,h such that A2: a = g * h & g in A & h in B by A1,GROUP_2:12; x = (g |^ b) * (h |^ b) & g |^ b in A |^ C & h |^ b in B |^ C by A1,A2,Th28,Th38; hence thesis by GROUP_2:12; end; theorem Th42: A |^ B |^ C = A |^ (B * C) proof thus A |^ B |^ C c= A |^ (B * C) proof let x; assume x in A |^ B |^ C; then consider a,c such that A1: x = a |^ c & a in A |^ B & c in C by Th38; consider g,h such that A2: a = g |^ h & g in A & h in B by A1,Th38; x = g |^ (h * c) & h * c in B * C by A1,A2,Th29,GROUP_2:12; hence thesis by A2,Th38; end; let x; assume x in A |^ (B * C); then consider a,b such that A3: x = a |^ b & a in A & b in B * C by Th38; consider g,h such that A4: b = g * h & g in B & h in C by A3,GROUP_2:12; a |^ g in A |^ B by A3,A4,Th38; then x = a |^ g |^ h & a |^ g |^ h in A |^ B |^ C by A3,A4,Th29,Th38; hence thesis; end; theorem A" |^ B = (A |^ B)" proof thus A" |^ B c= (A |^ B)" proof let x; assume x in A" |^ B; then consider a,b such that A1: x = a |^ b & a in A" & b in B by Th38; consider c such that A2: a = c" & c in A by A1,GROUP_2:5; x = (c |^ b)" & c |^ b in A |^ B by A1,A2,Th32,Th38; hence thesis by GROUP_2:5; end; let x; assume x in (A |^ B)"; then consider a such that A3: x = a" & a in A |^ B by GROUP_2:5; consider b,c such that A4: a = b |^ c & b in A & c in B by A3,Th38; x = b" |^ c & b" in A" by A3,A4,Th32,GROUP_2:5; hence thesis by A4,Th38; end; theorem Th44: {a} |^ {b} = {a |^ b} proof A1: {a} |^ {b} c= {b}" * {a} * {b} by Th40; A2: {b}" * {a} * {b} = {b"} * {a} * {b} by GROUP_2:6 .= {b" * a} * {b} by GROUP_2:22 .= {b" * a * b} by GROUP_2:22 .= {a |^ b} by Th20; {a} |^ {b} <> {} by Th39; hence thesis by A1,A2,ZFMISC_1:39; 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 g,h such that A1: x = g |^ h & g in {a} & h in{b,c} by Th38; g = a & (h = b or h = c) by A1,TARSKI:def 1,def 2; hence thesis by A1,TARSKI:def 2; end; let x; assume x in {a |^ b,a |^ c}; then (x = a |^ b or x = a |^ c) & a in {a} & b in {b,c} & c in {b,c} by TARSKI:def 1,def 2; hence thesis by Th38; 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 g,h such that A1: x = g |^ h & g in {a,b} & h in {c} by Th38; h = c & (g = b or g = a) by A1,TARSKI:def 1,def 2; hence thesis by A1,TARSKI:def 2; end; let x; assume x in {a |^ c,b |^ c}; then (x = a |^ c or x = b |^ c) & a in {a,b} & b in {a,b} & c in {c} by TARSKI:def 1,def 2; hence thesis by Th38; end; theorem {a,b} |^ {c,d} = {a |^ c,a |^ d,b |^ c,b |^ d} proof thus {a,b} |^ {c,d} c= {a |^ c,a |^ d,b |^ c,b |^ d} proof let x; assume x in {a,b} |^ {c,d}; then consider g,h such that A1: x = g |^ h & g in {a,b} & h in {c,d} by Th38; (g = a or g = b) & (h = c or h = d) by A1,TARSKI:def 2; hence thesis by A1,ENUMSET1:19; end; let x; assume x in {a |^ c,a |^ d,b |^ c,b |^ d}; then (x = a |^ c or x = a |^ d or x = b |^ c or x = b |^ d) & a in {a,b} & b in {a,b} & c in {c,d} & d in {c,d} by ENUMSET1:18,TARSKI:def 2; hence thesis by Th38; end; definition let G,A,g; func A |^ g -> Subset of G equals :Def4: A |^ {g}; correctness; func g |^ A -> Subset of G equals :Def5: {g} |^ A; correctness; end; canceled 2; theorem Th50: 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 a,b such that A1: x = a |^ b & a in A & b in {g} by Th38; b = 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,Th38; hence thesis by Def4; end; theorem Th51: 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 Def5; then consider a,b such that A1: x = a |^ b & a in {g} & b in A by Th38; a = 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,Th38; hence thesis by Def5; end; theorem g |^ A c= A" * g * A proof let x; assume x in g |^ A; then consider a such that A1: x = g |^ a & a in A by Th51; a" in A" by A1,GROUP_2:5; then a" * g in A" * g by GROUP_2:34; then a" * g * a in A" * g * A by A1,GROUP_2:12; hence thesis by A1,Th20; end; theorem Th53: A |^ B |^ g = A |^ (B * g) proof thus A |^ B |^ g = A |^ B |^ {g} by Def4 .= A |^ (B * {g}) by Th42 .= A |^ (B * g) by GROUP_2:def 4; end; theorem Th54: A |^ g |^ B = A |^ (g * B) proof thus A |^ g |^ B = A |^ {g} |^ B by Def4 .= A |^ ({g} * B) by Th42 .= A |^ (g * B) by GROUP_2:def 3; end; theorem g |^ A |^ B = g |^ (A * B) proof thus g |^ A |^ B = {g} |^ A |^ B by Def5 .= {g} |^ (A * B) by Th42 .= g |^ (A * B) by Def5; end; theorem Th56: A |^ a |^ b = A |^ (a * b) proof thus A |^ a |^ b = A |^ a |^ {b} by Def4 .= A |^ (a * {b}) by Th54 .= A |^ ({a} * {b}) by GROUP_2:def 3 .= A |^ {a * b} by GROUP_2:22 .= A |^ (a * b) by Def4; end; theorem a |^ A |^ b = a |^ (A * b) proof thus a |^ A |^ b = {a} |^ A |^ b by Def5 .= {a} |^ (A * b) by Th53 .= a |^ (A * b) by Def5; end; theorem a |^ b |^ A = a |^ (b * A) proof thus a |^ b |^ A = {a |^ b} |^ A by Def5 .= {a} |^ {b} |^ A by Th44 .= {a} |^ ({b} * A) by Th42 .= a |^ ({b} * A) by Def5 .= a |^ (b * A) by GROUP_2:def 3; end; theorem Th59: A |^ g = g" * A * g proof A |^ g = A |^ {g} by Def4; then A |^ g c= {g}" * A * {g} by Th40; then A |^ g c= {g"} * A * {g} by GROUP_2:6; then A |^ g c= {g"} * A * g by GROUP_2:def 4; hence A |^ g c= g" * A * g by GROUP_2:def 3; let x; assume x in g" * A * g; then consider a such that A1: x = a * g & a in g" * A by GROUP_2:34; consider b such that A2: a = g" * b & b in A by A1,GROUP_2:33; x = b |^ g by A1,A2,Th20; hence thesis by A2,Th50; end; theorem (A * B) |^ a c= (A |^ a) * (B |^ a) proof A1: (A * B) |^ a = (A * B) |^ {a} by Def4; A |^ a = A |^ {a} & B |^ a = B |^ {a} by Def4; hence thesis by A1,Th41; end; theorem Th61: A |^ 1.G = A proof thus A |^ 1.G = (1.G)" * A * 1.G by Th59 .= (1.G)" * A by GROUP_2:43 .= 1.G * A by GROUP_1:16 .= A by GROUP_2:43; end; theorem A <> {} implies (1.G) |^ A = {1.G} proof assume A1: A <> {}; thus (1.G) |^ A c= {1.G} proof let x; assume x in (1.G) |^ A; then ex a st x = (1.G) |^ a & a in A by Th51; then x = 1.G by Th22; hence thesis by TARSKI:def 1; end; let x; assume x in {1.G}; then A2: x = 1.G by TARSKI:def 1; consider y being Element of A; reconsider y as Element of G by A1,TARSKI:def 3; (1.G) |^ y = x by A2,Th22; hence thesis by A1,Th51; end; theorem Th63: A |^ a |^ a" = A & A |^ a" |^ a = A proof thus A |^ a |^ a" = A |^ (a * a") by Th56 .= A |^ 1.G by GROUP_1:def 5 .= A by Th61; thus A |^ a" |^ a = A |^ (a" * a) by Th56 .= A |^ 1.G by GROUP_1:def 5 .= A by Th61; end; canceled; theorem Th65: G is commutative Group iff for A,B st B <> {} holds A |^ B = A proof thus G is commutative Group implies for A,B st B <> {} holds A |^ B = A proof assume A1: G is commutative Group; let A,B; assume A2: B <> {}; thus A |^ B c= A proof let x; assume x in A |^ B; then ex a,b st x = a |^ b & a in A & b in B by Th38; hence thesis by A1,Th35; end; let x; assume A3: x in A; then reconsider a = x as Element of G; consider y being Element of B; reconsider y as Element of G by A2,TARSKI:def 3; a |^ y = x by A1,Th35; hence thesis by A2,A3,Th38; end; assume A4: for A,B st B <> {} holds A |^ B = A; now let a,b; {a} = {a} |^ {b} by A4 .= {a |^ b} by Th44; hence a = a |^ b by ZFMISC_1:6; end; hence thesis by Th36; end; theorem G is commutative Group iff for A,g holds A |^ g = A proof thus G is commutative Group implies for A,g holds A |^ g = A proof assume A1: G is commutative Group; let A,g; A |^ {g} = A by A1,Th65; hence thesis by Def4; end; assume A2: for A,g holds A |^ g = A; now let a,b; {a} = {a} |^ b by A2 .= {a} |^ {b} by Def4 .= {a |^ b} by Th44; hence a = a |^ b by ZFMISC_1:6; end; hence thesis by Th36; end; theorem G is commutative Group iff for A,g st A <> {} holds g |^ A = {g} proof thus G is commutative Group implies for A,g st A <> {} holds g |^ A = {g} proof assume A1: G is commutative Group; let A,g; assume A <> {}; then {g} |^ A = {g} by A1,Th65; hence thesis by Def5; end; assume A2: for A,g st A <> {} holds g |^ A = {g}; now let a,b; {a} = a |^ {b} by A2 .= {a} |^ {b} by Def5 .= {a |^ b} by Th44; hence a = a |^ b by ZFMISC_1:6; end; hence thesis by Th36; end; definition let G,H,a; func H |^ a -> strict Subgroup of G means :Def6: the carrier of it = carr(H) |^ a; existence proof consider H1 being strict Subgroup of G such that A1: the carrier of H1 = a" * H * a"" by GROUP_2:150; the carrier of H1 = a" * H * a by A1,GROUP_1:19 .= a" * carr H * a by GROUP_2:def 13 .= carr(H) |^ a by Th59; hence thesis; end; correctness by GROUP_2:68; end; canceled 2; theorem Th70: 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 the carrier of H |^ a by RLVECT_1:def 1; then x in carr H |^ a by Def6; then consider b such that A1: x = b |^ a and A2: b in carr H by Th50; take b; thus thesis by A1,A2,GROUP_2:88; end; given g such that A3: x = g |^ a & g in H; g in carr H by A3,GROUP_2:88; then x in carr H |^ a by A3,Th50; then x in the carrier of H |^ a by Def6; hence thesis by RLVECT_1:def 1; end; theorem Th71: the carrier of H |^ a = a" * H * a proof thus the carrier of H |^ a = carr(H) |^ a by Def6 .= a" * carr H * a by Th59 .= a" * H * a by GROUP_2:def 13; end; theorem Th72: H |^ a |^ b = H |^ (a * b) proof A1: carr(H |^ a) = the carrier of H |^ a by GROUP_2:def 9; the carrier of H |^ a |^ b = carr(H |^ a) |^ b by Def6 .= (carr H |^ a) |^ b by A1,Def6 .= carr H |^ (a * b) by Th56 .= the carrier of H |^ (a * b) by Def6; hence thesis by GROUP_2:68; end; theorem Th73: for H being strict Subgroup of G holds H |^ 1.G = H proof let H be strict Subgroup of G; the carrier of H |^ 1.G = carr H |^ 1.G by Def6 .= carr H by Th61 .= the carrier of H by GROUP_2:def 9; hence thesis by GROUP_2:68; end; theorem Th74: for H being strict Subgroup of G holds H |^ a |^ a" = H & H |^ a" |^ a = H proof let H be strict Subgroup of G; thus H |^ a |^ a" = H |^ (a * a") by Th72 .= H |^ 1.G by GROUP_1:def 5 .= H by Th73; thus H |^ a" |^ a = H |^ (a" * a) by Th72 .= H |^ 1.G by GROUP_1:def 5 .= H by Th73; end; canceled; theorem Th76: (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a) proof let g; thus g in (H1 /\ H2) |^ a implies g in (H1 |^ a) /\ (H2 |^ a) proof assume g in (H1 /\ H2) |^ a; then consider h such that A1: g = h |^ a & h in H1 /\ H2 by Th70; h in H1 & h in H2 by A1,GROUP_2:99; then g in H1 |^ a & g in H2 |^ a by A1,Th70; hence thesis by GROUP_2:99; end; assume A2: g in (H1 |^ a) /\ (H2 |^ a); then g in H1 |^ a by GROUP_2:99; then consider b such that A3: g = b |^ a & b in H1 by Th70; g in H2 |^ a by A2,GROUP_2:99; then consider c such that A4: g = c |^ a & c in H2 by Th70; b = c by A3,A4,Th21; then b in (H1 /\ H2) by A3,A4,GROUP_2:99; hence thesis by A3,Th70; end; theorem Th77: Ord H = Ord(H |^ a) proof deffunc F(Element of G) = $1 |^ a; consider f being Function of the carrier of G, the carrier of G such that A1: for g holds f.g = F(g) from LambdaD; set g = f | (the carrier of H); A2: dom f = the carrier of G & the carrier of H c= the carrier of G by FUNCT_2:def 1,GROUP_2:def 5; then A3: dom g = the carrier of H by RELAT_1:91; A4: rng g = the carrier of H |^ a proof A5: the carrier of H = carr H by GROUP_2:def 9; thus rng g c= the carrier of H |^ a proof let x; assume x in rng g; then consider y such that A6: y in dom g and A7: g.y = x by FUNCT_1:def 5; reconsider y as Element of H by A2,A6,RELAT_1:91; reconsider y as Element of G by GROUP_2:51; f.y = y |^ a & f.y = g.y by A1,A6,FUNCT_1:70; then x in carr H |^ a by A5,A7,Th50; hence thesis by Def6; end; let x; assume x in the carrier of H |^ a; then x in carr H |^ a by Def6; then consider b such that A8: x = b |^ a and A9: b in carr H by Th50; g.b = f.b & f.b = b |^ a by A1,A3,A5,A9,FUNCT_1:70; hence thesis by A3,A5,A8,A9,FUNCT_1:def 5; end; g is one-to-one proof let x,y; assume that A10: x in dom g & y in dom g and A11: g.x = g.y; reconsider b = x, c = y as Element of H by A2,A10,RELAT_1:91; reconsider b,c as Element of G by GROUP_2:51; f.x = g.x & f.y = g.y & f.x = b |^ a & f.y = c |^ a by A1,A10,FUNCT_1:70; hence thesis by A11,Th21; end; then the carrier of H,the carrier of H |^ a are_equipotent by A3,A4,WELLORD2:def 4; then Card the carrier of H = Card the carrier of H |^ a by CARD_1:21; then Card the carrier of H = Ord(H |^ a) by GROUP_1:def 12; hence thesis by GROUP_1:def 12; end; theorem Th78: H is finite iff H |^ a is finite proof Ord H = Card the carrier of H & Ord H = Ord(H |^ a) & Ord(H |^ a) = Card the carrier of H |^ a by Th77,GROUP_1:def 12; then the carrier of H,the carrier of H |^ a are_equipotent by CARD_1:21; then the carrier of H is finite iff the carrier of H |^ a is finite by CARD_1:68; hence thesis by GROUP_1:def 13; end; theorem Th79: H is finite implies ord H = ord(H |^ a) proof assume A1: H is finite; then H |^ a is finite by Th78; then consider C being finite set such that A2: C = the carrier of H |^ a & ord(H |^ a) = card C by GROUP_1:def 14; consider B being finite set such that A3: B = the carrier of H & ord H = card B by A1,GROUP_1:def 14; Ord H = Card the carrier of H & Ord H = Ord(H |^ a) & Ord(H |^ a) = Card the carrier of H |^ a by Th77,GROUP_1:def 12; hence thesis by A2,A3; end; theorem Th80: (1).G |^ a = (1).G proof A1: the carrier of (1).G = {1.G} & carr (1).G = the carrier of (1).G by GROUP_2:def 7,def 9; the carrier of (1).G |^ a = (carr (1).G) |^ a by Def6 .= {1.G} |^ {a} by A1,Def4 .= {(1.G) |^ a} by Th44 .= {1.G} by Th22; hence thesis by GROUP_2:def 7; end; theorem for H being strict Subgroup of G holds H |^ a = (1).G implies H = (1).G proof let H be strict Subgroup of G; assume A1: H |^ a = (1).G; A2: (1).G is finite & ord (1).G = 1 by GROUP_2:80,81; then A3: H is finite by A1,Th78; then ord H = 1 by A1,A2,Th79; hence thesis by A3,GROUP_2:82; end; theorem Th82: for G being Group, a being Element of G holds (Omega).G |^ a = (Omega).G proof let G be Group, a be Element of G; A1: (Omega).G = the HGrStr of G by GROUP_2:def 8; let h be Element of G; A2: (h |^ a") |^ a = h |^ (a" * a) by Th29 .= h |^ 1.G by GROUP_1:def 5 .= h by Th24; h |^ a" in the HGrStr of G by RLVECT_1:def 1; hence h in (Omega).G |^ a iff h in (Omega).G by A1,A2,Th70,RLVECT_1:def 1 ; end; theorem for H being strict Subgroup of G holds H |^ a = G implies H = G proof let H be strict Subgroup of G; assume A1: H |^ a = G; now let g; assume A2: not g in H; now assume g |^ a in H |^ a; then ex h st g |^ a = h |^ a & h in H by Th70; hence contradiction by A2,Th21; end; hence contradiction by A1,RLVECT_1:def 1; end; hence thesis by A1,GROUP_2:71; end; theorem Th84: Index H = Index(H |^ a) proof defpred P[set,set] means ex b st $1 = b * H & $2 = (b |^ a) * (H |^ a); A1: for x,y1,y2 st x in Left_Cosets H & P[x,y1] & P[x,y2] holds y1 = y2 proof let x,y1,y2; set A = carr H; assume x in Left_Cosets H; given b such that A2: x = b * H & y1 = (b |^ a) * (H |^ a); given c such that A3: x = c * H & y2 = (c |^ a) * (H |^ a); A4: the carrier of H |^ a = carr(H |^ a) by GROUP_2:def 9; thus y1 = (a" * b * a) * (H |^ a) by A2,Th20 .= (a" * b * a) * carr(H |^ a) by GROUP_2:def 13 .= (a" * b * a) * (a" * H * a) by A4,Th71 .= (a" * b * a) * (a" * A * a) by GROUP_2:def 13 .= (a" * b * a) * (a" * A) * a by GROUP_2:39 .= (a" * b) * (a * (a" * A)) * a by GROUP_2:38 .= a" * b * (a * a" * A) * a by GROUP_2:38 .= a" * b * (1.G * A) * a by GROUP_1:def 5 .= a" * b * A * a by GROUP_2:43 .= a" * (b * A) * a by GROUP_2:38 .= a" * (c * H) * a by A2,A3,GROUP_2:def 13 .= a" * (c * A) * a by GROUP_2:def 13 .= a" * c * A * a by GROUP_2:38 .= a" * c * (1.G * A) * a by GROUP_2:43 .= a" * c * (a * a" * A) * a by GROUP_1:def 5 .= (a" * c) * (a * (a" * A)) * a by GROUP_2:38 .= (a" * c * a) * (a" * A) * a by GROUP_2:38 .= (a" * c * a) * (a" * A * a) by GROUP_2:39 .= (a" * c * a) * (a" * H * a) by GROUP_2:def 13 .= (a" * c * a) * carr(H |^ a) by A4,Th71 .= (a" * c * a) * (H |^ a) by GROUP_2:def 13 .= y2 by A3,Th20; end; A5: 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 b such that A6: x = b * H by GROUP_2:def 15; reconsider y = (b |^ a) * (H |^ a) as set; take y; take b; thus thesis by A6; end; consider f being Function such that A7: dom f = Left_Cosets H and A8: for x st x in Left_Cosets H holds P[x,f.x] from FuncEx(A1,A5); A9: rng f = Left_Cosets(H |^ a) proof thus rng f c= Left_Cosets(H |^ a) proof let x; assume x in rng f; then consider y such that A10: y in dom f & f.y = x by FUNCT_1:def 5 ; ex b st y = b * H & x = (b |^ a) * (H |^ a) by A7,A8,A10; hence thesis by GROUP_2:def 15; end; let x; assume x in Left_Cosets(H |^ a); then consider b such that A11: x = b * (H |^ a) by GROUP_2:def 15; set c = b |^ a"; A12: x = (c |^ a) * (H |^ a) by A11,Th30; A13: c * H in Left_Cosets H by GROUP_2:def 15; then consider d such that A14: c * H = d * H & f.(c * H) = (d |^ a) * (H |^ a) by A8; (c |^ a) * (H |^ a) = (d |^ a) * (H |^ a) by A1,A13,A14; hence thesis by A7,A12,A13,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 b such that A18: x = b * H and A19: f.x = (b |^ a) * (H |^ a) by A7,A8, A15; consider c such that A20: y = c * H and A21: f.y = (c |^ a) * (H |^ a) by A7,A8, A16; A22: (c |^ a)" * (b |^ a) in H |^ a by A17,A19,A21,GROUP_2:137; (c |^ a)" * (b |^ a) = (c" |^ a) * (b |^ a) by Th32 .= (c" * b) |^ a by Th28; then consider d such that A23: (c" * b) |^ a = d |^ a & d in H by A22,Th70; c" * b = d by A23,Th21; hence thesis by A18,A20,A23,GROUP_2:137; end; then A24: Left_Cosets H,Left_Cosets(H |^ a) are_equipotent by A7,A9,WELLORD2:def 4; thus Index H = Card Left_Cosets H by GROUP_2:175 .= Card Left_Cosets(H |^ a) by A24,CARD_1:21 .= Index(H |^ a) by GROUP_2:175; end; theorem Left_Cosets H is finite implies index H = index(H |^ a) proof assume Left_Cosets H is finite; then consider B being finite set such that A1: B = Left_Cosets H & index H = card B by GROUP_2:def 18; A2: Index H = Card Left_Cosets H & Index(H |^ a) = Card Left_Cosets(H|^ a) & Index H = Index(H |^ a) by Th84,GROUP_2:175; then Left_Cosets H,Left_Cosets(H |^ a) are_equipotent by CARD_1:21; then Left_Cosets(H |^ a) is finite by A1,CARD_1:68; then consider C being finite set such that A3: C = Left_Cosets(H |^ a) & index(H |^ a) = card C by GROUP_2:def 18; thus thesis by A1,A2,A3; end; theorem Th86: G is commutative Group implies for H being strict Subgroup of G for a holds H |^ a = H proof assume A1: G is commutative Group; let H be strict Subgroup of G; let a; the carrier of H |^ a = a" * H * a by Th71 .= H * a" * a by A1,GROUP_2:135 .= H * (a" * a) by GROUP_2:129 .= H * 1.G by GROUP_1:def 5 .= carr H by GROUP_2:132 .= the carrier of H by GROUP_2:def 9; hence thesis by GROUP_2:68; end; definition let G,a,b; pred a,b are_conjugated means :Def7: ex g st a = b |^ g; antonym a,b are_not_conjugated; end; canceled; theorem Th88: a,b are_conjugated iff ex g st b = a |^ g proof thus a,b are_conjugated implies ex g st b = a |^ g proof given g such that A1: a = b |^ g; a |^ g" = b by A1,Th30; hence thesis; end; given g such that A2: b = a |^ g; a = b |^ g" by A2,Th30; hence thesis by Def7; end; theorem Th89: a,a are_conjugated proof take 1.G; thus thesis by Th24; end; theorem Th90: a,b are_conjugated implies b,a are_conjugated proof given g such that A1: a = b |^ g; b = a |^ g" by A1,Th30; hence thesis by Def7; end; definition let G,a,b; redefine pred a,b are_conjugated; reflexivity by Th89; symmetry by Th90; end; theorem Th91: a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated proof given g such that A1: a = b |^ g; given h such that A2: b = c |^ h; a = c |^ (h * g) by A1,A2,Th29; hence thesis by Def7; end; theorem Th92: a,1.G are_conjugated or 1.G,a are_conjugated implies a = 1.G proof assume A1: a,1.G are_conjugated or 1.G,a are_conjugated; now per cases by A1; suppose a,1.G are_conjugated; then ex g st 1.G = a |^ g by Th88; hence thesis by Th23; suppose 1.G,a are_conjugated; then ex g st 1.G = a |^ g by Def7; hence thesis by Th23; end; hence thesis; end; theorem Th93: a |^ carr (Omega).G = {b : a,b are_conjugated} proof set A = a |^ carr (Omega).G; set B = {b : a,b are_conjugated}; thus A c= B proof let x; assume A1: x in A; then A2: ex g st x = a |^ g & g in carr(Omega).G by Th51; reconsider b = x as Element of G by A1; b,a are_conjugated by A2,Def7; hence thesis; end; let x; assume x in B; then consider b such that A3: x = b & a,b are_conjugated; b,a are_conjugated by A3; then consider g such that A4: b = a |^ g by Def7; g in the HGrStr of G by RLVECT_1:def 1; then g in (Omega).G by GROUP_2:def 8; then g in carr (Omega).G by GROUP_2:88; hence thesis by A3,A4,Th51; end; definition let G,a; func con_class a -> Subset of G equals :Def8: a |^ carr (Omega).G; correctness; end; canceled; theorem Th95: x in con_class a iff ex b st b = x & a,b are_conjugated proof thus x in con_class a implies ex b st b = x & a,b are_conjugated proof assume x in con_class a; then x in a |^ carr (Omega).G by Def8; then x in {b : a,b are_conjugated} by Th93; hence thesis; end; given b such that A1: b = x & a,b are_conjugated; x in {c : a,c are_conjugated} by A1; then x in a |^ carr (Omega).G by Th93; hence thesis by Def8; end; theorem Th96: a in con_class b iff a,b are_conjugated proof thus a in con_class b implies a,b are_conjugated proof assume a in con_class b; then ex c st a = c & b,c are_conjugated by Th95; hence thesis; end; assume a,b are_conjugated; hence thesis by Th95; end; theorem Th97: a |^ g in con_class a proof a,a |^ g are_conjugated by Th88; hence thesis by Th95; end; theorem a in con_class a by Th96; theorem a in con_class b implies b in con_class a proof assume a in con_class b; then a,b are_conjugated by Th96; hence thesis by Th96; end; theorem con_class a = con_class b iff con_class a meets con_class b proof thus con_class a = con_class b implies con_class a meets con_class b proof assume con_class a = con_class b; then a in con_class b & a in con_class a by Th96; hence thesis by XBOOLE_0:3; end; assume con_class a meets con_class b; then consider x such that A1: x in con_class a & x in con_class b by XBOOLE_0:3; reconsider x as Element of G by A1; thus con_class a c= con_class b proof let y; assume y in con_class a; then consider g such that A2: g = y & a,g are_conjugated by Th95; x,a are_conjugated & x,b are_conjugated by A1,Th96; then x,g are_conjugated & b,x are_conjugated by A2,Th91; then b,g are_conjugated by Th91; hence thesis by A2,Th95; end; let y; assume y in con_class b; then consider g such that A3: g = y & b,g are_conjugated by Th95; x,b are_conjugated & x,a are_conjugated by A1,Th96; then a,x are_conjugated & x,g are_conjugated by A3,Th91; then a,g are_conjugated by Th91; hence thesis by A3,Th95; end; theorem con_class a = {1.G} iff a = 1.G proof thus con_class a = {1.G} implies a = 1.G proof assume A1: con_class a = {1.G}; a in con_class a by Th96; hence thesis by A1,TARSKI:def 1; end; assume A2: a = 1.G; thus con_class a c= {1.G} proof let x; assume x in con_class a; then consider b such that A3: b = x & a,b are_conjugated by Th95; b = 1.G by A2,A3,Th92; hence thesis by A3,TARSKI:def 1; end; 1.G in con_class a by A2,Th96; hence thesis by ZFMISC_1:37; end; theorem con_class a * A = A * con_class a proof thus con_class a * A c= A * con_class a proof let x; assume x in con_class a * A; then consider b,c such that A1: x = b * c & b in con_class a & c in A by GROUP_2:12; b,a are_conjugated by A1,Th96; then consider g such that A2: b = a |^ g by Def7; reconsider h = x as Element of G by A1; h |^ c" = c"" * ((a |^ g) * c) * c" by A1,A2,Th20 .= c * ((a |^ g) * c) * c" by GROUP_1:19 .= c * (((a |^ g) * c) * c") by VECTSP_1:def 16 .= c * (a |^ g) by Th1; then A3: x = (c * (a |^ g)) |^ c by Th30 .= (c |^ c) * (a |^ g |^ c) by Th28 .= c * (a |^ g |^ c) by Th25 .= c * (a |^ (g * c)) by Th29; a |^ (g * c) in con_class a by Th97; hence thesis by A1,A3,GROUP_2:12; end; let x; assume x in A * con_class a; then consider b,c such that A4: x = b * c & b in A & c in con_class a by GROUP_2:12; c,a are_conjugated by A4,Th96; then consider g such that A5: c = a |^ g by Def7; reconsider h = x as Element of G by A4; h |^ b = b" * (b * (a |^ g)) * b by A4,A5,Th20 .= (a |^ g) * b by Th1; then A6: x = ((a |^ g) * b) |^ b" by Th30 .= (a |^ g) |^ b" * (b |^ b") by Th28 .= a |^ (g * b") * (b |^ b") by Th29 .= a |^ (g * b") * b by Th26; a |^ (g * b") in con_class a by Th97; hence thesis by A4,A6,GROUP_2:12; end; definition let G,A,B; pred A,B are_conjugated means :Def9: ex g st A = B |^ g; antonym A,B are_not_conjugated; end; canceled; theorem Th104: A,B are_conjugated iff ex g st B = A |^ g proof thus A,B are_conjugated implies ex g st B = A |^ g proof given g such that A1: A = B |^ g; A |^ g" = B by A1,Th63; hence thesis; end; given g such that A2: B = A |^ g; A = B |^ g" by A2,Th63; hence thesis by Def9; end; theorem Th105: A,A are_conjugated proof take 1.G; thus thesis by Th61; end; theorem Th106: A,B are_conjugated implies B,A are_conjugated proof given g such that A1: A = B |^ g; B = A |^ g" by A1,Th63; hence thesis by Def9; end; definition let G,A,B; redefine pred A,B are_conjugated; reflexivity by Th105; symmetry by Th106; end; theorem Th107: A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated proof given g such that A1: A = B |^ g; given h such that A2: B = C |^ h; A = C |^ (h * g) by A1,A2,Th56; hence thesis by Def9; end; theorem Th108: {a},{b} are_conjugated iff a,b are_conjugated proof thus {a},{b} are_conjugated implies a,b are_conjugated proof assume {a},{b} are_conjugated; then consider g such that A1: {a} |^ g = {b} by Th104; {b} = {a} |^ {g} by A1,Def4 .= {a |^ g} by Th44; then b = a |^ g by ZFMISC_1:6; hence thesis by Th88; end; assume a,b are_conjugated; then consider g such that A2: a |^ g = b by Th88; {b} = {a} |^ {g} by A2,Th44 .= {a} |^ g by Def4; hence thesis by Th104; end; theorem Th109: A,carr H1 are_conjugated implies ex H2 being strict Subgroup of G st the carrier of H2 = A proof assume A,carr H1 are_conjugated; then consider g such that A1: A = carr H1 |^ g by Def9; A = the carrier of H1 |^ g by A1,Def6; hence thesis; end; definition let G,A; func con_class A -> Subset-Family of G equals :Def10: {B : A,B are_conjugated}; coherence proof set X = {B: A,B are_conjugated}; X c= bool the carrier of G proof let x; assume x in X; then ex B st x = B & A,B are_conjugated; hence thesis; end; hence thesis by SETFAM_1:def 7; end; end; canceled; theorem Th111: x in con_class A iff ex B st x = B & A,B are_conjugated proof thus x in con_class A implies ex B st x = B & A,B are_conjugated proof assume x in con_class A; then x in {B : A,B are_conjugated} by Def10; hence thesis; end; given B such that A1: x = B & A,B are_conjugated; x in {C : A,C are_conjugated} by A1; hence thesis by Def10; end; canceled; theorem Th113: A in con_class B iff A,B are_conjugated proof thus A in con_class B implies A,B are_conjugated proof assume A in con_class B; then ex C st A = C & B,C are_conjugated by Th111; hence thesis; end; assume A,B are_conjugated; hence thesis by Th111; end; theorem A |^ g in con_class A proof A,A |^ g are_conjugated by Th104; hence thesis by Th111; end; theorem A in con_class A by Th111; theorem A in con_class B implies B in con_class A proof assume A in con_class B; then A,B are_conjugated by Th113; hence thesis by Th113; end; theorem con_class A = con_class B iff con_class A meets con_class B proof thus con_class A = con_class B implies con_class A meets con_class B proof assume con_class A = con_class B; then A in con_class B & A in con_class A by Th111; hence thesis by XBOOLE_0:3; end; assume con_class A meets con_class B; then consider x such that A1: x in con_class A & x in con_class B by XBOOLE_0:3; reconsider x as Subset of G by A1; thus con_class A c= con_class B proof let y; assume y in con_class A; then consider C such that A2: C = y & A,C are_conjugated by Th111; x,A are_conjugated & x,B are_conjugated by A1,Th113; then x,C are_conjugated & B,x are_conjugated by A2,Th107; then B,C are_conjugated by Th107; hence thesis by A2,Th111; end; let y; assume y in con_class B; then consider C such that A3: C = y & B,C are_conjugated by Th111; x,B are_conjugated & x,A are_conjugated by A1,Th113; then A,x are_conjugated & x,C are_conjugated by A3,Th107; then A,C are_conjugated by Th107; hence thesis by A3,Th111; end; theorem Th118: con_class{a} = {{b} : b in con_class a} proof set A = {{b} : b in con_class a}; thus con_class{a} c= A proof let x; assume x in con_class{a}; then consider B such that A1: x = B & {a},B are_conjugated by Th111; consider b such that A2: {a} |^ b = B by A1,Th104; A3: B = {a} |^ {b} by A2,Def4 .= {a |^ b} by Th44; a,a |^ b are_conjugated by Th88; then a |^ b in con_class a by Th96; hence thesis by A1,A3; end; let x; assume x in A; then consider b such that A4: x = {b} & b in con_class a; b,a are_conjugated by A4,Th96; then {b},{a} are_conjugated by Th108; hence thesis by A4,Th113; end; theorem G is finite implies con_class A is finite proof assume G is finite; then the carrier of G is finite by GROUP_1:def 13; then con_class A c= bool the carrier of G & bool the carrier of G is finite by FINSET_1:24; hence thesis by FINSET_1:13; end; definition let G,H1,H2; pred H1,H2 are_conjugated means :Def11: ex g st the HGrStr of H1 = H2 |^ g; antonym H1,H2 are_not_conjugated; end; canceled; theorem Th121: for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated iff ex g st H2 = H1 |^ g proof let H1,H2 be strict Subgroup of G; thus H1,H2 are_conjugated implies ex g st H2 = H1 |^ g proof given g such that A1: the HGrStr of H1 = H2 |^ g; H1 |^ g" = H2 by A1,Th74; hence thesis; end; given g such that A2: H2 = H1 |^ g; H1 = H2 |^ g" by A2,Th74; hence thesis by Def11; end; theorem Th122: for H1 being strict Subgroup of G holds H1,H1 are_conjugated proof let H1 be strict Subgroup of G; take 1.G; thus thesis by Th73; end; theorem Th123: for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated implies H2,H1 are_conjugated proof let H1,H2 be strict Subgroup of G; given g such that A1: the HGrStr of H1 = H2 |^ g; H2 = H1 |^ g" by A1,Th74; hence thesis by Def11; end; definition let G; let H1,H2 be strict Subgroup of G; redefine pred H1,H2 are_conjugated; reflexivity by Th122; symmetry by Th123; end; theorem Th124: for H1,H2 being strict Subgroup of G holds H1,H2 are_conjugated & H2,H3 are_conjugated implies H1,H3 are_conjugated proof let H1,H2 be strict Subgroup of G; given g such that A1: the HGrStr of H1 = H2 |^ g; given h such that A2: the HGrStr of H2 = H3 |^ h; H1 = H3 |^ (h * g) by A1,A2,Th72; hence thesis by Def11; end; reserve L for Subset of Subgroups G; definition let G,H; func con_class H -> Subset of Subgroups G means :Def12: x in it iff ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated; existence proof defpred P[set] means ex H1 being strict Subgroup of G st $1 = H1 & H,H1 are_conjugated; consider L such that A1: x in L iff x in Subgroups G & P[x] from Subset_Ex; take L; let x; thus x in L implies ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated by A1; given H1 being strict Subgroup of G such that A2: x = H1 & H,H1 are_conjugated; x in Subgroups G by A2,Def1; hence thesis by A1,A2; end; uniqueness proof let A1,A2 be Subset of Subgroups G; defpred P[set] means ex H3 being strict Subgroup of G st $1 = H3 & H,H3 are_conjugated; assume A3: x in A1 iff P[x]; assume A4: x in A2 iff P[x]; thus thesis from Extensionality(A3,A4); end; end; canceled 2; theorem Th127: x in con_class H implies x is strict Subgroup of G proof assume x in con_class H; then ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated by Def12; hence thesis; end; theorem Th128: for H1,H2 being strict Subgroup of G holds H1 in con_class H2 iff H1,H2 are_conjugated proof let H1,H2 be strict Subgroup of G; thus H1 in con_class H2 implies H1,H2 are_conjugated proof assume H1 in con_class H2; then ex H3 being strict Subgroup of G st H1 = H3 & H2,H3 are_conjugated by Def12; hence thesis; end; assume H1,H2 are_conjugated; hence thesis by Def12; end; theorem Th129: for H being strict Subgroup of G holds H |^ g in con_class H proof let H be strict Subgroup of G; H,H |^ g are_conjugated by Th121; hence thesis by Def12; end; theorem Th130: for H being strict Subgroup of G holds H in con_class H proof let H be strict Subgroup of G; H,H are_conjugated; hence thesis by Def12; end; theorem for H1,H2 being strict Subgroup of G holds H1 in con_class H2 implies H2 in con_class H1 proof let H1,H2 be strict Subgroup of G; assume H1 in con_class H2; then H1,H2 are_conjugated by Th128; hence thesis by Th128; end; theorem for H1,H2 being strict Subgroup of G holds con_class H1 = con_class H2 iff con_class H1 meets con_class H2 proof let H1,H2 be strict Subgroup of G; thus con_class H1 = con_class H2 implies con_class H1 meets con_class H2 proof assume con_class H1 = con_class H2; then H1 in con_class H2 & H1 in con_class H1 by Th130; hence thesis by XBOOLE_0:3; end; assume con_class H1 meets con_class H2; then consider x such that A1: x in con_class H1 & x in con_class H2 by XBOOLE_0:3; reconsider x as strict Subgroup of G by A1,Th127; thus con_class H1 c= con_class H2 proof let y; assume y in con_class H1; then consider H3 being strict Subgroup of G such that A2: H3 = y & H1,H3 are_conjugated by Def12; x,H1 are_conjugated & x,H2 are_conjugated by A1,Th128; then x,H3 are_conjugated & H2,x are_conjugated by A2,Th124; then H2,H3 are_conjugated by Th124; hence thesis by A2,Def12; end; let y; assume y in con_class H2; then consider H3 being strict Subgroup of G such that A3: H3 = y & H2,H3 are_conjugated by Def12; x,H2 are_conjugated & x,H1 are_conjugated by A1,Th128; then H1,x are_conjugated & x,H3 are_conjugated by A3,Th124; then H1,H3 are_conjugated by Th124; hence thesis by A3,Def12; end; theorem G is finite implies con_class H is finite proof assume G is finite; then Subgroups G is finite & con_class H c= Subgroups G by Th19; hence thesis by FINSET_1:13; end; theorem Th134: for H1 being strict Subgroup of G holds H1,H2 are_conjugated iff carr H1,carr H2 are_conjugated proof let H1 be strict Subgroup of G; thus H1,H2 are_conjugated implies carr H1,carr H2 are_conjugated proof given a such that A1: the HGrStr of H1 = H2 |^ a; carr H1 = the carrier of H1 by GROUP_2:def 9; then carr H1 = carr H2 |^ a by A1,Def6; hence thesis by Def9; end; given a such that A2: carr H1 = carr H2 |^ a; the carrier of H1 = carr H2 |^ a by A2,GROUP_2:def 9 .= the carrier of H2 |^ a by Def6; then H1 = H2 |^ a by GROUP_2:68; hence thesis by Def11; end; definition let G; let IT be Subgroup of G; attr IT is normal means :Def13: for a holds IT |^ a = the HGrStr of IT; end; definition let G; cluster strict normal Subgroup of G; existence proof for a holds (1).G |^ a = (1).G by Th80; then (1).G is normal by Def13; hence thesis; end; end; reserve N2 for normal Subgroup of G; canceled 2; theorem Th137: (1).G is normal & (Omega).G is normal proof thus for a being Element of G holds (1).G |^ a = the HGrStr of (1).G by Th80; thus for a being Element of G holds (Omega).G |^ a = the HGrStr of (Omega).G by Th82; end; theorem for N1,N2 being strict normal Subgroup of G holds N1 /\ N2 is normal proof let N1,N2 be strict normal Subgroup of G; let a; thus (N1 /\ N2) |^ a = (N1 |^ a) /\ (N2 |^ a) by Th76 .= N1 /\ (N2 |^ a) by Def13 .= the HGrStr of (N1 /\ N2) by Def13; end; theorem for H being strict Subgroup of G holds G is commutative Group implies H is normal proof let H be strict Subgroup of G; assume G is commutative Group; hence H |^ a = the HGrStr of H by Th86; end; theorem Th140: H is normal Subgroup of G iff for a holds a * H = H * a proof thus H is normal Subgroup of G implies for a holds a * H = H * a proof assume A1: H is normal Subgroup of G; let a; A2: carr(H |^ a) = the carrier of H |^ a by GROUP_2:def 9 .= the carrier of the HGrStr of H by A1,Def13 .= carr H by GROUP_2:def 9; A3: carr(H |^ a) = the carrier of H |^ a by GROUP_2:def 9 .= a" * H * a by Th71; thus a * H = a * carr(H |^ a) by A2,GROUP_2:def 13 .= a * (a" * H) * a by A3,GROUP_2:39 .= a * a" * H * a by GROUP_2:127 .= 1.G * H * a by GROUP_1:def 5 .= 1.G * (H * a) by GROUP_2:128 .= H * a by GROUP_2:43; end; assume A4: for a holds a * H = H * a; H is normal proof let a; the carrier of H |^ a = a" * H * a by Th71 .= H * a" * a by A4 .= H * (a" * a) by GROUP_2:129 .= H * 1.G by GROUP_1:def 5 .= carr H by GROUP_2:132 .= the carrier of H by GROUP_2:def 9; hence thesis by GROUP_2:68; end; hence thesis; end; theorem Th141: for H being Subgroup of G holds H is normal Subgroup of G iff for a holds a * H c= H * a proof let H be Subgroup of G; thus H is normal Subgroup of G implies for a holds a * H c= H * a by Th140 ; assume A1: for a holds a * H c= H * a; A2: now let a; a" * H c= H * a" by A1; then a * (a" * H) c= a * (H * a") by Th5; then a * a" * H c= a * (H * a") by GROUP_2:127; then 1.G * H c= a * (H * a") by GROUP_1:def 5; then carr H c= a * (H * a") by GROUP_2:132; then carr H c= a * H * a" by GROUP_2:128; then carr H * a c= a * H * a" * a by Th5; then H * a c= a * H * a" * a by GROUP_2:def 14; then H * a c= a * H * (a" * a) by GROUP_2:40; then H * a c= a * H * 1.G by GROUP_1:def 5; hence H * a c= a * H by GROUP_2:43; end; now let a; a * H c= H * a & H * a c= a * H by A1,A2; hence a * H = H * a by XBOOLE_0:def 10; end; hence thesis by Th140; end; theorem Th142: for H being Subgroup of G holds H is normal Subgroup of G iff for a holds H * a c= a * H proof let H be Subgroup of G; thus H is normal Subgroup of G implies for a holds H * a c= a * H by Th140 ; assume A1: for a holds H * a c= a * H; A2: now let a; H * a" c= a" * H by A1; then a * (H * a") c= a * (a" * H) by Th5; then a * (H * a") c= a * a" * H by GROUP_2:127; then a * (H * a") c= 1.G * H by GROUP_1:def 5; then a * (H * a") c= carr H by GROUP_2:132; then a * H * a" c= carr H by GROUP_2:128; then a * H * a" * a c= carr H * a by Th5; then a * H * a" * a c= H * a by GROUP_2:def 14; then a * H * (a" * a) c= H * a by GROUP_2:40; then a * H * 1.G c= H * a by GROUP_1:def 5; hence a * H c= H * a by GROUP_2:43; end; now let a; a * H c= H * a & H * a c= a * H by A1,A2; hence a * H = H * a by XBOOLE_0:def 10; end; hence thesis by Th140; end; theorem for H being Subgroup of G holds H is normal Subgroup of G iff for A holds A * H = H * A proof let H be Subgroup of G; thus H is normal Subgroup of G implies for A holds A * H = H * A proof assume A1: H is normal Subgroup of G; let A; thus A * H c= H * A proof let x; assume x in A * H; then consider a,h such that A2: x = a * h & a in A & h in H by GROUP_2:114; x in a * H by A2,GROUP_2:125; then x in H * a by A1,Th140; then ex g st x = g * a & g in H by GROUP_2:126; hence thesis by A2,GROUP_2:115; end; let x; assume x in H * A; then consider h,a such that A3: x = h * a & h in H & a in A by GROUP_2: 115; x in H * a by A3,GROUP_2:126; then x in a * H by A1,Th140; then ex g st x = a * g & g in H by GROUP_2:125; hence thesis by A3,GROUP_2:114; end; assume A4: for A holds A * H = H * A; now let a; thus a * H = {a} * H by Th7 .= H * {a} by A4 .= H * a by Th8; end; hence thesis by Th140; end; theorem for H being strict Subgroup of G holds H is normal Subgroup of G iff for a holds H is Subgroup of H |^ a proof let H be strict Subgroup of G; thus H is normal Subgroup of G implies for a holds H is Subgroup of H |^ a proof assume A1: H is normal Subgroup of G; let a; H |^ a = the HGrStr of H by A1,Def13; hence thesis by GROUP_2:63; end; assume A2: for a holds H is Subgroup of H |^ a; now let a; A3: H is Subgroup of H |^ a" by A2; A4: the carrier of H |^ a" = carr(H |^ a") by GROUP_2:def 9; H |^ a" * a = carr(H |^ a") * a by GROUP_2:def 14 .= a"" * H * a" * a by A4,Th71 .= a"" * H * (a" * a) by GROUP_2:40 .= a"" * H * 1.G by GROUP_1:def 5 .= a"" * H by GROUP_2:43 .= a * H by GROUP_1:19; hence H * a c= a * H by A3,Th6; end; hence thesis by Th142; end; theorem for H being strict Subgroup of G holds H is normal Subgroup of G iff for a holds H |^ a is Subgroup of H proof let H be strict Subgroup of G; thus H is normal Subgroup of G implies for a holds H |^ a is Subgroup of H proof assume A1: H is normal Subgroup of G; let a; H |^ a = the HGrStr of H by A1,Def13; hence thesis by GROUP_2:63; end; assume A2: for a holds H |^ a is Subgroup of H; now let a; A3: H |^ a" is Subgroup of H by A2; A4: the carrier of H |^ a" = carr(H |^ a") by GROUP_2:def 9; H |^ a" * a = carr(H |^ a") * a by GROUP_2:def 14 .= a"" * H * a" * a by A4,Th71 .= a"" * H * (a" * a) by GROUP_2:40 .= a"" * H * 1.G by GROUP_1:def 5 .= a"" * H by GROUP_2:43 .= a * H by GROUP_1:19; hence a * H c= H * a by A3,Th6; end; hence thesis by Th141; end; theorem for H being strict Subgroup of G holds H is normal Subgroup of G iff con_class H = {H} proof let H be strict Subgroup of G; thus H is normal Subgroup of G implies con_class H = {H} proof assume A1: H is normal Subgroup of G; thus con_class H c= {H} proof let x; assume x in con_class H; then consider H1 being strict Subgroup of G such that A2: x = H1 & H,H1 are_conjugated by Def12; ex g st H1 = H |^ g by A2,Th121; then x = H by A1,A2,Def13; hence thesis by TARSKI:def 1; end; H in con_class H by Th130; hence thesis by ZFMISC_1:37; end; assume A3: con_class H = {H}; H is normal proof let a; H |^ a in con_class H by Th129; hence thesis by A3,TARSKI:def 1; end; hence thesis; end; theorem for H being strict Subgroup of G holds H is normal Subgroup of G iff for a st a in H holds con_class a c= carr H proof let H be strict Subgroup of G; thus H is normal Subgroup of G implies for a st a in H holds con_class a c= carr H proof assume A1: H is normal Subgroup of G; let a; assume A2: a in H; let x; assume x in con_class a; then consider b such that A3: x = b & a,b are_conjugated by Th95; consider c such that A4: b = a |^ c by A3,Th88; x in H |^ c by A2,A3,A4,Th70; then x in H by A1,Def13; hence thesis by GROUP_2:88; end; assume A5: for a st a in H holds con_class a c= carr H; H is normal proof let a; H |^ a = H proof let b; thus b in H |^ a implies b in H proof assume b in H |^ a; then consider c such that A6: b = c |^ a & c in H by Th70; b in con_class c & con_class c c= carr H by A5,A6,Th97; hence thesis by GROUP_2:88; end; assume b in H; then con_class b c= carr H & b |^ a" in con_class b by A5,Th97; then b |^ a" in H by GROUP_2:88; then b |^ a" |^ a in H |^ a by Th70; hence thesis by Th30; end; hence H |^ a = the HGrStr of H; end; hence thesis; end; Lm5: for N1 being strict normal Subgroup of G holds carr N1 * carr N2 c= carr N2 * carr N1 proof let N1 be strict normal Subgroup of G; let x; assume x in carr N1 * carr N2; then consider a,b such that A1: x = a * b & a in carr N1 & b in carr N2 by GROUP_2:12; a in N1 by A1,GROUP_2:88; then a |^ b in N1 |^ b by Th70; then a |^ b in the HGrStr of N1 by Def13; then A2: a |^ b in carr N1 by GROUP_2:88; b * (a |^ b) = b * (b" * (a * b)) by Th20 .= a * b by Th1; hence thesis by A1,A2,GROUP_2:12; end; theorem Th148: for N1,N2 being strict normal Subgroup of G holds carr N1 * carr N2 = carr N2 * carr N1 proof let N1,N2 be strict normal Subgroup of G; carr N1 * carr N2 c= carr N2 * carr N1 & carr N2 * carr N1 c= carr N1 * carr N2 by Lm5; hence thesis by XBOOLE_0:def 10; end; theorem for N1,N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st the carrier of N = carr N1 * carr N2 proof let N1,N2 be strict normal Subgroup of G; set A = carr N1 * carr N2; set B = carr N1; set C = carr N2; carr N1 * carr N2 = carr N2 * carr N1 by Th148; then consider H being strict Subgroup of G such that A1: the carrier of H = A by GROUP_2:93; A2: carr H = A by A1,GROUP_2:def 9; now let a; thus a * H = a * A by A2,GROUP_2:def 13 .= a * B * C by GROUP_2:35 .= a * N1 * C by GROUP_2:def 13 .= N1 * a * C by Th140 .= B * a * C by GROUP_2:def 14 .= B * (a * C) by GROUP_2:36 .= B * (a * N2) by GROUP_2:def 13 .= B * (N2 * a) by Th140 .= B * (C * a) by GROUP_2:def 14 .= A * a by GROUP_2:37 .= H * a by A2,GROUP_2:def 14; end; then H is normal Subgroup of G by Th140; hence thesis by A1; end; theorem for N being normal Subgroup of G holds Left_Cosets N = Right_Cosets N proof let N be normal Subgroup of G; thus Left_Cosets N c= Right_Cosets N proof let x; assume x in Left_Cosets N; then consider a such that A1: x = a * N by GROUP_2:def 15; x = N * a by A1,Th140; hence thesis by GROUP_2:def 16; end; let x; assume x in Right_Cosets N; then consider a such that A2: x = N * a by GROUP_2:def 16; x = a * N by A2,Th140; hence thesis by GROUP_2:def 15; end; Lm6: for X being finite set st card X = 2 ex x,y st x <> y & X = {x,y} proof let X be finite set; assume A1: card X = 2; then A2: X <> {} by CARD_1:47; consider x being Element of X; {x} c= X by A1,CARD_1:47,ZFMISC_1:37; then card(X \ {x}) = card X - card{x} by CARD_2:63 .= 1 + 1 - 1 by A1,CARD_1:79 .= 1; then consider y such that A3: X \ {x} = {y} by CARD_2:60; take x,y; now assume x = y; then not x in {x} by A3,XBOOLE_0:def 4; hence contradiction by TARSKI:def 1; end; hence x <> y; thus X c= {x,y} proof let z be set; assume A4: z in X; now per cases; suppose z = x; hence thesis by TARSKI:def 2; suppose z <> x; then not z in {x} by TARSKI:def 1; then z in {y} by A3,A4,XBOOLE_0:def 4; then z = y by TARSKI:def 1; hence thesis by TARSKI:def 2; end; hence thesis; end; let z be set; assume z in {x,y}; then A5: z = x or z = y by TARSKI:def 2; y in X \ {x} by A3,TARSKI:def 1; hence thesis by A2,A5,XBOOLE_0:def 4; end; theorem for H being Subgroup of G holds Left_Cosets H is finite & index H = 2 implies H is normal Subgroup of G proof let H be Subgroup of G; assume that A1: Left_Cosets H is finite and A2: index H = 2; consider B being finite set such that A3: B = Left_Cosets H & index H = card B by A1,GROUP_2:176; consider C being finite set such that A4: C = Right_Cosets H & index H = card C by A1,GROUP_2:176; consider x,y such that A5: x <> y and A6: Left_Cosets H = {x,y} by A2,A3,Lm6; consider z1,z2 being set such that A7: z1 <> z2 and A8: Right_Cosets H = {z1,z2} by A2,A4,Lm6; A9: carr H in Left_Cosets H & carr H in Right_Cosets H by GROUP_2:165; then {x,y} = {x,carr H} or {x,y} = {carr H,y} by A6,TARSKI:def 2; then consider z3 being set such that A10: {x,y} = {carr H,z3}; {z1,z2} = {z1,carr H} or {z1,z2} = {carr H,z2} by A8,A9,TARSKI:def 2; then consider z4 being set such that A11: {z1,z2} = {carr H,z4}; A12: union Left_Cosets H = the carrier of G & union Right_Cosets H = the carrier of G by GROUP_2:167; A13: union Left_Cosets H = carr H \/ z3 by A6,A10,ZFMISC_1:93; carr H misses z3 proof assume A14: not thesis; z3 in Left_Cosets H by A6,A10,TARSKI:def 2; then A15: ex a st z3 = a * H by GROUP_2:def 15; carr H = 1.G * H by GROUP_2:132; then carr H = z3 by A14,A15,GROUP_2:138; then {x,y} = {carr H} by A10,ENUMSET1:69; then x = carr H & y = carr H by ZFMISC_1:8; hence thesis by A5; end; then A16: z3 = (the carrier of G) \ carr H by A12,A13,XBOOLE_1:88; A17: union Right_Cosets H = carr H \/ z4 by A8,A11,ZFMISC_1:93; A18: carr H misses z4 proof assume A19: not thesis; z4 in Right_Cosets H by A8,A11,TARSKI:def 2; then A20: ex a st z4 = H * a by GROUP_2:def 16; carr H = H * 1.G by GROUP_2:132; then carr H = z4 by A19,A20,GROUP_2:144; then {z1,z2} = {carr H} by A11,ENUMSET1:69; then z1 = carr H & z2 = carr H by ZFMISC_1:8; hence thesis by A7; end; now let c; now per cases; suppose A21: c * H = carr H; then c in H by GROUP_2:136; hence c * H = H * c by A21,GROUP_2:142; suppose A22: c * H <> carr H; then not c in H by GROUP_2:136; then A23: H * c <> carr H by GROUP_2:142; c * H in Left_Cosets H & H * c in Right_Cosets H by GROUP_2:def 15,def 16; then c * H = z3 & H * c = z4 by A6,A8,A10,A11,A22,A23,TARSKI:def 2; hence c * H = H * c by A12,A16,A17,A18,XBOOLE_1:88; end; hence c * H = H * c; end; hence thesis by Th140; end; definition let G; let A; func Normalizator A -> strict Subgroup of G means :Def14: the carrier of it = {h : A |^ h = A}; existence proof set X = {h : A |^ h = A}; X c= the carrier of G proof let x; assume x in X; then ex h st x = h & A |^ h = A; hence thesis; end; then reconsider X as Subset of G; A |^ 1.G = A by Th61; then A1: 1.G in X; A2: now let a,b; assume that A3: a in X and A4: b in X; A5: ex g st a = g & A |^ g = A by A3; ex h st b = h & A |^ h = A by A4; then A |^ (a * b) = A by A5,Th56; hence a * b in X; end; now let a; assume a in X; then ex b st a = b & A |^ b = A; then A = A |^ a" by Th63; hence a" in X; end; hence thesis by A1,A2,GROUP_2:61; end; uniqueness by GROUP_2:68; end; canceled 2; theorem Th154: x in Normalizator A iff ex h st x = h & A |^ h = A proof thus x in Normalizator A implies ex h st x = h & A |^ h = A proof assume x in Normalizator A; then x in the carrier of Normalizator A by RLVECT_1:def 1; then x in {h : A |^ h = A} by Def14; hence thesis; end; given h such that A1: x = h & A |^ h = A; x in {b : A |^ b = A} by A1; then x in the carrier of Normalizator A by Def14; hence thesis by RLVECT_1:def 1; end; theorem Th155: Card con_class A = Index Normalizator A proof defpred P[set,set] means ex a st $1 = A |^ a & $2 = Normalizator A * a; A1: for x,y1,y2 st x in con_class A & P[x,y1] & P[x,y2] holds y1 = y2 proof let x,y1,y2; assume x in con_class A; given a such that A2: x = A |^ a and A3: y1 = Normalizator A * a; given b such that A4: x = A |^ b and A5: y2 = Normalizator A * b; A = A |^ b |^ a" by A2,A4,Th63 .= A |^ (b * a") by Th56; then b * a" in Normalizator A by Th154; hence thesis by A3,A5,GROUP_2:143; end; A6: for x st x in con_class A ex y st P[x,y] proof let x; assume x in con_class A; then consider B such that A7: x = B & A,B are_conjugated by Th111; consider g such that A8: B = A |^ g by A7,Th104; reconsider y = Normalizator A * g as set; take y; take g; thus thesis by A7,A8; end; consider f being Function such that A9: dom f = con_class A and A10: for x st x in con_class A holds P[x,f.x] from FuncEx(A1,A6); A11: rng f = Right_Cosets Normalizator A proof thus rng f c= Right_Cosets Normalizator A proof let x; assume x in rng f; then consider y such that A12: y in dom f & f.y = x by FUNCT_1:def 5; ex a st y = A |^ a & x = Normalizator A * a by A9,A10,A12; hence thesis by GROUP_2:def 16; end; let x; assume x in Right_Cosets Normalizator A; then consider a such that A13: x = Normalizator A * a by GROUP_2:def 16; set y = A |^ a; A,A |^ a are_conjugated by Th104; then A14: y in con_class A by Th111; then ex b st y = A |^ b & f.y = Normalizator A * b by A10; then x = f.y by A1,A13,A14; hence thesis by A9,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 a such that A18: x = A |^ a & f.x = Normalizator A * a by A9,A10,A15; consider b such that A19: y = A |^ b & f.y = Normalizator A * b by A9,A10,A16; b * a" in Normalizator A by A17,A18,A19,GROUP_2:143; then ex h st b * a" = h & A |^ h = A by Th154; then A = A |^ b |^ a" by Th56; hence thesis by A18,A19,Th63; end; then con_class A,Right_Cosets Normalizator A are_equipotent by A9,A11,WELLORD2:def 4; hence Card con_class A = Card Right_Cosets Normalizator A by CARD_1:21 .= Index Normalizator A by GROUP_2:175; end; theorem con_class A is finite or Left_Cosets Normalizator A is finite implies ex C being finite set st C = con_class A & card C = index Normalizator A proof assume A1: con_class A is finite or Left_Cosets Normalizator A is finite; A2: Card con_class A = Index Normalizator A by Th155 .= Card Left_Cosets Normalizator A by GROUP_2:175; then A3: con_class A,Left_Cosets Normalizator A are_equipotent by CARD_1:21; then con_class A is finite & Left_Cosets Normalizator A is finite by A1,CARD_1:68; then consider B being finite set such that A4: B = Left_Cosets Normalizator A & index Normalizator A = card B by GROUP_2:def 18; reconsider C = con_class A as finite set by A1,A3,CARD_1:68; take C; thus C = con_class A; thus card C = index Normalizator A by A2,A4; end; theorem Th157: Card con_class a = Index Normalizator{a} proof deffunc F(set) = {$1}; consider f being Function such that A1: dom f = con_class a and A2: for x st x in con_class a holds f.x = F(x) from Lambda; A3: rng f = con_class{a} proof thus rng f c= con_class{a} proof let x; assume x in rng f; then consider y such that A4: y in dom f & f.y = x by FUNCT_1:def 5; reconsider y as Element of G by A1,A4; f.y = {y} by A1,A2,A4; then x in {{d} : d in con_class a} by A1,A4; hence thesis by Th118; end; let x; assume x in con_class{a}; then x in {{b} : b in con_class a} by Th118; then consider b such that A5: x = {b} & b in con_class a; f.b = {b} by A2,A5; hence thesis by A1,A5,FUNCT_1:def 5; end; f is one-to-one proof let x,y; assume that A6: x in dom f & y in dom f and A7: f.x = f.y; f.x = {x} & f.y = {y} by A1,A2,A6; hence thesis by A7,ZFMISC_1:6; end; then con_class a,con_class{a} are_equipotent by A1,A3,WELLORD2:def 4; hence Card con_class a = Card con_class{a} by CARD_1:21 .= Index Normalizator{a} by Th155; end; theorem con_class a is finite or Left_Cosets Normalizator{a} is finite implies ex C being finite set st C = con_class a & card C = index Normalizator{a} proof assume A1: con_class a is finite or Left_Cosets Normalizator {a} is finite; A2: Card con_class a = Index Normalizator {a} by Th157 .= Card Left_Cosets Normalizator {a} by GROUP_2:175; then A3: con_class a,Left_Cosets Normalizator {a} are_equipotent by CARD_1:21; then con_class a is finite & Left_Cosets Normalizator {a} is finite by A1,CARD_1:68; then consider B being finite set such that A4: B = Left_Cosets Normalizator {a} & index Normalizator {a} = card B by GROUP_2:def 18; reconsider C = con_class a as finite set by A1,A3,CARD_1:68; take C; thus C = con_class a; thus card C = index Normalizator {a} by A2,A4; end; definition let G; let H; func Normalizator H -> strict Subgroup of G equals :Def15: Normalizator carr H; correctness; end; canceled; theorem Th160: for H being strict Subgroup of G holds x in Normalizator H iff ex h st x = h & H |^ h = H proof let H be strict Subgroup of G; thus x in Normalizator H implies ex h st x = h & H |^ h = H proof assume x in Normalizator H; then x in Normalizator carr H by Def15; then consider a such that A1: x = a & carr H |^ a = carr H by Th154; carr H = the carrier of H & the carrier of H |^ a = carr H |^ a by Def6,GROUP_2:def 9; then H |^ a = H by A1,GROUP_2:68; hence thesis by A1; end; given h such that A2: x = h & H |^ h = H; carr H |^ h = the carrier of H by A2,Def6 .= carr H by GROUP_2:def 9; then x in Normalizator carr H by A2,Th154; hence thesis by Def15; end; theorem Th161: for H being strict Subgroup of G holds Card con_class H = Index Normalizator H proof let H be strict Subgroup of G; defpred P[set,set] means ex H1 being strict Subgroup of G st $1 = H1 & $2 = carr H1; A1: for x,y1,y2 st x in con_class H & P[x,y1] & P[x,y2] holds y1 = y2; A2: for x st x in con_class H ex y st P[x,y] proof let x; assume x in con_class H; then reconsider H = x as strict Subgroup of G by Def1; reconsider y = carr H as set; take y; take H; thus thesis; end; consider f being Function such that A3: dom f = con_class H and A4: for x st x in con_class H holds P[x,f.x] from FuncEx(A1,A2); A5: rng f = con_class carr H proof thus rng f c= con_class carr H proof let x; assume x in rng f; then consider y such that A6: y in dom f & f.y = x by FUNCT_1:def 5; consider H1 being strict Subgroup of G such that A7: y = H1 & x = carr H1 by A3,A4,A6; H1,H are_conjugated by A3,A6,A7,Th128; then carr H1,carr H are_conjugated by Th134; hence thesis by A7,Th113; end; let x; assume x in con_class carr H; then consider B such that A8: B = x & carr H,B are_conjugated by Th111; consider H1 being strict Subgroup of G such that A9: the carrier of H1 = B by A8,Th109; A10: B = carr H1 by A9,GROUP_2:def 9; then H1,H are_conjugated by A8,Th134; then A11: H1 in con_class H by Th128; then ex H2 being strict Subgroup of G st H1 = H2 & f.H1 = carr H2 by A4; hence thesis by A3,A8,A10,A11,FUNCT_1:def 5; end; f is one-to-one proof let x,y; assume that A12: x in dom f and A13: y in dom f and A14: f.x = f.y; consider H1 being strict Subgroup of G such that A15: x = H1 & f.x = carr H1 by A3,A4,A12; consider H2 being strict Subgroup of G such that A16: y = H2 & f.y = carr H2 by A3,A4,A13; the carrier of H1 = carr H1 & the carrier of H2 = carr H2 by GROUP_2:def 9; hence thesis by A14,A15,A16,GROUP_2:68; end; then con_class H,con_class carr H are_equipotent by A3,A5,WELLORD2:def 4; hence Card con_class H = Card con_class carr H by CARD_1:21 .= Index Normalizator carr H by Th155 .= Index Normalizator H by Def15; end; theorem for H being strict Subgroup of G holds con_class H is finite or Left_Cosets Normalizator H is finite implies ex C being finite set st C = con_class H & card C = index Normalizator H proof let H be strict Subgroup of G; assume A1: con_class H is finite or Left_Cosets Normalizator H is finite; A2: Card con_class H = Index Normalizator H by Th161 .= Card Left_Cosets Normalizator H by GROUP_2:175; then A3: con_class H,Left_Cosets Normalizator H are_equipotent by CARD_1:21; then con_class H is finite & Left_Cosets Normalizator H is finite by A1,CARD_1:68; then consider B being finite set such that A4: B = Left_Cosets Normalizator H & index Normalizator H = card B by GROUP_2:def 18; reconsider C = con_class H as finite set by A1,A3,CARD_1:68; take C; thus C = con_class H; thus card C = index Normalizator H by A2,A4; end; theorem Th163: for G being strict Group, H being strict Subgroup of G holds H is normal Subgroup of G iff Normalizator H = G proof let G be strict Group, H be strict Subgroup of G; thus H is normal Subgroup of G implies Normalizator H = G proof assume A1: H is normal Subgroup of G; now let a be Element of G; H |^ a = H by A1,Def13; hence a in Normalizator H by Th160; end; hence thesis by GROUP_2:71; end; assume A2: Normalizator H = G; H is normal proof let a be Element of G; a in Normalizator H by A2,RLVECT_1:def 1; then ex b being Element of G st b = a & H |^ b = H by Th160; hence H |^ a = the HGrStr of H; end; hence thesis; end; theorem for G being strict Group holds Normalizator (1).G = G proof let G be strict Group; (1).G is normal Subgroup of G by Th137; hence thesis by Th163; end; theorem for G being strict Group holds Normalizator (Omega).G = G proof let G be strict Group; (Omega).G is normal Subgroup of G by Th137; hence thesis by Th163; end; :: :: Auxiliary theorems. :: theorem for X being finite set st card X = 2 ex x,y st x <> y & X = {x,y} by Lm6;

Back to top