:: Classes of Conjugation. Normal Subgroups :: by Wojciech A. Trybulec :: :: Received August 10, 1990 :: Copyright (c) 1990-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies GROUP_1, SUBSET_1, GROUP_2, NAT_1, INT_1, RELAT_1, BINOP_1, ALGSTR_0, FUNCT_1, STRUCT_0, TARSKI, ZFMISC_1, XBOOLE_0, FINSET_1, CARD_1, NEWTON, ARYTM_3, XXREAL_0, COMPLEX1, RLSUB_1, CQC_SIM1, SETFAM_1, PRE_TOPC, GROUP_3; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, CARD_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, DOMAIN_1, XXREAL_0, INT_1, INT_2; constructors SETFAM_1, WELLORD2, BINOP_1, XXREAL_0, NAT_1, INT_2, REALSET1, REAL_1, GROUP_2, RELSET_1, BINOP_2, NUMBERS; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, XREAL_0, INT_1, STRUCT_0, GROUP_1, GROUP_2, ORDINAL1; requirements NUMERALS, SUBSET, BOOLE; definitions XBOOLE_0, BINOP_1, FUNCT_1, GROUP_2, TARSKI, GROUP_1; equalities BINOP_1, GROUP_2, TARSKI, ALGSTR_0, STRUCT_0; expansions XBOOLE_0, BINOP_1, GROUP_1, STRUCT_0; theorems ABSVALUE, CARD_1, CARD_2, ENUMSET1, FINSET_1, FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, TARSKI, WELLORD2, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, STRUCT_0, XTUPLE_0; schemes FUNCT_1, FUNCT_2, NAT_1, SUBSET_1, XBOOLE_0, CLASSES1, XFAMILY; 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 GROUP_1:def 3 .= a * 1_G by GROUP_1:def 5 .= a by GROUP_1:def 4; thus A2: a * b" * b = a * (b" * b) by GROUP_1:def 3 .= 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,GROUP_1:def 3; 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 multF of G is commutative proof thus G is commutative Group implies the multF of G is commutative proof assume A1: G is commutative Group; let a,b; thus (the multF of G).(a,b) = a * b .= b * a by A1,Lm1 .= (the multF of G).(b,a); end; assume A2: the multF of G is commutative; G is commutative by A2; hence thesis; end; theorem (1).G is commutative proof let a,b be Element of (1).G; a in the carrier of (1).G; then a in {1_G} by GROUP_2:def 7; then A1: a = 1_G by TARSKI:def 1; b in the carrier of (1).G; then b in {1_G} by GROUP_2:def 7; hence thesis by A1,TARSKI:def 1; 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 be object; assume x in A * C; then ex a,c st x = a * c & a in A & c in C; hence thesis by A1; end; theorem A c= B implies a * A c= a * B & A * a c= B * a by Th4; 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 by GROUP_2:def 5; hence thesis by Th4; end; theorem a * H = {a} * H; theorem H * a = H * {a}; theorem Th9: A * a * H = A * (a * H) proof thus A * a * H = A * ({a} * H) by GROUP_2:96 .= A * (a * H); end; theorem a * H * A = a * (H * A) proof thus a * H * A = {a} * H * A .= a * (H * A) by GROUP_2:97; end; theorem A * H * a = A * (H * a) proof thus A * H * a = A * (H * {a}) by GROUP_2:97 .= A * (H * a); end; theorem H * a * A = H * (a * A) proof thus H * a * A = H * {a} * A .= H * (a * A) by GROUP_2:98; end; theorem H1 * a * H2 = H1 * (a * H2) by Th9; definition let G; func Subgroups G -> set means :Def1: for x being object holds x in it iff x is strict Subgroup of G; existence proof defpred P[object,object] means ex H being strict Subgroup of G st \$2 = H & \$1 = the carrier of H; 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 XFAMILY:sch 1; A2: for x,y1,y2 being object st P[x,y1] & P[x,y2] holds y1 = y2 by GROUP_2:59; consider f being Function such that A3: for x,y being object holds [x,y] in f iff x in B & P[x,y] from FUNCT_1:sch 1(A2); for x being object holds x in B iff ex y being object st [x,y] in f proof let x be object; thus x in B implies ex y being object 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; take H; thus thesis by A3,A4,A5; end; thus thesis by A3; end; then A6: B = dom f by XTUPLE_0:def 12; for y being object holds y in rng f iff y is strict Subgroup of G proof let y be object; thus y in rng f implies y is strict Subgroup of G proof assume y in rng f; then consider x being object such that A7: x in dom f & y = f.x by FUNCT_1:def 3; [x,y] in f by A7,FUNCT_1:def 2; 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; A8: y is set by TARSKI:1; 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,A6; then [x,y] in f by A3,A6; then y = f.x by A9,FUNCT_1:def 2,A8; hence thesis by A9,FUNCT_1:def 3; end; hence thesis; end; uniqueness proof defpred P[object] means \$1 is strict Subgroup of G; let A1,A2 be set; assume A10: for x being object holds x in A1 iff P[x]; assume A11: for x being object holds x in A2 iff P[x]; thus thesis from XBOOLE_0:sch 2(A10,A11); end; end; registration let G; cluster Subgroups G -> non empty; coherence proof set x = the strict Subgroup of G; x in Subgroups G by Def1; hence thesis; end; end; 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:54; hence thesis by Def1; end; theorem Th15: G is finite implies Subgroups G is finite proof defpred P[object,object] means ex H being strict Subgroup of G st \$1 = H & \$2 = the carrier of H; assume A1: G is finite; A2: for x being object st x in Subgroups G ex y being object st P[x,y] proof let x be object; 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 A3: dom f = Subgroups G and A4: for x being object st x in Subgroups G holds P[x,f.x] from CLASSES1:sch 1(A2); A5: rng f c= bool the carrier of G proof let x be object; assume x in rng f; then consider y being object such that A6: y in dom f & f.y = x by FUNCT_1:def 3; consider H being strict Subgroup of G such that y = H and A7: x = the carrier of H by A3,A4,A6; the carrier of H c= the carrier of G by GROUP_2:def 5; hence thesis by A7; end; f is one-to-one proof let x,y be object; assume that A8: x in dom f & y in dom f and A9: f.x = f.y; ( ex H1 being strict Subgroup of G st x = H1 & f.x = the carrier of H1)& ex H2 being strict Subgroup of G st y = H2 & f.y = the carrier of H2 by A3 ,A4,A8; hence thesis by A9,GROUP_2:59; end; then card Subgroups G c= card bool the carrier of G by A3,A5,CARD_1:10; hence thesis by A1,CARD_2:49; end; definition let G,a,b; func a |^ b -> Element of G equals b" * a * b; correctness; end; theorem Th16: a |^ g = b |^ g implies a = b proof assume a |^ g = b |^ g; then g" * a = g" * b by GROUP_1:6; hence thesis by GROUP_1:6; end; theorem Th17: (1_G) |^ a = 1_G proof thus (1_G) |^ a = a" * a by GROUP_1:def 4 .= 1_G by GROUP_1:def 5; end; theorem Th18: a |^ b = 1_G implies a = 1_G proof assume a |^ b = 1_G; then b" = b" * a by GROUP_1:12; hence thesis by GROUP_1:7; end; theorem Th19: a |^ 1_G = a proof thus a |^ 1_G = (1_G)" * a by GROUP_1:def 4 .= 1_G * a by GROUP_1:8 .= a by GROUP_1:def 4; end; theorem Th20: a |^ a = a proof thus a |^ a = 1_G * a by GROUP_1:def 5 .= a by GROUP_1:def 4; end; theorem a |^ a" = a & a" |^ a = a" by Th1; theorem Th22: 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 GROUP_1:def 3; hence thesis by GROUP_1:13; end; assume a * b = b * a; then a = b" * (a * b) by GROUP_1:13; hence thesis by GROUP_1:def 3; end; theorem Th23: (a * b) |^ g = a |^ g * (b |^ g) proof thus (a * b) |^ g = 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 GROUP_1:def 3 .= g" * (a * g * (g" * b)) * g by GROUP_1:def 3 .= g" * (a * g) * (g" * b) * g by GROUP_1:def 3 .= a |^ g * (g" * b) * g by GROUP_1:def 3 .= a |^ g * (b |^ g) by GROUP_1:def 3; end; theorem Th24: a |^ g |^ h = a |^ (g * h) proof thus a |^ g |^ h = h" * (g" * a) * g * h by GROUP_1:def 3 .= h" * g" * a * g * h by GROUP_1:def 3 .= (g * h)" * a * g * h by GROUP_1:17 .= a |^ (g * h) by GROUP_1:def 3; end; theorem Th25: a |^ b |^ b" = a & a |^ b" |^ b = a proof thus a |^ b |^ b" = a |^ (b * b") by Th24 .= a |^ 1_G by GROUP_1:def 5 .= a by Th19; thus a |^ b" |^ b = a |^ (b" * b) by Th24 .= a |^ 1_G by GROUP_1:def 5 .= a by Th19; end; theorem Th26: a" |^ b = (a |^ b)" proof thus a" |^ b = (a * b)" * b by GROUP_1:17 .= (a * b)" * b"" .= (b" * (a * b))" by GROUP_1:17 .= (a |^ b)" by GROUP_1:def 3; end; Lm2: now let G,a,b; thus a |^ 0 |^ b = (1_G) |^ b by GROUP_1:25 .= 1_G by Th17 .= (a |^ b) |^ 0 by GROUP_1:25; 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:34 .= (a |^ n |^ b) * (a |^ b) by Th23 .= ((a |^ b) |^ n) * (a |^ b) by A1 .= (a |^ b) |^ (n + 1) by GROUP_1:34; 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: for k be Nat st P[k] holds P[k+1] by Lm3; A2: P[0] by Lm2; for k be Nat holds P[k] from NAT_1:sch 2(A2,A1); 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 = |.i.| by ABSVALUE:def 1; hence thesis by Lm4; end; suppose A1: i < 0; hence a |^ i |^ b = (a |^ |.i.|)" |^ b by GROUP_1:30 .= (a |^ |.i.| |^ b)" by Th26 .= ((a |^ b) |^ |.i.|)" by Lm4 .= (a |^ b) |^ i by A1,GROUP_1:30; end; end; theorem Th29: G is commutative Group implies a |^ b = a proof assume G is commutative Group; hence a |^ b = a * b" * b by Lm1 .= a by Th1; end; theorem Th30: (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 Th22; end; definition let G,A,B; func A |^ B -> Subset of G equals {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 be object; assume x in X; then ex g,h st x = g |^ h & g in A & h in B; hence thesis; end; hence thesis; end; end; theorem Th31: x in A |^ B iff ex g,h st x = g |^ h & g in A & h in B; theorem Th32: A |^ B <> {} iff A <> {} & B <> {} proof set x = the Element of A; set y = the Element of B; thus A |^ B <> {} implies A <> {} & B <> {} proof set x = the Element of A |^ B; assume A |^ B <> {}; then ex a,b st x = a |^ b & a in A & b in B by Th31; hence thesis; end; assume A1: A <> {}; assume A2: B <> {}; then reconsider x,y as Element of G by A1,TARSKI:def 3; x |^ y in A |^ B by A1,A2; hence thesis; end; theorem Th33: A |^ B c= B" * A * B proof let x be object; assume x in A |^ B; then consider a,b such that A1: x = a |^ b and A2: a in A and A3: b in B; b" in B" by A3; then b" * a in B" * A by A2; hence thesis by A1,A3; end; theorem Th34: (A * B) |^ C c= A |^ C * (B |^ C) proof let x be object; assume x in (A * B) |^ C; then consider a,b such that A1: x = a |^ b and A2: a in A * B and A3: b in C; consider g,h such that A4: a = g * h & g in A and A5: h in B by A2; A6: h |^ b in B |^ C by A3,A5; x = (g |^ b) * (h |^ b) & g |^ b in A |^ C by A1,A3,A4,Th23; hence thesis by A6; end; theorem Th35: A |^ B |^ C = A |^ (B * C) proof thus A |^ B |^ C c= A |^ (B * C) proof let x be object; assume x in A |^ B |^ C; then consider a,c such that A1: x = a |^ c and A2: a in A |^ B and A3: c in C; consider g,h such that A4: a = g |^ h and A5: g in A and A6: h in B by A2; x = g |^ (h * c) & h * c in B * C by A1,A3,A4,A6,Th24; hence thesis by A5; end; let x be object; assume x in A |^ (B * C); then consider a,b such that A7: x = a |^ b & a in A and A8: b in B * C; consider g,h such that A9: b = g * h & g in B and A10: h in C by A8; a |^ g in A |^ B & x = a |^ g |^ h by A7,A9,Th24; hence thesis by A10; end; theorem A" |^ B = (A |^ B)" proof thus A" |^ B c= (A |^ B)" proof let x be object; assume x in A" |^ B; then consider a,b such that A1: x = a |^ b and A2: a in A" and A3: b in B; consider c such that A4: a = c" & c in A by A2; x = (c |^ b)" & c |^ b in A |^ B by A1,A3,A4,Th26; hence thesis; end; let x be object; assume x in (A |^ B)"; then consider a such that A5: x = a" and A6: a in A |^ B; consider b,c such that A7: a = b |^ c and A8: b in A and A9: c in B by A6; A10: b" in A" by A8; x = b" |^ c by A5,A7,Th26; hence thesis by A9,A10; end; theorem Th37: {a} |^ {b} = {a |^ b} proof A1: {b}" * {a} * {b} = {b"} * {a} * {b} by GROUP_2:3 .= {b" * a} * {b} by GROUP_2:18 .= {a |^ b} by GROUP_2:18; {a} |^ {b} c= {b}" * {a} * {b} & {a} |^ {b} <> {} by Th32,Th33; hence thesis by A1,ZFMISC_1:33; end; theorem {a} |^ {b,c} = {a |^ b,a |^ c} proof thus {a} |^ {b,c} c= {a |^ b,a |^ c} proof let x be object; assume x in {a} |^ {b,c}; then consider g,h such that A1: x = g |^ h and A2: g in {a} and A3: h in{b,c}; A4: h = b or h = c by A3,TARSKI:def 2; g = a by A2,TARSKI:def 1; hence thesis by A1,A4,TARSKI:def 2; end; let x be object; A5: c in {b,c} by TARSKI:def 2; assume x in {a |^ b,a |^ c}; then A6: x = a |^ b or x = a |^ c by TARSKI:def 2; a in {a} & b in {b,c} by TARSKI:def 1,def 2; hence thesis by A6,A5; end; theorem {a,b} |^ {c} = {a |^ c,b |^ c} proof thus {a,b} |^ {c} c= {a |^ c,b |^ c} proof let x be object; assume x in {a,b} |^ {c}; then consider g,h such that A1: x = g |^ h and A2: g in {a,b} and A3: h in {c}; A4: g = b or g = a by A2,TARSKI:def 2; h = c by A3,TARSKI:def 1; hence thesis by A1,A4,TARSKI:def 2; end; let x be object; A5: c in {c} by TARSKI:def 1; assume x in {a |^ c,b |^ c}; then A6: x = a |^ c or x = b |^ c by TARSKI:def 2; a in {a,b} & b in {a,b} by TARSKI:def 2; hence thesis by A6,A5; 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 be object; assume x in {a,b} |^ {c,d}; then consider g,h such that A1: x = g |^ h and A2: g in {a,b} and A3: h in {c,d}; A4: h = c or h = d by A3,TARSKI:def 2; g = a or g = b by A2,TARSKI:def 2; hence thesis by A1,A4,ENUMSET1:def 2; end; let x be object; A5: c in {c,d} & d in {c,d} by TARSKI:def 2; assume x in {a |^ c,a |^ d,b |^ c,b |^ d}; then A6: x = a |^ c or x = a |^ d or x = b |^ c or x = b |^ d by ENUMSET1:def 2; a in {a,b} & b in {a,b} by TARSKI:def 2; hence thesis by A6,A5; end; definition let G,A,g; func A |^ g -> Subset of G equals A |^ {g}; correctness; func g |^ A -> Subset of G equals {g} |^ A; correctness; end; theorem Th41: 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 consider a,b such that A1: x = a |^ b & a in A and A2: b in {g}; b = g by A2,TARSKI:def 1; hence thesis by A1; end; given h such that A3: x = h |^ g & h in A; g in {g} by TARSKI:def 1; hence thesis by A3; end; theorem Th42: 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 consider a,b such that A1: x = a |^ b and A2: a in {g} and A3: b in A; a = g by A2,TARSKI:def 1; hence thesis by A1,A3; end; given h such that A4: x = g |^ h & h in A; g in {g} by TARSKI:def 1; hence thesis by A4; end; theorem g |^ A c= A" * g * A proof let x be object; assume x in g |^ A; then consider a such that A1: x = g |^ a and A2: a in A by Th42; a" in A" by A2; then a" * g in A" * g by GROUP_2:28; hence thesis by A1,A2; end; theorem A |^ B |^ g = A |^ (B * g) by Th35; theorem A |^ g |^ B = A |^ (g * B) by Th35; theorem g |^ A |^ B = g |^ (A * B) by Th35; theorem Th47: A |^ a |^ b = A |^ (a * b) proof thus A |^ a |^ b = A |^ (a * {b}) by Th35 .= A |^ (a * b) by GROUP_2:18; end; theorem a |^ A |^ b = a |^ (A * b) by Th35; theorem a |^ b |^ A = a |^ (b * A) proof thus a |^ b |^ A = {a} |^ {b} |^ A by Th37 .= a |^ (b * A) by Th35; end; theorem Th50: A |^ g = g" * A * g proof A |^ g c= {g}" * A * {g} by Th33; hence A |^ g c= g" * A * g by GROUP_2:3; let x be object; assume x in g" * A * g; then consider a such that A1: x = a * g and A2: a in g" * A by GROUP_2:28; consider b such that A3: a = g" * b and A4: b in A by A2,GROUP_2:27; x = b |^ g by A1,A3; hence thesis by A4,Th41; end; theorem (A * B) |^ a c= (A |^ a) * (B |^ a) by Th34; theorem Th52: A |^ 1_G = A proof thus A |^ 1_G = (1_G)" * A * 1_G by Th50 .= (1_G)" * A by GROUP_2:37 .= 1_G * A by GROUP_1:8 .= A by GROUP_2:37; end; theorem A <> {} implies (1_G) |^ A = {1_G} proof set y = the Element of A; assume A1: A <> {}; then reconsider y as Element of G by TARSKI:def 3; thus (1_G) |^ A c= {1_G} proof let x be object; assume x in (1_G) |^ A; then ex a st x = (1_G) |^ a & a in A by Th42; then x = 1_G by Th17; hence thesis by TARSKI:def 1; end; let x be object; assume x in {1_G}; then x = 1_G by TARSKI:def 1; then (1_G) |^ y = x by Th17; hence thesis by A1,Th42; end; theorem Th54: A |^ a |^ a" = A & A |^ a" |^ a = A proof thus A |^ a |^ a" = A |^ (a * a") by Th47 .= A |^ 1_G by GROUP_1:def 5 .= A by Th52; thus A |^ a" |^ a = A |^ (a" * a) by Th47 .= A |^ 1_G by GROUP_1:def 5 .= A by Th52; end; theorem Th55: 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; set y = the Element of B; assume A2: B <> {}; then reconsider y as Element of G by TARSKI:def 3; thus A |^ B c= A proof let x be object; assume x in A |^ B; then ex a,b st x = a |^ b & a in A & b in B; hence thesis by A1,Th29; end; let x be object; assume A3: x in A; then reconsider a = x as Element of G; a |^ y = x by A1,Th29; hence thesis by A2,A3; end; assume A4: for A,B st B <> {} holds A |^ B = A; now let a,b; {a} = {a} |^ {b} by A4 .= {a |^ b} by Th37; hence a = a |^ b by ZFMISC_1:3; end; hence thesis by Th30; 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 by Th55; assume A1: for A,g holds A |^ g = A; now let a,b; {a} = {a} |^ b by A1 .= {a |^ b} by Th37; hence a = a |^ b by ZFMISC_1:3; end; hence thesis by Th30; 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} by Th55; assume A1: for A,g st A <> {} holds g |^ A = {g}; now let a,b; {a} = a |^ {b} by A1 .= {a |^ b} by Th37; hence a = a |^ b by ZFMISC_1:3; end; hence thesis by Th30; 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:127; the carrier of H1 = a" * carr H * a by A1 .= carr(H) |^ a by Th50; hence thesis; end; correctness by GROUP_2:59; end; theorem Th58: 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; then x in carr H |^ a by Def6; then consider b such that A1: x = b |^ a & b in carr H by Th41; take b; thus thesis by A1; end; given g such that A2: x = g |^ a and A3: g in H; g in carr H by A3; then x in carr H |^ a by A2,Th41; then x in the carrier of H |^ a by Def6; hence thesis; end; theorem Th59: the carrier of H |^ a = a" * H * a proof thus the carrier of H |^ a = carr(H) |^ a by Def6 .= a" * H * a by Th50; end; theorem Th60: H |^ a |^ b = H |^ (a * b) proof the carrier of H |^ a |^ b = carr(H |^ a) |^ b by Def6 .= (carr H |^ a) |^ b by Def6 .= carr H |^ (a * b) by Th47 .= the carrier of H |^ (a * b) by Def6; hence thesis by GROUP_2:59; end; theorem Th61: 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 .= the carrier of H by Th52; hence thesis by GROUP_2:59; end; theorem Th62: 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 Th60 .= H |^ 1_G by GROUP_1:def 5 .= H by Th61; thus H |^ a" |^ a = H |^ (a" * a) by Th60 .= H |^ 1_G by GROUP_1:def 5 .= H by Th61; end; theorem Th63: (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 and A2: h in H1 /\ H2 by Th58; h in H2 by A2,GROUP_2:82; then A3: g in H2 |^ a by A1,Th58; h in H1 by A2,GROUP_2:82; then g in H1 |^ a by A1,Th58; hence thesis by A3,GROUP_2:82; end; assume A4: g in (H1 |^ a) /\ (H2 |^ a); then g in H1 |^ a by GROUP_2:82; then consider b such that A5: g = b |^ a and A6: b in H1 by Th58; g in H2 |^ a by A4,GROUP_2:82; then consider c such that A7: g = c |^ a and A8: c in H2 by Th58; b = c by A5,A7,Th16; then b in (H1 /\ H2) by A6,A8,GROUP_2:82; hence thesis by A5,Th58; end; theorem Th64: card H = card(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 FUNCT_2:sch 4; 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:62; A4: rng g = the carrier of H |^ a proof thus rng g c= the carrier of H |^ a proof let x be object; assume x in rng g; then consider y being object such that A5: y in dom g and A6: g.y = x by FUNCT_1:def 3; reconsider y as Element of H by A2,A5,RELAT_1:62; reconsider y as Element of G by GROUP_2:42; A7: f.y = g.y by A5,FUNCT_1:47; f.y = y |^ a by A1; then x in carr H |^ a by A6,A7,Th41; hence thesis by Def6; end; let x be object; 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 Th41; A10: f.b = b |^ a by A1; g.b = f.b by A3,A9,FUNCT_1:47; hence thesis by A3,A8,A9,A10,FUNCT_1:def 3; end; g is one-to-one proof let x,y be object; assume that A11: x in dom g and A12: y in dom g and A13: g.x = g.y; reconsider b = x, c = y as Element of H by A2,A11,A12,RELAT_1:62; reconsider b,c as Element of G by GROUP_2:42; A14: f.x = b |^ a & f.y = c |^ a by A1; f.x = g.x by A11,FUNCT_1:47; hence thesis by A12,A13,A14,Th16,FUNCT_1:47; end; then the carrier of H,the carrier of H |^ a are_equipotent by A3,A4, WELLORD2:def 4; hence thesis by CARD_1:5; end; theorem Th65: H is finite iff H |^ a is finite proof card H = card(H |^ a) by Th64; then the carrier of H,the carrier of H |^ a are_equipotent by CARD_1:5; hence thesis by CARD_1:38; end; registration let G,a; let H be finite Subgroup of G; cluster H |^ a -> finite; coherence by Th65; end; theorem for H being finite Subgroup of G holds card H = card(H |^ a) by Th64; theorem Th67: (1).G |^ a = (1).G proof A1: the carrier of (1).G = {1_G} by GROUP_2:def 7; the carrier of (1).G |^ a = (carr (1).G) |^ a by Def6 .= {(1_G) |^ a} by A1,Th37 .= {1_G} by Th17; 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; then reconsider H as finite Subgroup of G by Th65; card (1).G = 1 by GROUP_2:69; then card H = 1 by A1,Th64; hence thesis by GROUP_2:70; end; theorem Th69: 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; let h be Element of G; (h |^ a") |^ a = h |^ (a" * a) by Th24 .= h |^ 1_G by GROUP_1:def 5 .= h by Th19; hence thesis by Th58,STRUCT_0:def 5; 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 Th58; hence contradiction by A2,Th16; end; hence contradiction by A1; end; hence thesis by A1,GROUP_2:62; end; theorem Th71: Index H = Index(H |^ a) proof defpred P[object,object] means ex b st \$1 = b * H & \$2 = (b |^ a) * (H |^ a); A1: for x being object st x in Left_Cosets H ex y being object st P[x,y] proof let x be object; assume x in Left_Cosets H; then consider b such that A2: x = b * H by GROUP_2:def 15; reconsider y = (b |^ a) * (H |^ a) as set; take y; take b; thus thesis by A2; end; consider f being Function such that A3: dom f = Left_Cosets H and A4: for x being object st x in Left_Cosets H holds P[x,f.x] from CLASSES1:sch 1(A1); A5: for x,y1,y2 st x in Left_Cosets H & P[x,y1] & P[x,y2] holds y1 = y2 proof set A = carr H; let x,y1,y2; assume x in Left_Cosets H; given b such that A6: x = b * H and A7: y1 = (b |^ a) * (H |^ a); given c such that A8: x = c * H and A9: y2 = (c |^ a) * (H |^ a); thus y1 = (a" * b * a) * (a" * H * a) by A7,Th59 .= (a" * b * a) * (a" * A) * a by GROUP_2:33 .= (a" * b) * (a * (a" * A)) * a by GROUP_2:32 .= a" * b * (a * a" * A) * a by GROUP_2:32 .= a" * b * (1_G * A) * a by GROUP_1:def 5 .= a" * b * A * a by GROUP_2:37 .= a" * (c * H) * a by A6,A8,GROUP_2:32 .= a" * c * A * a by GROUP_2:32 .= a" * c * (1_G * A) * a by GROUP_2:37 .= a" * c * (a * a" * A) * a by GROUP_1:def 5 .= (a" * c) * (a * (a" * A)) * a by GROUP_2:32 .= (a" * c * a) * (a" * A) * a by GROUP_2:32 .= (a" * c * a) * (a" * H * a) by GROUP_2:33 .= y2 by A9,Th59; end; A10: rng f = Left_Cosets(H |^ a) proof thus rng f c= Left_Cosets(H |^ a) proof let x be object; assume x in rng f; then consider y being object such that A11: y in dom f & f.y = x by FUNCT_1:def 3; ex b st y = b * H & x = (b |^ a) * (H |^ a) by A3,A4,A11; hence thesis by GROUP_2:def 15; end; let x be object; assume x in Left_Cosets(H |^ a); then consider b such that A12: x = b * (H |^ a) by GROUP_2:def 15; set c = b |^ a"; A13: x = (c |^ a) * (H |^ a) by A12,Th25; A14: c * H in Left_Cosets H by GROUP_2:def 15; then consider d such that A15: c * H = d * H and A16: f.(c * H) = (d |^ a) * (H |^ a) by A4; (c |^ a) * (H |^ a) = (d |^ a) * (H |^ a) by A5,A14,A15; hence thesis by A3,A13,A14,A16,FUNCT_1:def 3; end; f is one-to-one proof let x,y be object; assume that A17: x in dom f and A18: y in dom f and A19: f.x = f.y; consider c such that A20: y = c * H and A21: f.y = (c |^ a) * (H |^ a) by A3,A4,A18; consider b such that A22: x = b * H and A23: f.x = (b |^ a) * (H |^ a) by A3,A4,A17; A24: (c |^ a)" * (b |^ a) = (c" |^ a) * (b |^ a) by Th26 .= (c" * b) |^ a by Th23; (c |^ a)" * (b |^ a) in H |^ a by A19,A23,A21,GROUP_2:114; then consider d such that A25: (c" * b) |^ a = d |^ a and A26: d in H by A24,Th58; c" * b = d by A25,Th16; hence thesis by A22,A20,A26,GROUP_2:114; end; then Left_Cosets H,Left_Cosets(H |^ a) are_equipotent by A3,A10, WELLORD2:def 4; hence thesis by CARD_1:5; end; theorem Left_Cosets H is finite implies index H = index(H |^ a) proof assume A1: Left_Cosets H is finite; then A2: ex B being finite set st B = Left_Cosets H & index H = card B by GROUP_2:def 18; A3: Index H = Index(H |^ a) by Th71; then Left_Cosets H,Left_Cosets(H |^ a) are_equipotent by CARD_1:5; then Left_Cosets(H |^ a) is finite by A1,CARD_1:38; hence thesis by A2,A3,GROUP_2:def 18; end; theorem Th73: 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 Th59 .= H * a" * a by A1,GROUP_2:112 .= H * (a" * a) by GROUP_2:107 .= H * 1_G by GROUP_1:def 5 .= the carrier of H by GROUP_2:109; hence thesis by GROUP_2:59; end; definition let G,a,b; pred a,b are_conjugated means :Def7: ex g st a = b |^ g; end; notation let G,a,b; antonym a,b are_not_conjugated for a,b are_conjugated; end; theorem Th74: 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,Th25; hence thesis; end; given g such that A2: b = a |^ g; a = b |^ g" by A2,Th25; hence thesis; end; theorem Th75: a,a are_conjugated proof take 1_G; thus thesis by Th19; end; theorem Th76: a,b are_conjugated implies b,a are_conjugated proof given g such that A1: a = b |^ g; b = a |^ g" by A1,Th25; hence thesis; end; definition let G,a,b; redefine pred a,b are_conjugated; reflexivity by Th75; symmetry by Th76; end; theorem Th77: 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,Th24; hence thesis; end; theorem Th78: 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 Th74; hence thesis by Th18; end; suppose 1_G,a are_conjugated; then ex g st 1_G = a |^ g; hence thesis by Th18; end; end; hence thesis; end; theorem Th79: 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 be object; assume A1: x in A; then reconsider b = x as Element of G; ex g st x = a |^ g & g in carr(Omega).G by A1,Th42; then b,a are_conjugated; hence thesis; end; let x be object; assume x in B; then consider b such that A2: x = b and A3: a,b are_conjugated; ex g st b = a |^ g by A3,Def7; hence thesis by A2,Th42; end; definition let G,a; func con_class a -> Subset of G equals a |^ carr (Omega).G; correctness; end; theorem Th80: 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 {b : a,b are_conjugated} by Th79; hence thesis; end; given b such that A1: b = x & a,b are_conjugated; x in {c : a,c are_conjugated} by A1; hence thesis by Th79; end; theorem Th81: 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 Th80; hence thesis; end; assume a,b are_conjugated; hence thesis by Th80; end; theorem Th82: a |^ g in con_class a by Th80,Th74; theorem a in con_class a by Th81; 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 Th81; hence thesis by Th81; 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 by Th81; assume con_class a meets con_class b; then consider x being object such that A1: x in con_class a and A2: x in con_class b by XBOOLE_0:3; reconsider x as Element of G by A1; A3: a,x are_conjugated by A1,Th81; thus con_class a c= con_class b proof let y be object; assume y in con_class a; then consider g such that A4: g = y and A5: a,g are_conjugated by Th80; A6: b,x are_conjugated by A2,Th81; x,a are_conjugated by A1,Th81; then x,g are_conjugated by A5,Th77; then b,g are_conjugated by A6,Th77; hence thesis by A4,Th80; end; let y be object; assume y in con_class b; then consider g such that A7: g = y and A8: b,g are_conjugated by Th80; x,b are_conjugated by A2,Th81; then x,g are_conjugated by A8,Th77; then a,g are_conjugated by A3,Th77; hence thesis by A7,Th80; 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 Th81; hence thesis by A1,TARSKI:def 1; end; assume A2: a = 1_G; thus con_class a c= {1_G} proof let x be object; assume x in con_class a; then consider b such that A3: b = x and A4: a,b are_conjugated by Th80; b = 1_G by A2,A4,Th78; hence thesis by A3,TARSKI:def 1; end; 1_G in con_class a by A2,Th81; hence thesis by ZFMISC_1:31; end; theorem con_class a * A = A * con_class a proof thus con_class a * A c= A * con_class a proof let x be object; assume x in con_class a * A; then consider b,c such that A1: x = b * c and A2: b in con_class a and A3: c in A; reconsider h = x as Element of G by A1; b,a are_conjugated by A2,Th81; then consider g such that A4: b = a |^ g; h |^ c" = c * ((a |^ g) * c) * c" by A1,A4 .= c * (((a |^ g) * c) * c") by GROUP_1:def 3 .= c * (a |^ g) by Th1; then A5: x = (c * (a |^ g)) |^ c by Th25 .= (c |^ c) * (a |^ g |^ c) by Th23 .= c * (a |^ g |^ c) by Th20 .= c * (a |^ (g * c)) by Th24; a |^ (g * c) in con_class a by Th82; hence thesis by A3,A5; end; let x be object; assume x in A * con_class a; then consider b,c such that A6: x = b * c and A7: b in A and A8: c in con_class a; reconsider h = x as Element of G by A6; c,a are_conjugated by A8,Th81; then consider g such that A9: c = a |^ g; h |^ b = (a |^ g) * b by A6,A9,Th1; then A10: x = ((a |^ g) * b) |^ b" by Th25 .= (a |^ g) |^ b" * (b |^ b") by Th23 .= a |^ (g * b") * (b |^ b") by Th24 .= a |^ (g * b") * b by Th1; a |^ (g * b") in con_class a by Th82; hence thesis by A7,A10; end; definition let G,A,B; pred A,B are_conjugated means ex g st A = B |^ g; end; notation let G,A,B; antonym A,B are_not_conjugated for A,B are_conjugated; end; 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,Th54; hence thesis; end; given g such that A2: B = A |^ g; A = B |^ g" by A2,Th54; hence thesis; end; theorem Th89: A,A are_conjugated proof take 1_G; thus thesis by Th52; 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,Th54; hence thesis; 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,Th47; hence thesis; end; theorem Th92: {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 Th88; {b} = {a |^ g} by A1,Th37; then b = a |^ g by ZFMISC_1:3; hence thesis by Th74; end; assume a,b are_conjugated; then consider g such that A2: a |^ g = b by Th74; {b} = {a} |^ g by A2,Th37; hence thesis by Th88; end; theorem Th93: 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; 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 {B : A,B are_conjugated}; coherence proof set X = {B: A,B are_conjugated}; X c= bool the carrier of G proof let x be object; assume x in X; then ex B st x = B & A,B are_conjugated; hence thesis; end; hence thesis; end; end; theorem x in con_class A iff ex B st x = B & A,B are_conjugated; theorem Th95: 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; hence thesis; end; assume A,B are_conjugated; hence thesis; end; theorem A |^ g in con_class A proof A,A |^ g are_conjugated by Th88; hence thesis; end; theorem A in con_class A; 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 Th95; hence thesis; 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 A1: A in con_class A; assume con_class A = con_class B; hence thesis by A1; end; assume con_class A meets con_class B; then consider x being object such that A2: x in con_class A and A3: x in con_class B by XBOOLE_0:3; reconsider x as Subset of G by A2; A4: A,x are_conjugated by A2,Th95; thus con_class A c= con_class B proof let y be object; assume y in con_class A; then consider C such that A5: C = y and A6: A,C are_conjugated; A7: B,x are_conjugated by A3,Th95; x,A are_conjugated by A2,Th95; then x,C are_conjugated by A6,Th91; then B,C are_conjugated by A7,Th91; hence thesis by A5; end; let y be object; assume y in con_class B; then consider C such that A8: C = y and A9: B,C are_conjugated; x,B are_conjugated by A3,Th95; then x,C are_conjugated by A9,Th91; then A,C are_conjugated by A4,Th91; hence thesis by A8; end; theorem Th100: 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 be object; assume x in con_class{a}; then consider B such that A1: x = B and A2: {a},B are_conjugated; consider b such that A3: {a} |^ b = B by A2,Th88; a,a |^ b are_conjugated by Th74; then A4: a |^ b in con_class a by Th81; B = {a |^ b} by A3,Th37; hence thesis by A1,A4; end; let x be object; assume x in A; then consider b such that A5: x = {b} and A6: b in con_class a; b,a are_conjugated by A6,Th81; then {b},{a} are_conjugated by Th92; hence thesis by A5; end; theorem G is finite implies con_class A is finite; definition let G,H1,H2; pred H1,H2 are_conjugated means ex g st the multMagma of H1 = H2 |^ g; end; notation let G,H1,H2; antonym H1,H2 are_not_conjugated for H1,H2 are_conjugated; end; theorem Th102: 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 multMagma of H1 = H2 |^ g; H1 |^ g" = H2 by A1,Th62; hence thesis; end; given g such that A2: H2 = H1 |^ g; H1 = H2 |^ g" by A2,Th62; hence thesis; end; theorem Th103: 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 Th61; end; theorem Th104: 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 multMagma of H1 = H2 |^ g; H2 = H1 |^ g" by A1,Th62; hence thesis; end; definition let G; let H1,H2 be strict Subgroup of G; redefine pred H1,H2 are_conjugated; reflexivity by Th103; symmetry by Th104; end; theorem Th105: 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 multMagma of H1 = H2 |^ g; given h such that A2: the multMagma of H2 = H3 |^ h; H1 = H3 |^ (h * g) by A1,A2,Th60; hence thesis; end; reserve L for Subset of Subgroups G; definition let G,H; func con_class H -> Subset of Subgroups G means :Def12: for x being object holds 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_1:sch 1; take L; let x be object; 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 and A3: H,H1 are_conjugated; x in Subgroups G by A2,Def1; hence thesis by A1,A2,A3; end; uniqueness proof defpred P[object] means ex H3 being strict Subgroup of G st \$1 = H3 & H,H3 are_conjugated; let A1,A2 be Subset of Subgroups G; assume A4: for x being object holds x in A1 iff P[x]; assume A5: for x being object holds x in A2 iff P[x]; thus thesis from XBOOLE_0:sch 2(A4,A5); end; end; theorem Th106: 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 Th107: 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 Th108: 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 Th102; hence thesis by Def12; end; theorem Th109: 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 Th107; hence thesis by Th107; 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 by Th109; assume con_class H1 meets con_class H2; then consider x being object such that A1: x in con_class H1 and A2: x in con_class H2 by XBOOLE_0:3; reconsider x as strict Subgroup of G by A1,Th106; A3: H1,x are_conjugated by A1,Th107; thus con_class H1 c= con_class H2 proof let y be object; assume y in con_class H1; then consider H3 being strict Subgroup of G such that A4: H3 = y and A5: H1,H3 are_conjugated by Def12; A6: H2,x are_conjugated by A2,Th107; x,H1 are_conjugated by A1,Th107; then x,H3 are_conjugated by A5,Th105; then H2,H3 are_conjugated by A6,Th105; hence thesis by A4,Def12; end; let y be object; assume y in con_class H2; then consider H3 being strict Subgroup of G such that A7: H3 = y and A8: H2,H3 are_conjugated by Def12; x,H2 are_conjugated by A2,Th107; then x,H3 are_conjugated by A8,Th105; then H1,H3 are_conjugated by A3,Th105; hence thesis by A7,Def12; end; theorem G is finite implies con_class H is finite by Th15,FINSET_1:1; theorem Th113: 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 multMagma of H1 = H2 |^ a; carr H1 = carr H2 |^ a by A1,Def6; hence thesis; end; given a such that A2: carr H1 = carr H2 |^ a; H1 = H2 |^ a by A2,Def6; hence thesis; end; definition let G; let IT be Subgroup of G; attr IT is normal means :Def13: for a holds IT |^ a = the multMagma of IT; end; registration let G; cluster strict normal for Subgroup of G; existence proof for a holds (1).G |^ a = (1).G by Th67; then (1).G is normal; hence thesis; end; end; reserve N2 for normal Subgroup of G; theorem Th114: (1).G is normal & (Omega).G is normal by Th67,Th69; 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 Th63 .= N1 /\ (N2 |^ a) by Def13 .= the multMagma of (N1 /\ N2) by Def13; end; theorem for H being strict Subgroup of G holds G is commutative Group implies H is normal by Th73; theorem Th117: 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) = a" * H * a by Th59; carr(H |^ a) = the carrier of the multMagma of H by A1,Def13 .= carr H; hence a * H = a * (a" * H) * a by A2,GROUP_2:33 .= a * a" * H * a by GROUP_2:105 .= 1_G * H * a by GROUP_1:def 5 .= H * a by GROUP_2:37; end; assume A3: for a holds a * H = H * a; H is normal proof let a; the carrier of H |^ a = a" * H * a by Th59 .= H * a" * a by A3 .= H * (a" * a) by GROUP_2:107 .= H * 1_G by GROUP_1:def 5 .= the carrier of H by GROUP_2:109; hence thesis by GROUP_2:59; end; hence thesis; end; theorem Th118: 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 Th117; assume A1: for a holds a * H c= H * a; now let a; a" * H c= H * a" by A1; then a * (a" * H) c= a * (H * a") by Th4; then a * a" * H c= a * (H * a") by GROUP_2:105; then 1_G * H c= a * (H * a") by GROUP_1:def 5; then carr H c= a * (H * a") by GROUP_2:109; then carr H c= a * H * a" by GROUP_2:106; then carr H * a c= a * H * a" * a by Th4; then H * a c= a * H * (a" * a) by GROUP_2:34; then H * a c= a * H * 1_G by GROUP_1:def 5; hence H * a c= a * H by GROUP_2:37; end; then for a holds a * H = H * a by A1; hence thesis by Th117; end; theorem Th119: 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 Th117; assume A1: for a holds H * a c= a * H; now let a; H * a" c= a" * H by A1; then a * (H * a") c= a * (a" * H) by Th4; then a * (H * a") c= a * a" * H by GROUP_2:105; then a * (H * a") c= 1_G * H by GROUP_1:def 5; then a * (H * a") c= carr H by GROUP_2:109; then a * H * a" c= carr H by GROUP_2:106; then a * H * a" * a c= carr H * a by Th4; then a * H * (a" * a) c= H * a by GROUP_2:34; then a * H * 1_G c= H * a by GROUP_1:def 5; hence a * H c= H * a by GROUP_2:37; end; then for a holds a * H = H * a by A1; hence thesis by Th117; 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 be object; assume x in A * H; then consider a,h such that A2: x = a * h and A3: a in A and A4: h in H by GROUP_2:94; x in a * H by A2,A4,GROUP_2:103; then x in H * a by A1,Th117; then ex g st x = g * a & g in H by GROUP_2:104; hence thesis by A3; end; let x be object; assume x in H * A; then consider h,a such that A5: x = h * a & h in H and A6: a in A by GROUP_2:95; x in H * a by A5,GROUP_2:104; then x in a * H by A1,Th117; then ex g st x = a * g & g in H by GROUP_2:103; hence thesis by A6; end; assume A7: for A holds A * H = H * A; now let a; thus a * H = {a} * H .= H * {a} by A7 .= H * a; end; hence thesis by Th117; 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 multMagma of H by A1,Def13; hence thesis by GROUP_2:54; end; assume A2: for a holds H is Subgroup of H |^ a; now let a; A3: H |^ a" * a = a"" * H * a" * a by Th59 .= a"" * H * (a" * a) by GROUP_2:34 .= a"" * H * 1_G by GROUP_1:def 5 .= a"" * H by GROUP_2:37 .= a * H; H is Subgroup of H |^ a" by A2; hence H * a c= a * H by A3,Th6; end; hence thesis by Th119; 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 multMagma of H by A1,Def13; hence thesis by GROUP_2:54; end; assume A2: for a holds H |^ a is Subgroup of H; now let a; A3: H |^ a" * a = a"" * H * a" * a by Th59 .= a"" * H * (a" * a) by GROUP_2:34 .= a"" * H * 1_G by GROUP_1:def 5 .= a"" * H by GROUP_2:37 .= a * H; H |^ a" is Subgroup of H by A2; hence a * H c= H * a by A3,Th6; end; hence thesis by Th118; 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 be object; assume x in con_class H; then consider H1 being strict Subgroup of G such that A2: x = H1 and A3: H,H1 are_conjugated by Def12; ex g st H1 = H |^ g by A3,Th102; then x = H by A1,A2,Def13; hence thesis by TARSKI:def 1; end; H in con_class H by Th109; hence thesis by ZFMISC_1:31; end; assume A4: con_class H = {H}; H is normal proof let a; H |^ a in con_class H by Th108; hence thesis by A4,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 be object; assume x in con_class a; then consider b such that A3: x = b and A4: a,b are_conjugated by Th80; consider c such that A5: b = a |^ c by A4,Th74; x in H |^ c by A2,A3,A5,Th58; then x in H by A1,Def13; hence thesis; end; assume A6: 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 A7: b = c |^ a & c in H by Th58; b in con_class c & con_class c c= carr H by A6,A7,Th82; hence thesis; end; assume b in H; then A8: con_class b c= carr H by A6; b |^ a" in con_class b by Th82; then b |^ a" in H by A8; then b |^ a" |^ a in H |^ a by Th58; hence thesis by Th25; end; hence thesis; 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 be object; assume x in carr N1 * carr N2; then consider a,b such that A1: x = a * b and A2: a in carr N1 and A3: b in carr N2; a in N1 by A2; then a |^ b in N1 |^ b by Th58; then a |^ b in the multMagma of N1 by Def13; then A4: a |^ b in carr N1; b * (a |^ b) = b * (b" * (a * b)) by GROUP_1:def 3 .= a * b by Th1; hence thesis by A1,A3,A4; end; theorem Th125: for N1,N2 being strict normal Subgroup of G holds carr N1 * carr N2 = carr N2 * carr N1 by Lm5; 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 Th125; then consider H being strict Subgroup of G such that A1: the carrier of H = A by GROUP_2:78; now let a; thus a * H = a * N1 * C by A1,GROUP_2:29 .= N1 * a * C by Th117 .= B * (a * N2) by GROUP_2:30 .= B * (N2 * a) by Th117 .= H * a by A1,GROUP_2:31; end; then H is normal Subgroup of G by Th117; 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 be object; 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,Th117; hence thesis by GROUP_2:def 16; end; let x be object; 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,Th117; hence thesis by GROUP_2:def 15; 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; ex B being finite set st B = Left_Cosets H & index H = card B by A1, GROUP_2:146; then consider x,y being object such that A3: x <> y and A4: Left_Cosets H = {x,y} by A2,CARD_2:60; carr H in Left_Cosets H by GROUP_2:135; then {x,y} = {x,carr H} or {x,y} = {carr H,y} by A4,TARSKI:def 2; then consider z3 being object such that A5: {x,y} = {carr H,z3}; reconsider z3 as set by TARSKI:1; A6: carr H misses z3 proof z3 in Left_Cosets H by A4,A5,TARSKI:def 2; then A7: ex a st z3 = a * H by GROUP_2:def 15; A8: carr H = 1_G * H by GROUP_2:109; assume not thesis; then carr H = z3 by A7,A8,GROUP_2:115; then A9: {x,y} = {carr H} by A5,ENUMSET1:29; then x = carr H by ZFMISC_1:4; hence thesis by A3,A9,ZFMISC_1:4; end; union Left_Cosets H = the carrier of G & union Left_Cosets H = carr H \/ z3 by A4,A5,GROUP_2:137,ZFMISC_1:75; then A10: union Right_Cosets H = the carrier of G & z3 = (the carrier of G) \ carr H by A6,GROUP_2:137,XBOOLE_1:88; ex C being finite set st C = Right_Cosets H & index H = card C by A1, GROUP_2:146; then consider z1,z2 being object such that A11: z1 <> z2 and A12: Right_Cosets H = {z1,z2} by A2,CARD_2:60; carr H in Right_Cosets H by GROUP_2:135; then {z1,z2} = {z1,carr H} or {z1,z2} = {carr H,z2} by A12,TARSKI:def 2; then consider z4 being object such that A13: {z1,z2} = {carr H,z4}; reconsider z4 as set by TARSKI:1; A14: carr H misses z4 proof z4 in Right_Cosets H by A12,A13,TARSKI:def 2; then A15: ex a st z4 = H * a by GROUP_2:def 16; A16: carr H = H * 1_G by GROUP_2:109; assume not thesis; then carr H = z4 by A15,A16,GROUP_2:121; then A17: {z1,z2} = {carr H} by A13,ENUMSET1:29; then z1 = carr H by ZFMISC_1:4; hence thesis by A11,A17,ZFMISC_1:4; end; A18: union Right_Cosets H = carr H \/ z4 by A12,A13,ZFMISC_1:75; now let c; now per cases; suppose A19: c * H = carr H; then c in H by GROUP_2:113; hence c * H = H * c by A19,GROUP_2:119; end; suppose A20: c * H <> carr H; then not c in H by GROUP_2:113; then A21: H * c <> carr H by GROUP_2:119; c * H in Left_Cosets H by GROUP_2:def 15; then A22: c * H = z3 by A4,A5,A20,TARSKI:def 2; H * c in Right_Cosets H by GROUP_2:def 16; then H * c = z4 by A12,A13,A21,TARSKI:def 2; hence c * H = H * c by A10,A18,A14,A22,XBOOLE_1:88; end; end; hence c * H = H * c; end; hence thesis by Th117; end; definition let G; let A; func Normalizer 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 be object; assume x in X; then ex h st x = h & A |^ h = A; hence thesis; end; then reconsider X as Subset of G; A1: now let a,b; assume a in X & b in X; then ( ex g st a = g & A |^ g = A)& ex h st b = h & A |^ h = A; then A |^ (a * b) = A by Th47; hence a * b in X; end; A2: now let a; assume a in X; then ex b st a = b & A |^ b = A; then A = A |^ a" by Th54; hence a" in X; end; A |^ 1_G = A by Th52; then 1_G in X; hence thesis by A1,A2,GROUP_2:52; end; uniqueness by GROUP_2:59; end; theorem Th129: x in Normalizer A iff ex h st x = h & A |^ h = A proof thus x in Normalizer A implies ex h st x = h & A |^ h = A proof assume x in Normalizer A; then x in the carrier of Normalizer A; 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 Normalizer A by Def14; hence thesis; end; theorem Th130: card con_class A = Index Normalizer A proof defpred P[object,object] means ex a st \$1 = A |^ a & \$2 = Normalizer A * a; A1: for x being object st x in con_class A ex y being object st P[x,y] proof let x be object; assume x in con_class A; then consider B such that A2: x = B and A3: A,B are_conjugated; consider g such that A4: B = A |^ g by A3,Th88; reconsider y = Normalizer A * g as set; take y; take g; thus thesis by A2,A4; end; consider f being Function such that A5: dom f = con_class A and A6: for x being object st x in con_class A holds P[x,f.x] from CLASSES1:sch 1(A1); A7: 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 A8: x = A |^ a and A9: y1 = Normalizer A * a; given b such that A10: x = A |^ b and A11: y2 = Normalizer A * b; A = A |^ b |^ a" by A8,A10,Th54 .= A |^ (b * a") by Th47; then b * a" in Normalizer A by Th129; hence thesis by A9,A11,GROUP_2:120; end; A12: rng f = Right_Cosets Normalizer A proof thus rng f c= Right_Cosets Normalizer A proof let x be object; assume x in rng f; then consider y being object such that A13: y in dom f & f.y = x by FUNCT_1:def 3; ex a st y = A |^ a & x = Normalizer A * a by A5,A6,A13; hence thesis by GROUP_2:def 16; end; let x be object; assume x in Right_Cosets Normalizer A; then consider a such that A14: x = Normalizer A * a by GROUP_2:def 16; set y = A |^ a; A,A |^ a are_conjugated by Th88; then A15: y in con_class A; then ex b st y = A |^ b & f.y = Normalizer A * b by A6; then x = f.y by A7,A14,A15; hence thesis by A5,A15,FUNCT_1:def 3; end; f is one-to-one proof let x,y be object; assume that A16: x in dom f and A17: y in dom f and A18: f.x = f.y; consider b such that A19: y = A |^ b and A20: f.y = Normalizer A * b by A5,A6,A17; consider a such that A21: x = A |^ a and A22: f.x = Normalizer A * a by A5,A6,A16; b * a" in Normalizer A by A18,A22,A20,GROUP_2:120; then ex h st b * a" = h & A |^ h = A by Th129; then A = A |^ b |^ a" by Th47; hence thesis by A21,A19,Th54; end; then con_class A,Right_Cosets Normalizer A are_equipotent by A5,A12, WELLORD2:def 4; hence card con_class A = card Right_Cosets Normalizer A by CARD_1:5 .= Index Normalizer A by GROUP_2:145; end; theorem con_class A is finite or Left_Cosets Normalizer A is finite implies ex C being finite set st C = con_class A & card C = index Normalizer A proof A1: card con_class A = Index Normalizer A by Th130 .= card Left_Cosets Normalizer A; then A2: con_class A,Left_Cosets Normalizer A are_equipotent by CARD_1:5; assume A3: con_class A is finite or Left_Cosets Normalizer A is finite; then reconsider C = con_class A as finite set by A2,CARD_1:38; take C; thus C = con_class A; Left_Cosets Normalizer A is finite by A3,A2,CARD_1:38; hence thesis by A1,GROUP_2:def 18; end; theorem Th132: card con_class a = Index Normalizer{a} proof deffunc F(object) = {\$1}; consider f being Function such that A1: dom f = con_class a and A2: for x being object st x in con_class a holds f.x = F(x) from FUNCT_1:sch 3; A3: rng f = con_class{a} proof thus rng f c= con_class{a} proof let x be object; assume x in rng f; then consider y being object such that A4: y in dom f and A5: f.y = x by FUNCT_1:def 3; 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,A5; hence thesis by Th100; end; let x be object; assume x in con_class{a}; then x in {{b} : b in con_class a} by Th100; then consider b such that A6: x = {b} and A7: b in con_class a; f.b = {b} by A2,A7; hence thesis by A1,A6,A7,FUNCT_1:def 3; end; f is one-to-one proof let x,y be object; assume that A8: x in dom f & y in dom f and A9: f.x = f.y; f.x = {x} & f.y = {y} by A1,A2,A8; hence thesis by A9,ZFMISC_1:3; 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:5 .= Index Normalizer{a} by Th130; end; theorem con_class a is finite or Left_Cosets Normalizer{a} is finite implies ex C being finite set st C = con_class a & card C = index Normalizer{a} proof A1: card con_class a = Index Normalizer {a} by Th132 .= card Left_Cosets Normalizer {a}; then A2: con_class a,Left_Cosets Normalizer {a} are_equipotent by CARD_1:5; assume A3: con_class a is finite or Left_Cosets Normalizer {a} is finite; then reconsider C = con_class a as finite set by A2,CARD_1:38; take C; thus C = con_class a; Left_Cosets Normalizer {a} is finite by A3,A2,CARD_1:38; hence thesis by A1,GROUP_2:def 18; end; definition let G; let H; func Normalizer H -> strict Subgroup of G equals Normalizer carr H; correctness; end; theorem Th134: for H being strict Subgroup of G holds x in Normalizer H iff ex h st x = h & H |^ h = H proof let H be strict Subgroup of G; thus x in Normalizer H implies ex h st x = h & H |^ h = H proof assume x in Normalizer H; then consider a such that A1: x = a and A2: carr H |^ a = carr H by Th129; H |^ a = H by A2,Def6; hence thesis by A1; end; given h such that A3: x = h and A4: H |^ h = H; carr H |^ h = carr H by A4,Def6; hence thesis by A3,Th129; end; theorem Th135: for H being strict Subgroup of G holds card con_class H = Index Normalizer H proof let H be strict Subgroup of G; defpred P[object,object] means ex H1 being strict Subgroup of G st \$1 = H1 & \$2 = carr H1; A1: for x being object st x in con_class H ex y being object st P[x,y] proof let x be object; 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 A2: dom f = con_class H and A3: for x being object st x in con_class H holds P[x,f.x] from CLASSES1:sch 1(A1); A4: rng f = con_class carr H proof thus rng f c= con_class carr H proof let x be object; assume x in rng f; then consider y being object such that A5: y in dom f and A6: f.y = x by FUNCT_1:def 3; consider H1 being strict Subgroup of G such that A7: y = H1 and A8: x = carr H1 by A2,A3,A5,A6; H1,H are_conjugated by A2,A5,A7,Th107; then carr H1,carr H are_conjugated by Th113; hence thesis by A8; end; let x be object; assume x in con_class carr H; then consider B such that A9: B = x and A10: carr H,B are_conjugated; consider H1 being strict Subgroup of G such that A11: the carrier of H1 = B by A10,Th93; B = carr H1 by A11; then H1,H are_conjugated by A10,Th113; then A12: H1 in con_class H by Th107; then ex H2 being strict Subgroup of G st H1 = H2 & f.H1 = carr H2 by A3; hence thesis by A2,A9,A11,A12,FUNCT_1:def 3; end; f is one-to-one proof let x,y be object; assume that A13: x in dom f & y in dom f and A14: f.x = f.y; (ex H1 being strict Subgroup of G st x = H1 & f.x = carr H1 )& ex H2 being strict Subgroup of G st y = H2 & f.y = carr H2 by A2,A3,A13; hence thesis by A14,GROUP_2:59; end; then con_class H,con_class carr H are_equipotent by A2,A4,WELLORD2:def 4; hence card con_class H = card con_class carr H by CARD_1:5 .= Index Normalizer H by Th130; end; theorem for H being strict Subgroup of G holds con_class H is finite or Left_Cosets Normalizer H is finite implies ex C being finite set st C = con_class H & card C = index Normalizer H proof let H be strict Subgroup of G; A1: card con_class H = Index Normalizer H by Th135 .= card Left_Cosets Normalizer H; then A2: con_class H,Left_Cosets Normalizer H are_equipotent by CARD_1:5; assume A3: con_class H is finite or Left_Cosets Normalizer H is finite; then reconsider C = con_class H as finite set by A2,CARD_1:38; take C; thus C = con_class H; Left_Cosets Normalizer H is finite by A3,A2,CARD_1:38; hence thesis by A1,GROUP_2:def 18; end; theorem Th137: for G being strict Group, H being strict Subgroup of G holds H is normal Subgroup of G iff Normalizer H = G proof let G be strict Group, H be strict Subgroup of G; thus H is normal Subgroup of G implies Normalizer 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 Normalizer H by Th134; end; hence thesis by GROUP_2:62; end; assume A2: Normalizer H = G; H is normal proof let a be Element of G; a in Normalizer H by A2; then ex b being Element of G st b = a & H |^ b = H by Th134; hence thesis; end; hence thesis; end; theorem for G being strict Group holds Normalizer (1).G = G proof let G be strict Group; (1).G is normal Subgroup of G by Th114; hence thesis by Th137; end; theorem for G being strict Group holds Normalizer (Omega).G = G proof let G be strict Group; (Omega).G is normal Subgroup of G by Th114; hence thesis by Th137; end;