:: GROUP_2 semantic presentation begin Lm1: for x being set for G being non empty 1-sorted for A being Subset of G st x in A holds x is Element of G ; theorem :: GROUP_2:1 for G being non empty 1-sorted for A being Subset of G st G is finite holds A is finite ; definition let G be Group; let A be Subset of G; funcA " -> Subset of G equals :: GROUP_2:def 1 { (g ") where g is Element of G : g in A } ; coherence { (g ") where g is Element of G : g in A } is Subset of G proof set F = { (g ") where g is Element of G : g in A } ; { (g ") where g is Element of G : g in A } c= the carrier of G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (g ") where g is Element of G : g in A } or x in the carrier of G ) assume x in { (g ") where g is Element of G : g in A } ; ::_thesis: x in the carrier of G then ex g being Element of G st ( x = g " & g in A ) ; hence x in the carrier of G ; ::_thesis: verum end; hence { (g ") where g is Element of G : g in A } is Subset of G ; ::_thesis: verum end; involutiveness for b1, b2 being Subset of G st b1 = { (g ") where g is Element of G : g in b2 } holds b2 = { (g ") where g is Element of G : g in b1 } proof let R, B be Subset of G; ::_thesis: ( R = { (g ") where g is Element of G : g in B } implies B = { (g ") where g is Element of G : g in R } ) assume A1: R = { (g ") where g is Element of G : g in B } ; ::_thesis: B = { (g ") where g is Element of G : g in R } thus B c= { (g ") where g is Element of G : g in R } :: according to XBOOLE_0:def_10 ::_thesis: { (g ") where g is Element of G : g in R } c= B proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in { (g ") where g is Element of G : g in R } ) assume A2: a in B ; ::_thesis: a in { (g ") where g is Element of G : g in R } then reconsider a = a as Element of G ; ( (a ") " = a & a " in R ) by A1, A2; hence a in { (g ") where g is Element of G : g in R } ; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (g ") where g is Element of G : g in R } or a in B ) assume a in { (g ") where g is Element of G : g in R } ; ::_thesis: a in B then consider g being Element of G such that A3: a = g " and A4: g in R ; ex h being Element of G st ( g = h " & h in B ) by A1, A4; hence a in B by A3; ::_thesis: verum end; end; :: deftheorem defines " GROUP_2:def_1_:_ for G being Group for A being Subset of G holds A " = { (g ") where g is Element of G : g in A } ; theorem Th2: :: GROUP_2:2 for x being set for G being Group for A being Subset of G holds ( x in A " iff ex g being Element of G st ( x = g " & g in A ) ) ; theorem :: GROUP_2:3 for G being Group for g being Element of G holds {g} " = {(g ")} proof let G be Group; ::_thesis: for g being Element of G holds {g} " = {(g ")} let g be Element of G; ::_thesis: {g} " = {(g ")} thus {g} " c= {(g ")} :: according to XBOOLE_0:def_10 ::_thesis: {(g ")} c= {g} " proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g} " or x in {(g ")} ) assume x in {g} " ; ::_thesis: x in {(g ")} then consider h being Element of G such that A1: x = h " and A2: h in {g} ; h = g by A2, TARSKI:def_1; hence x in {(g ")} by A1, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g ")} or x in {g} " ) assume x in {(g ")} ; ::_thesis: x in {g} " then A3: x = g " by TARSKI:def_1; g in {g} by TARSKI:def_1; hence x in {g} " by A3; ::_thesis: verum end; theorem :: GROUP_2:4 for G being Group for g, h being Element of G holds {g,h} " = {(g "),(h ")} proof let G be Group; ::_thesis: for g, h being Element of G holds {g,h} " = {(g "),(h ")} let g, h be Element of G; ::_thesis: {g,h} " = {(g "),(h ")} thus {g,h} " c= {(g "),(h ")} :: according to XBOOLE_0:def_10 ::_thesis: {(g "),(h ")} c= {g,h} " proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g,h} " or x in {(g "),(h ")} ) assume x in {g,h} " ; ::_thesis: x in {(g "),(h ")} then consider a being Element of G such that A1: x = a " and A2: a in {g,h} ; ( a = g or a = h ) by A2, TARSKI:def_2; hence x in {(g "),(h ")} by A1, TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g "),(h ")} or x in {g,h} " ) assume x in {(g "),(h ")} ; ::_thesis: x in {g,h} " then A3: ( x = g " or x = h " ) by TARSKI:def_2; ( g in {g,h} & h in {g,h} ) by TARSKI:def_2; hence x in {g,h} " by A3; ::_thesis: verum end; theorem :: GROUP_2:5 for G being Group holds ({} the carrier of G) " = {} proof let G be Group; ::_thesis: ({} the carrier of G) " = {} thus ({} the carrier of G) " c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= ({} the carrier of G) " proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ({} the carrier of G) " or x in {} ) assume x in ({} the carrier of G) " ; ::_thesis: x in {} then ex a being Element of G st ( x = a " & a in {} the carrier of G ) ; hence x in {} ; ::_thesis: verum end; thus {} c= ({} the carrier of G) " by XBOOLE_1:2; ::_thesis: verum end; theorem :: GROUP_2:6 for G being Group holds ([#] the carrier of G) " = the carrier of G proof let G be Group; ::_thesis: ([#] the carrier of G) " = the carrier of G thus ([#] the carrier of G) " c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= ([#] the carrier of G) " let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in ([#] the carrier of G) " ) assume x in the carrier of G ; ::_thesis: x in ([#] the carrier of G) " then reconsider a = x as Element of G ; (a ") " in ([#] the carrier of G) " ; hence x in ([#] the carrier of G) " ; ::_thesis: verum end; theorem Th7: :: GROUP_2:7 for G being Group for A being Subset of G holds ( A <> {} iff A " <> {} ) proof let G be Group; ::_thesis: for A being Subset of G holds ( A <> {} iff A " <> {} ) let A be Subset of G; ::_thesis: ( A <> {} iff A " <> {} ) set x = the Element of A " ; thus ( A <> {} implies A " <> {} ) ::_thesis: ( A " <> {} implies A <> {} ) proof set x = the Element of A; assume A1: A <> {} ; ::_thesis: A " <> {} then reconsider x = the Element of A as Element of G by Lm1; x " in A " by A1; hence A " <> {} ; ::_thesis: verum end; assume A " <> {} ; ::_thesis: A <> {} then ex a being Element of G st ( the Element of A " = a " & a in A ) by Th2; hence A <> {} ; ::_thesis: verum end; registration let G be Group; let A be empty Subset of G; clusterA " -> empty ; coherence A " is empty by Th7; end; registration let G be Group; let A be non empty Subset of G; clusterA " -> non empty ; coherence not A " is empty by Th7; end; definition let G be non empty multMagma ; let A, B be Subset of G; funcA * B -> Subset of G equals :: GROUP_2:def 2 { (g * h) where g, h is Element of G : ( g in A & h in B ) } ; coherence { (g * h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G proof set S = { (g * h) where g, h is Element of G : ( g in A & h in B ) } ; { (g * h) where g, h is Element of G : ( g in A & h in B ) } c= the carrier of G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (g * h) where g, h is Element of G : ( g in A & h in B ) } or x in the carrier of G ) assume x in { (g * h) where g, h is Element of G : ( g in A & h in B ) } ; ::_thesis: x in the carrier of G then ex g, h being Element of G st ( x = g * h & g in A & h in B ) ; hence x in the carrier of G ; ::_thesis: verum end; hence { (g * h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G ; ::_thesis: verum end; end; :: deftheorem defines * GROUP_2:def_2_:_ for G being non empty multMagma for A, B being Subset of G holds A * B = { (g * h) where g, h is Element of G : ( g in A & h in B ) } ; definition let G be non empty commutative multMagma ; let A, B be Subset of G; :: original: * redefine funcA * B -> Subset of G; commutativity for A, B being Subset of G holds A * B = B * A proof let A, B be Subset of G; ::_thesis: A * B = B * A thus A * B c= B * A :: according to XBOOLE_0:def_10 ::_thesis: B * A c= A * B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B or x in B * A ) assume x in A * B ; ::_thesis: x in B * A then ex g, h being Element of G st ( x = g * h & g in A & h in B ) ; hence x in B * A ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B * A or x in A * B ) assume x in B * A ; ::_thesis: x in A * B then ex g, h being Element of G st ( x = g * h & g in B & h in A ) ; hence x in A * B ; ::_thesis: verum end; end; theorem Th8: :: GROUP_2:8 for x being set for G being non empty multMagma for A, B being Subset of G holds ( x in A * B iff ex g, h being Element of G st ( x = g * h & g in A & h in B ) ) ; theorem Th9: :: GROUP_2:9 for G being non empty multMagma for A, B being Subset of G holds ( ( A <> {} & B <> {} ) iff A * B <> {} ) proof let G be non empty multMagma ; ::_thesis: for A, B being Subset of G holds ( ( A <> {} & B <> {} ) iff A * B <> {} ) let A, B be Subset of G; ::_thesis: ( ( A <> {} & B <> {} ) iff A * B <> {} ) thus ( A <> {} & B <> {} implies A * B <> {} ) ::_thesis: ( A * B <> {} implies ( A <> {} & B <> {} ) ) proof assume A1: A <> {} ; ::_thesis: ( not B <> {} or A * B <> {} ) then reconsider x = the Element of A as Element of G by TARSKI:def_3; assume A2: B <> {} ; ::_thesis: A * B <> {} then reconsider y = the Element of B as Element of G by TARSKI:def_3; x * y in A * B by A1, A2; hence A * B <> {} ; ::_thesis: verum end; set x = the Element of A * B; assume A * B <> {} ; ::_thesis: ( A <> {} & B <> {} ) then ex a, b being Element of G st ( the Element of A * B = a * b & a in A & b in B ) by Th8; hence ( A <> {} & B <> {} ) ; ::_thesis: verum end; theorem Th10: :: GROUP_2:10 for G being non empty multMagma for A, B, C being Subset of G st G is associative holds (A * B) * C = A * (B * C) proof let G be non empty multMagma ; ::_thesis: for A, B, C being Subset of G st G is associative holds (A * B) * C = A * (B * C) let A, B, C be Subset of G; ::_thesis: ( G is associative implies (A * B) * C = A * (B * C) ) assume A1: G is associative ; ::_thesis: (A * B) * C = A * (B * C) thus (A * B) * C c= A * (B * C) :: according to XBOOLE_0:def_10 ::_thesis: A * (B * C) c= (A * B) * C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * B) * C or x in A * (B * C) ) assume x in (A * B) * C ; ::_thesis: x in A * (B * C) then consider g, h being Element of G such that A2: x = g * h and A3: g in A * B and A4: h in C ; consider g1, g2 being Element of G such that A5: g = g1 * g2 and A6: g1 in A and A7: g2 in B by A3; ( x = g1 * (g2 * h) & g2 * h in B * C ) by A1, A2, A4, A5, A7, GROUP_1:def_3; hence x in A * (B * C) by A6; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (B * C) or x in (A * B) * C ) assume x in A * (B * C) ; ::_thesis: x in (A * B) * C then consider g, h being Element of G such that A8: x = g * h and A9: g in A and A10: h in B * C ; consider g1, g2 being Element of G such that A11: h = g1 * g2 and A12: g1 in B and A13: g2 in C by A10; A14: g * g1 in A * B by A9, A12; x = (g * g1) * g2 by A1, A8, A11, GROUP_1:def_3; hence x in (A * B) * C by A13, A14; ::_thesis: verum end; theorem :: GROUP_2:11 for G being Group for A, B being Subset of G holds (A * B) " = (B ") * (A ") proof let G be Group; ::_thesis: for A, B being Subset of G holds (A * B) " = (B ") * (A ") let A, B be Subset of G; ::_thesis: (A * B) " = (B ") * (A ") thus (A * B) " c= (B ") * (A ") :: according to XBOOLE_0:def_10 ::_thesis: (B ") * (A ") c= (A * B) " proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * B) " or x in (B ") * (A ") ) assume x in (A * B) " ; ::_thesis: x in (B ") * (A ") then consider g being Element of G such that A1: x = g " and A2: g in A * B ; consider g1, g2 being Element of G such that A3: g = g1 * g2 and A4: ( g1 in A & g2 in B ) by A2; A5: ( g1 " in A " & g2 " in B " ) by A4; x = (g2 ") * (g1 ") by A1, A3, GROUP_1:17; hence x in (B ") * (A ") by A5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B ") * (A ") or x in (A * B) " ) assume x in (B ") * (A ") ; ::_thesis: x in (A * B) " then consider g1, g2 being Element of G such that A6: x = g1 * g2 and A7: g1 in B " and A8: g2 in A " ; consider b being Element of G such that A9: g2 = b " and A10: b in A by A8; consider a being Element of G such that A11: g1 = a " and A12: a in B by A7; A13: b * a in A * B by A12, A10; x = (b * a) " by A6, A11, A9, GROUP_1:17; hence x in (A * B) " by A13; ::_thesis: verum end; theorem :: GROUP_2:12 for G being non empty multMagma for A, B, C being Subset of G holds A * (B \/ C) = (A * B) \/ (A * C) proof let G be non empty multMagma ; ::_thesis: for A, B, C being Subset of G holds A * (B \/ C) = (A * B) \/ (A * C) let A, B, C be Subset of G; ::_thesis: A * (B \/ C) = (A * B) \/ (A * C) thus A * (B \/ C) c= (A * B) \/ (A * C) :: according to XBOOLE_0:def_10 ::_thesis: (A * B) \/ (A * C) c= A * (B \/ C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (B \/ C) or x in (A * B) \/ (A * C) ) assume x in A * (B \/ C) ; ::_thesis: x in (A * B) \/ (A * C) then consider g1, g2 being Element of G such that A1: ( x = g1 * g2 & g1 in A ) and A2: g2 in B \/ C ; ( g2 in B or g2 in C ) by A2, XBOOLE_0:def_3; then ( x in A * B or x in A * C ) by A1; hence x in (A * B) \/ (A * C) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * B) \/ (A * C) or x in A * (B \/ C) ) assume A3: x in (A * B) \/ (A * C) ; ::_thesis: x in A * (B \/ C) now__::_thesis:_x_in_A_*_(B_\/_C) percases ( x in A * B or x in A * C ) by A3, XBOOLE_0:def_3; suppose x in A * B ; ::_thesis: x in A * (B \/ C) then consider g1, g2 being Element of G such that A4: ( x = g1 * g2 & g1 in A ) and A5: g2 in B ; g2 in B \/ C by A5, XBOOLE_0:def_3; hence x in A * (B \/ C) by A4; ::_thesis: verum end; suppose x in A * C ; ::_thesis: x in A * (B \/ C) then consider g1, g2 being Element of G such that A6: ( x = g1 * g2 & g1 in A ) and A7: g2 in C ; g2 in B \/ C by A7, XBOOLE_0:def_3; hence x in A * (B \/ C) by A6; ::_thesis: verum end; end; end; hence x in A * (B \/ C) ; ::_thesis: verum end; theorem :: GROUP_2:13 for G being non empty multMagma for A, B, C being Subset of G holds (A \/ B) * C = (A * C) \/ (B * C) proof let G be non empty multMagma ; ::_thesis: for A, B, C being Subset of G holds (A \/ B) * C = (A * C) \/ (B * C) let A, B, C be Subset of G; ::_thesis: (A \/ B) * C = (A * C) \/ (B * C) thus (A \/ B) * C c= (A * C) \/ (B * C) :: according to XBOOLE_0:def_10 ::_thesis: (A * C) \/ (B * C) c= (A \/ B) * C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A \/ B) * C or x in (A * C) \/ (B * C) ) assume x in (A \/ B) * C ; ::_thesis: x in (A * C) \/ (B * C) then consider g1, g2 being Element of G such that A1: x = g1 * g2 and A2: g1 in A \/ B and A3: g2 in C ; ( g1 in A or g1 in B ) by A2, XBOOLE_0:def_3; then ( x in A * C or x in B * C ) by A1, A3; hence x in (A * C) \/ (B * C) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * C) \/ (B * C) or x in (A \/ B) * C ) assume A4: x in (A * C) \/ (B * C) ; ::_thesis: x in (A \/ B) * C now__::_thesis:_x_in_(A_\/_B)_*_C percases ( x in A * C or x in B * C ) by A4, XBOOLE_0:def_3; suppose x in A * C ; ::_thesis: x in (A \/ B) * C then consider g1, g2 being Element of G such that A5: x = g1 * g2 and A6: g1 in A and A7: g2 in C ; g1 in A \/ B by A6, XBOOLE_0:def_3; hence x in (A \/ B) * C by A5, A7; ::_thesis: verum end; suppose x in B * C ; ::_thesis: x in (A \/ B) * C then consider g1, g2 being Element of G such that A8: x = g1 * g2 and A9: g1 in B and A10: g2 in C ; g1 in A \/ B by A9, XBOOLE_0:def_3; hence x in (A \/ B) * C by A8, A10; ::_thesis: verum end; end; end; hence x in (A \/ B) * C ; ::_thesis: verum end; theorem :: GROUP_2:14 for G being non empty multMagma for A, B, C being Subset of G holds A * (B /\ C) c= (A * B) /\ (A * C) proof let G be non empty multMagma ; ::_thesis: for A, B, C being Subset of G holds A * (B /\ C) c= (A * B) /\ (A * C) let A, B, C be Subset of G; ::_thesis: A * (B /\ C) c= (A * B) /\ (A * C) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (B /\ C) or x in (A * B) /\ (A * C) ) assume x in A * (B /\ C) ; ::_thesis: x in (A * B) /\ (A * C) then consider g1, g2 being Element of G such that A1: ( x = g1 * g2 & g1 in A ) and A2: g2 in B /\ C ; g2 in C by A2, XBOOLE_0:def_4; then A3: x in A * C by A1; g2 in B by A2, XBOOLE_0:def_4; then x in A * B by A1; hence x in (A * B) /\ (A * C) by A3, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: GROUP_2:15 for G being non empty multMagma for A, B, C being Subset of G holds (A /\ B) * C c= (A * C) /\ (B * C) proof let G be non empty multMagma ; ::_thesis: for A, B, C being Subset of G holds (A /\ B) * C c= (A * C) /\ (B * C) let A, B, C be Subset of G; ::_thesis: (A /\ B) * C c= (A * C) /\ (B * C) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) * C or x in (A * C) /\ (B * C) ) assume x in (A /\ B) * C ; ::_thesis: x in (A * C) /\ (B * C) then consider g1, g2 being Element of G such that A1: x = g1 * g2 and A2: g1 in A /\ B and A3: g2 in C ; g1 in B by A2, XBOOLE_0:def_4; then A4: x in B * C by A1, A3; g1 in A by A2, XBOOLE_0:def_4; then x in A * C by A1, A3; hence x in (A * C) /\ (B * C) by A4, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th16: :: GROUP_2:16 for G being non empty multMagma for A being Subset of G holds ( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} ) proof let G be non empty multMagma ; ::_thesis: for A being Subset of G holds ( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} ) let A be Subset of G; ::_thesis: ( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} ) A1: now__::_thesis:_not_A_*_({}_the_carrier_of_G)_<>_{} set x = the Element of A * ({} the carrier of G); assume A * ({} the carrier of G) <> {} ; ::_thesis: contradiction then ex g1, g2 being Element of G st ( the Element of A * ({} the carrier of G) = g1 * g2 & g1 in A & g2 in {} the carrier of G ) by Th8; hence contradiction ; ::_thesis: verum end; now__::_thesis:_not_({}_the_carrier_of_G)_*_A_<>_{} set x = the Element of ({} the carrier of G) * A; assume ({} the carrier of G) * A <> {} ; ::_thesis: contradiction then ex g1, g2 being Element of G st ( the Element of ({} the carrier of G) * A = g1 * g2 & g1 in {} the carrier of G & g2 in A ) by Th8; hence contradiction ; ::_thesis: verum end; hence ( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} ) by A1; ::_thesis: verum end; theorem Th17: :: GROUP_2:17 for G being Group for A being Subset of G st A <> {} holds ( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G ) proof let G be Group; ::_thesis: for A being Subset of G st A <> {} holds ( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G ) let A be Subset of G; ::_thesis: ( A <> {} implies ( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G ) ) set y = the Element of A; assume A1: A <> {} ; ::_thesis: ( ([#] the carrier of G) * A = the carrier of G & A * ([#] the carrier of G) = the carrier of G ) then reconsider y = the Element of A as Element of G by Lm1; thus ([#] the carrier of G) * A = the carrier of G ::_thesis: A * ([#] the carrier of G) = the carrier of G proof set y = the Element of A; reconsider y = the Element of A as Element of G by A1, Lm1; thus ([#] the carrier of G) * A c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= ([#] the carrier of G) * A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in ([#] the carrier of G) * A ) assume x in the carrier of G ; ::_thesis: x in ([#] the carrier of G) * A then reconsider a = x as Element of G ; (a * (y ")) * y = a * ((y ") * y) by GROUP_1:def_3 .= a * (1_ G) by GROUP_1:def_5 .= a by GROUP_1:def_4 ; hence x in ([#] the carrier of G) * A by A1; ::_thesis: verum end; thus A * ([#] the carrier of G) c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= A * ([#] the carrier of G) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in A * ([#] the carrier of G) ) assume x in the carrier of G ; ::_thesis: x in A * ([#] the carrier of G) then reconsider a = x as Element of G ; y * ((y ") * a) = (y * (y ")) * a by GROUP_1:def_3 .= (1_ G) * a by GROUP_1:def_5 .= a by GROUP_1:def_4 ; hence x in A * ([#] the carrier of G) by A1; ::_thesis: verum end; theorem Th18: :: GROUP_2:18 for G being non empty multMagma for g, h being Element of G holds {g} * {h} = {(g * h)} proof let G be non empty multMagma ; ::_thesis: for g, h being Element of G holds {g} * {h} = {(g * h)} let g, h be Element of G; ::_thesis: {g} * {h} = {(g * h)} thus {g} * {h} c= {(g * h)} :: according to XBOOLE_0:def_10 ::_thesis: {(g * h)} c= {g} * {h} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g} * {h} or x in {(g * h)} ) assume x in {g} * {h} ; ::_thesis: x in {(g * h)} then consider g1, g2 being Element of G such that A1: x = g1 * g2 and A2: ( g1 in {g} & g2 in {h} ) ; ( g1 = g & g2 = h ) by A2, TARSKI:def_1; hence x in {(g * h)} by A1, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g * h)} or x in {g} * {h} ) assume x in {(g * h)} ; ::_thesis: x in {g} * {h} then A3: x = g * h by TARSKI:def_1; ( g in {g} & h in {h} ) by TARSKI:def_1; hence x in {g} * {h} by A3; ::_thesis: verum end; theorem :: GROUP_2:19 for G being non empty multMagma for g, g1, g2 being Element of G holds {g} * {g1,g2} = {(g * g1),(g * g2)} proof let G be non empty multMagma ; ::_thesis: for g, g1, g2 being Element of G holds {g} * {g1,g2} = {(g * g1),(g * g2)} let g, g1, g2 be Element of G; ::_thesis: {g} * {g1,g2} = {(g * g1),(g * g2)} thus {g} * {g1,g2} c= {(g * g1),(g * g2)} :: according to XBOOLE_0:def_10 ::_thesis: {(g * g1),(g * g2)} c= {g} * {g1,g2} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g} * {g1,g2} or x in {(g * g1),(g * g2)} ) assume x in {g} * {g1,g2} ; ::_thesis: x in {(g * g1),(g * g2)} then consider h1, h2 being Element of G such that A1: x = h1 * h2 and A2: h1 in {g} and A3: h2 in {g1,g2} ; A4: ( h2 = g1 or h2 = g2 ) by A3, TARSKI:def_2; h1 = g by A2, TARSKI:def_1; hence x in {(g * g1),(g * g2)} by A1, A4, TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g * g1),(g * g2)} or x in {g} * {g1,g2} ) A5: g2 in {g1,g2} by TARSKI:def_2; assume x in {(g * g1),(g * g2)} ; ::_thesis: x in {g} * {g1,g2} then A6: ( x = g * g1 or x = g * g2 ) by TARSKI:def_2; ( g in {g} & g1 in {g1,g2} ) by TARSKI:def_1, TARSKI:def_2; hence x in {g} * {g1,g2} by A6, A5; ::_thesis: verum end; theorem :: GROUP_2:20 for G being non empty multMagma for g1, g2, g being Element of G holds {g1,g2} * {g} = {(g1 * g),(g2 * g)} proof let G be non empty multMagma ; ::_thesis: for g1, g2, g being Element of G holds {g1,g2} * {g} = {(g1 * g),(g2 * g)} let g1, g2, g be Element of G; ::_thesis: {g1,g2} * {g} = {(g1 * g),(g2 * g)} thus {g1,g2} * {g} c= {(g1 * g),(g2 * g)} :: according to XBOOLE_0:def_10 ::_thesis: {(g1 * g),(g2 * g)} c= {g1,g2} * {g} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g1,g2} * {g} or x in {(g1 * g),(g2 * g)} ) assume x in {g1,g2} * {g} ; ::_thesis: x in {(g1 * g),(g2 * g)} then consider h1, h2 being Element of G such that A1: x = h1 * h2 and A2: h1 in {g1,g2} and A3: h2 in {g} ; A4: ( h1 = g1 or h1 = g2 ) by A2, TARSKI:def_2; h2 = g by A3, TARSKI:def_1; hence x in {(g1 * g),(g2 * g)} by A1, A4, TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g1 * g),(g2 * g)} or x in {g1,g2} * {g} ) A5: g2 in {g1,g2} by TARSKI:def_2; assume x in {(g1 * g),(g2 * g)} ; ::_thesis: x in {g1,g2} * {g} then A6: ( x = g1 * g or x = g2 * g ) by TARSKI:def_2; ( g in {g} & g1 in {g1,g2} ) by TARSKI:def_1, TARSKI:def_2; hence x in {g1,g2} * {g} by A6, A5; ::_thesis: verum end; theorem :: GROUP_2:21 for G being non empty multMagma for g, h, g1, g2 being Element of G holds {g,h} * {g1,g2} = {(g * g1),(g * g2),(h * g1),(h * g2)} proof let G be non empty multMagma ; ::_thesis: for g, h, g1, g2 being Element of G holds {g,h} * {g1,g2} = {(g * g1),(g * g2),(h * g1),(h * g2)} let g, h, g1, g2 be Element of G; ::_thesis: {g,h} * {g1,g2} = {(g * g1),(g * g2),(h * g1),(h * g2)} set A = {g,h} * {g1,g2}; set B = {(g * g1),(g * g2),(h * g1),(h * g2)}; thus {g,h} * {g1,g2} c= {(g * g1),(g * g2),(h * g1),(h * g2)} :: according to XBOOLE_0:def_10 ::_thesis: {(g * g1),(g * g2),(h * g1),(h * g2)} c= {g,h} * {g1,g2} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {g,h} * {g1,g2} or x in {(g * g1),(g * g2),(h * g1),(h * g2)} ) assume x in {g,h} * {g1,g2} ; ::_thesis: x in {(g * g1),(g * g2),(h * g1),(h * g2)} then consider h1, h2 being Element of G such that A1: x = h1 * h2 and A2: h1 in {g,h} and A3: h2 in {g1,g2} ; A4: ( h2 = g1 or h2 = g2 ) by A3, TARSKI:def_2; ( h1 = g or h1 = h ) by A2, TARSKI:def_2; hence x in {(g * g1),(g * g2),(h * g1),(h * g2)} by A1, A4, ENUMSET1:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g * g1),(g * g2),(h * g1),(h * g2)} or x in {g,h} * {g1,g2} ) A5: ( g1 in {g1,g2} & g2 in {g1,g2} ) by TARSKI:def_2; assume x in {(g * g1),(g * g2),(h * g1),(h * g2)} ; ::_thesis: x in {g,h} * {g1,g2} then A6: ( x = g * g1 or x = g * g2 or x = h * g1 or x = h * g2 ) by ENUMSET1:def_2; ( g in {g,h} & h in {g,h} ) by TARSKI:def_2; hence x in {g,h} * {g1,g2} by A6, A5; ::_thesis: verum end; theorem Th22: :: GROUP_2:22 for G being Group for A being Subset of G st ( for g1, g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A ) & ( for g being Element of G st g in A holds g " in A ) holds A * A = A proof let G be Group; ::_thesis: for A being Subset of G st ( for g1, g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A ) & ( for g being Element of G st g in A holds g " in A ) holds A * A = A let A be Subset of G; ::_thesis: ( ( for g1, g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A ) & ( for g being Element of G st g in A holds g " in A ) implies A * A = A ) assume that A1: for g1, g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A and A2: for g being Element of G st g in A holds g " in A ; ::_thesis: A * A = A thus A * A c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= A * A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * A or x in A ) assume x in A * A ; ::_thesis: x in A then ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in A & g2 in A ) ; hence x in A by A1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A * A ) assume A3: x in A ; ::_thesis: x in A * A then reconsider a = x as Element of G ; a " in A by A2, A3; then (a ") * a in A by A1, A3; then A4: 1_ G in A by GROUP_1:def_5; (1_ G) * a = a by GROUP_1:def_4; hence x in A * A by A3, A4; ::_thesis: verum end; theorem Th23: :: GROUP_2:23 for G being Group for A being Subset of G st ( for g being Element of G st g in A holds g " in A ) holds A " = A proof let G be Group; ::_thesis: for A being Subset of G st ( for g being Element of G st g in A holds g " in A ) holds A " = A let A be Subset of G; ::_thesis: ( ( for g being Element of G st g in A holds g " in A ) implies A " = A ) assume A1: for g being Element of G st g in A holds g " in A ; ::_thesis: A " = A thus A " c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= A " proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A " or x in A ) assume x in A " ; ::_thesis: x in A then ex g being Element of G st ( x = g " & g in A ) ; hence x in A by A1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A " ) assume A2: x in A ; ::_thesis: x in A " then reconsider a = x as Element of G ; A3: x = (a ") " ; a " in A by A1, A2; hence x in A " by A3; ::_thesis: verum end; theorem :: GROUP_2:24 for G being non empty multMagma for A, B being Subset of G st ( for a, b being Element of G st a in A & b in B holds a * b = b * a ) holds A * B = B * A proof let G be non empty multMagma ; ::_thesis: for A, B being Subset of G st ( for a, b being Element of G st a in A & b in B holds a * b = b * a ) holds A * B = B * A let A, B be Subset of G; ::_thesis: ( ( for a, b being Element of G st a in A & b in B holds a * b = b * a ) implies A * B = B * A ) assume A1: for a, b being Element of G st a in A & b in B holds a * b = b * a ; ::_thesis: A * B = B * A thus A * B c= B * A :: according to XBOOLE_0:def_10 ::_thesis: B * A c= A * B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B or x in B * A ) assume x in A * B ; ::_thesis: x in B * A then consider a, b being Element of G such that A2: x = a * b and A3: ( a in A & b in B ) ; x = b * a by A1, A2, A3; hence x in B * A by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B * A or x in A * B ) assume x in B * A ; ::_thesis: x in A * B then consider b, a being Element of G such that A4: x = b * a and A5: ( b in B & a in A ) ; x = a * b by A1, A4, A5; hence x in A * B by A5; ::_thesis: verum end; Lm2: for A being commutative Group for a, b being Element of A holds a * b = b * a ; theorem Th25: :: GROUP_2:25 for G being non empty multMagma for A, B being Subset of G st G is commutative Group holds A * B = B * A proof let G be non empty multMagma ; ::_thesis: for A, B being Subset of G st G is commutative Group holds A * B = B * A let A, B be Subset of G; ::_thesis: ( G is commutative Group implies A * B = B * A ) assume A1: G is commutative Group ; ::_thesis: A * B = B * A thus A * B c= B * A :: according to XBOOLE_0:def_10 ::_thesis: B * A c= A * B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B or x in B * A ) assume x in A * B ; ::_thesis: x in B * A then consider g, h being Element of G such that A2: x = g * h and A3: ( g in A & h in B ) ; x = h * g by A1, A2, Lm2; hence x in B * A by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B * A or x in A * B ) assume x in B * A ; ::_thesis: x in A * B then consider g, h being Element of G such that A4: x = g * h and A5: ( g in B & h in A ) ; x = h * g by A1, A4, Lm2; hence x in A * B by A5; ::_thesis: verum end; theorem :: GROUP_2:26 for G being commutative Group for A, B being Subset of G holds (A * B) " = (A ") * (B ") proof let G be commutative Group; ::_thesis: for A, B being Subset of G holds (A * B) " = (A ") * (B ") let A, B be Subset of G; ::_thesis: (A * B) " = (A ") * (B ") thus (A * B) " c= (A ") * (B ") :: according to XBOOLE_0:def_10 ::_thesis: (A ") * (B ") c= (A * B) " proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A * B) " or x in (A ") * (B ") ) assume x in (A * B) " ; ::_thesis: x in (A ") * (B ") then consider g being Element of G such that A1: x = g " and A2: g in A * B ; consider g1, g2 being Element of G such that A3: g = g1 * g2 and A4: ( g1 in A & g2 in B ) by A2; A5: ( g1 " in A " & g2 " in B " ) by A4; x = (g1 ") * (g2 ") by A1, A3, GROUP_1:47; hence x in (A ") * (B ") by A5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ") * (B ") or x in (A * B) " ) assume x in (A ") * (B ") ; ::_thesis: x in (A * B) " then consider g1, g2 being Element of G such that A6: x = g1 * g2 and A7: g1 in A " and A8: g2 in B " ; consider b being Element of G such that A9: g2 = b " and A10: b in B by A8; consider a being Element of G such that A11: g1 = a " and A12: a in A by A7; A13: a * b in A * B by A12, A10; x = (a * b) " by A6, A11, A9, GROUP_1:47; hence x in (A * B) " by A13; ::_thesis: verum end; definition let G be non empty multMagma ; let g be Element of G; let A be Subset of G; funcg * A -> Subset of G equals :: GROUP_2:def 3 {g} * A; correctness coherence {g} * A is Subset of G; ; funcA * g -> Subset of G equals :: GROUP_2:def 4 A * {g}; correctness coherence A * {g} is Subset of G; ; end; :: deftheorem defines * GROUP_2:def_3_:_ for G being non empty multMagma for g being Element of G for A being Subset of G holds g * A = {g} * A; :: deftheorem defines * GROUP_2:def_4_:_ for G being non empty multMagma for g being Element of G for A being Subset of G holds A * g = A * {g}; theorem Th27: :: GROUP_2:27 for x being set for G being non empty multMagma for A being Subset of G for g being Element of G holds ( x in g * A iff ex h being Element of G st ( x = g * h & h in A ) ) proof let x be set ; ::_thesis: for G being non empty multMagma for A being Subset of G for g being Element of G holds ( x in g * A iff ex h being Element of G st ( x = g * h & h in A ) ) let G be non empty multMagma ; ::_thesis: for A being Subset of G for g being Element of G holds ( x in g * A iff ex h being Element of G st ( x = g * h & h in A ) ) let A be Subset of G; ::_thesis: for g being Element of G holds ( x in g * A iff ex h being Element of G st ( x = g * h & h in A ) ) let g be Element of G; ::_thesis: ( x in g * A iff ex h being Element of G st ( x = g * h & h in A ) ) thus ( x in g * A implies ex h being Element of G st ( x = g * h & h in A ) ) ::_thesis: ( ex h being Element of G st ( x = g * h & h in A ) implies x in g * A ) proof assume x in g * A ; ::_thesis: ex h being Element of G st ( x = g * h & h in A ) then consider g1, g2 being Element of G such that A1: x = g1 * g2 and A2: g1 in {g} and A3: g2 in A ; g1 = g by A2, TARSKI:def_1; hence ex h being Element of G st ( x = g * h & h in A ) by A1, A3; ::_thesis: verum end; given h being Element of G such that A4: ( x = g * h & h in A ) ; ::_thesis: x in g * A g in {g} by TARSKI:def_1; hence x in g * A by A4; ::_thesis: verum end; theorem Th28: :: GROUP_2:28 for x being set for G being non empty multMagma for A being Subset of G for g being Element of G holds ( x in A * g iff ex h being Element of G st ( x = h * g & h in A ) ) proof let x be set ; ::_thesis: for G being non empty multMagma for A being Subset of G for g being Element of G holds ( x in A * g iff ex h being Element of G st ( x = h * g & h in A ) ) let G be non empty multMagma ; ::_thesis: for A being Subset of G for g being Element of G holds ( x in A * g iff ex h being Element of G st ( x = h * g & h in A ) ) let A be Subset of G; ::_thesis: for g being Element of G holds ( x in A * g iff ex h being Element of G st ( x = h * g & h in A ) ) let g be Element of G; ::_thesis: ( x in A * g iff ex h being Element of G st ( x = h * g & h in A ) ) thus ( x in A * g implies ex h being Element of G st ( x = h * g & h in A ) ) ::_thesis: ( ex h being Element of G st ( x = h * g & h in A ) implies x in A * g ) proof assume x in A * g ; ::_thesis: ex h being Element of G st ( x = h * g & h in A ) then consider g1, g2 being Element of G such that A1: ( x = g1 * g2 & g1 in A ) and A2: g2 in {g} ; g2 = g by A2, TARSKI:def_1; hence ex h being Element of G st ( x = h * g & h in A ) by A1; ::_thesis: verum end; given h being Element of G such that A3: ( x = h * g & h in A ) ; ::_thesis: x in A * g g in {g} by TARSKI:def_1; hence x in A * g by A3; ::_thesis: verum end; theorem :: GROUP_2:29 for G being non empty multMagma for A, B being Subset of G for g being Element of G st G is associative holds (g * A) * B = g * (A * B) by Th10; theorem :: GROUP_2:30 for G being non empty multMagma for A, B being Subset of G for g being Element of G st G is associative holds (A * g) * B = A * (g * B) by Th10; theorem :: GROUP_2:31 for G being non empty multMagma for A, B being Subset of G for g being Element of G st G is associative holds (A * B) * g = A * (B * g) by Th10; theorem Th32: :: GROUP_2:32 for G being non empty multMagma for A being Subset of G for g, h being Element of G st G is associative holds (g * h) * A = g * (h * A) proof let G be non empty multMagma ; ::_thesis: for A being Subset of G for g, h being Element of G st G is associative holds (g * h) * A = g * (h * A) let A be Subset of G; ::_thesis: for g, h being Element of G st G is associative holds (g * h) * A = g * (h * A) let g, h be Element of G; ::_thesis: ( G is associative implies (g * h) * A = g * (h * A) ) assume A1: G is associative ; ::_thesis: (g * h) * A = g * (h * A) thus (g * h) * A = ({g} * {h}) * A by Th18 .= g * (h * A) by A1, Th10 ; ::_thesis: verum end; theorem :: GROUP_2:33 for G being non empty multMagma for A being Subset of G for g, h being Element of G st G is associative holds (g * A) * h = g * (A * h) by Th10; theorem Th34: :: GROUP_2:34 for G being non empty multMagma for A being Subset of G for g, h being Element of G st G is associative holds (A * g) * h = A * (g * h) proof let G be non empty multMagma ; ::_thesis: for A being Subset of G for g, h being Element of G st G is associative holds (A * g) * h = A * (g * h) let A be Subset of G; ::_thesis: for g, h being Element of G st G is associative holds (A * g) * h = A * (g * h) let g, h be Element of G; ::_thesis: ( G is associative implies (A * g) * h = A * (g * h) ) assume G is associative ; ::_thesis: (A * g) * h = A * (g * h) hence (A * g) * h = A * ({g} * {h}) by Th10 .= A * (g * h) by Th18 ; ::_thesis: verum end; theorem :: GROUP_2:35 for G being non empty multMagma for a being Element of G holds ( ({} the carrier of G) * a = {} & a * ({} the carrier of G) = {} ) by Th16; theorem :: GROUP_2:36 for G being Group for a being Element of G holds ( ([#] the carrier of G) * a = the carrier of G & a * ([#] the carrier of G) = the carrier of G ) by Th17; theorem Th37: :: GROUP_2:37 for G being non empty Group-like multMagma for A being Subset of G holds ( (1_ G) * A = A & A * (1_ G) = A ) proof let G be non empty Group-like multMagma ; ::_thesis: for A being Subset of G holds ( (1_ G) * A = A & A * (1_ G) = A ) let A be Subset of G; ::_thesis: ( (1_ G) * A = A & A * (1_ G) = A ) thus (1_ G) * A = A ::_thesis: A * (1_ G) = A proof thus (1_ G) * A c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= (1_ G) * A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (1_ G) * A or x in A ) assume x in (1_ G) * A ; ::_thesis: x in A then ex h being Element of G st ( x = (1_ G) * h & h in A ) by Th27; hence x in A by GROUP_1:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (1_ G) * A ) assume A1: x in A ; ::_thesis: x in (1_ G) * A then reconsider a = x as Element of G ; (1_ G) * a = a by GROUP_1:def_4; hence x in (1_ G) * A by A1, Th27; ::_thesis: verum end; thus A * (1_ G) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= A * (1_ G) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (1_ G) or x in A ) assume x in A * (1_ G) ; ::_thesis: x in A then ex h being Element of G st ( x = h * (1_ G) & h in A ) by Th28; hence x in A by GROUP_1:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A * (1_ G) ) assume A2: x in A ; ::_thesis: x in A * (1_ G) then reconsider a = x as Element of G ; a * (1_ G) = a by GROUP_1:def_4; hence x in A * (1_ G) by A2, Th28; ::_thesis: verum end; theorem :: GROUP_2:38 for G being non empty Group-like multMagma for g being Element of G for A being Subset of G st G is commutative Group holds g * A = A * g by Th25; definition let G be non empty Group-like multMagma ; mode Subgroup of G -> non empty Group-like multMagma means :Def5: :: GROUP_2:def 5 ( the carrier of it c= the carrier of G & the multF of it = the multF of G || the carrier of it ); existence ex b1 being non empty Group-like multMagma st ( the carrier of b1 c= the carrier of G & the multF of b1 = the multF of G || the carrier of b1 ) proof take G ; ::_thesis: ( the carrier of G c= the carrier of G & the multF of G = the multF of G || the carrier of G ) dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1; hence ( the carrier of G c= the carrier of G & the multF of G = the multF of G || the carrier of G ) by RELAT_1:68; ::_thesis: verum end; end; :: deftheorem Def5 defines Subgroup GROUP_2:def_5_:_ for G, b2 being non empty Group-like multMagma holds ( b2 is Subgroup of G iff ( the carrier of b2 c= the carrier of G & the multF of b2 = the multF of G || the carrier of b2 ) ); theorem Th39: :: GROUP_2:39 for G being non empty Group-like multMagma for H being Subgroup of G st G is finite holds H is finite proof let G be non empty Group-like multMagma ; ::_thesis: for H being Subgroup of G st G is finite holds H is finite let H be Subgroup of G; ::_thesis: ( G is finite implies H is finite ) assume A1: G is finite ; ::_thesis: H is finite the carrier of H c= the carrier of G by Def5; hence the carrier of H is finite by A1; :: according to STRUCT_0:def_11 ::_thesis: verum end; theorem Th40: :: GROUP_2:40 for x being set for G being non empty Group-like multMagma for H being Subgroup of G st x in H holds x in G proof let x be set ; ::_thesis: for G being non empty Group-like multMagma for H being Subgroup of G st x in H holds x in G let G be non empty Group-like multMagma ; ::_thesis: for H being Subgroup of G st x in H holds x in G let H be Subgroup of G; ::_thesis: ( x in H implies x in G ) assume x in H ; ::_thesis: x in G then A1: x in the carrier of H by STRUCT_0:def_5; the carrier of H c= the carrier of G by Def5; hence x in G by A1, STRUCT_0:def_5; ::_thesis: verum end; theorem Th41: :: GROUP_2:41 for G being non empty Group-like multMagma for H being Subgroup of G for h being Element of H holds h in G proof let G be non empty Group-like multMagma ; ::_thesis: for H being Subgroup of G for h being Element of H holds h in G let H be Subgroup of G; ::_thesis: for h being Element of H holds h in G let h be Element of H; ::_thesis: h in G h in H by STRUCT_0:def_5; hence h in G by Th40; ::_thesis: verum end; theorem Th42: :: GROUP_2:42 for G being non empty Group-like multMagma for H being Subgroup of G for h being Element of H holds h is Element of G proof let G be non empty Group-like multMagma ; ::_thesis: for H being Subgroup of G for h being Element of H holds h is Element of G let H be Subgroup of G; ::_thesis: for h being Element of H holds h is Element of G let h be Element of H; ::_thesis: h is Element of G h in G by Th41; hence h is Element of G by STRUCT_0:def_5; ::_thesis: verum end; theorem Th43: :: GROUP_2:43 for G being non empty Group-like multMagma for g1, g2 being Element of G for H being Subgroup of G for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds h1 * h2 = g1 * g2 proof let G be non empty Group-like multMagma ; ::_thesis: for g1, g2 being Element of G for H being Subgroup of G for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds h1 * h2 = g1 * g2 let g1, g2 be Element of G; ::_thesis: for H being Subgroup of G for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds h1 * h2 = g1 * g2 let H be Subgroup of G; ::_thesis: for h1, h2 being Element of H st h1 = g1 & h2 = g2 holds h1 * h2 = g1 * g2 let h1, h2 be Element of H; ::_thesis: ( h1 = g1 & h2 = g2 implies h1 * h2 = g1 * g2 ) assume A1: ( h1 = g1 & h2 = g2 ) ; ::_thesis: h1 * h2 = g1 * g2 h1 * h2 = ( the multF of G || the carrier of H) . [h1,h2] by Def5; hence h1 * h2 = g1 * g2 by A1, FUNCT_1:49; ::_thesis: verum end; registration let G be Group; cluster -> associative for Subgroup of G; coherence for b1 being Subgroup of G holds b1 is associative proof let H be Subgroup of G; ::_thesis: H is associative let x, y, z be Element of H; :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z) A1: ( x in the carrier of H & y in the carrier of H ) ; A2: ( z in the carrier of H & x * y in the carrier of H ) ; ( y * z in the carrier of H & the carrier of H c= the carrier of G ) by Def5; then reconsider a = x, b = y, c = z, ab = x * y, bc = y * z as Element of G by A1, A2; thus (x * y) * z = ab * c by Th43 .= (a * b) * c by Th43 .= a * (b * c) by GROUP_1:def_3 .= a * bc by Th43 .= x * (y * z) by Th43 ; ::_thesis: verum end; end; theorem Th44: :: GROUP_2:44 for G being Group for H being Subgroup of G holds 1_ H = 1_ G proof let G be Group; ::_thesis: for H being Subgroup of G holds 1_ H = 1_ G let H be Subgroup of G; ::_thesis: 1_ H = 1_ G set h = the Element of H; reconsider g = the Element of H, g9 = 1_ H as Element of G by Th42; the Element of H * (1_ H) = the Element of H by GROUP_1:def_4; then g * g9 = g by Th43; hence 1_ H = 1_ G by GROUP_1:7; ::_thesis: verum end; theorem :: GROUP_2:45 for G being Group for H1, H2 being Subgroup of G holds 1_ H1 = 1_ H2 proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds 1_ H1 = 1_ H2 let H1, H2 be Subgroup of G; ::_thesis: 1_ H1 = 1_ H2 thus 1_ H1 = 1_ G by Th44 .= 1_ H2 by Th44 ; ::_thesis: verum end; theorem Th46: :: GROUP_2:46 for G being Group for H being Subgroup of G holds 1_ G in H proof let G be Group; ::_thesis: for H being Subgroup of G holds 1_ G in H let H be Subgroup of G; ::_thesis: 1_ G in H 1_ H in H by STRUCT_0:def_5; hence 1_ G in H by Th44; ::_thesis: verum end; theorem :: GROUP_2:47 for G being Group for H1, H2 being Subgroup of G holds 1_ H1 in H2 proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds 1_ H1 in H2 let H1, H2 be Subgroup of G; ::_thesis: 1_ H1 in H2 1_ H1 = 1_ G by Th44; hence 1_ H1 in H2 by Th46; ::_thesis: verum end; theorem Th48: :: GROUP_2:48 for G being Group for g being Element of G for H being Subgroup of G for h being Element of H st h = g holds h " = g " proof let G be Group; ::_thesis: for g being Element of G for H being Subgroup of G for h being Element of H st h = g holds h " = g " let g be Element of G; ::_thesis: for H being Subgroup of G for h being Element of H st h = g holds h " = g " let H be Subgroup of G; ::_thesis: for h being Element of H st h = g holds h " = g " let h be Element of H; ::_thesis: ( h = g implies h " = g " ) reconsider g9 = h " as Element of G by Th42; A1: h * (h ") = 1_ H by GROUP_1:def_5; assume h = g ; ::_thesis: h " = g " then g * g9 = 1_ H by A1, Th43 .= 1_ G by Th44 ; hence h " = g " by GROUP_1:12; ::_thesis: verum end; theorem :: GROUP_2:49 for G being Group for H being Subgroup of G holds inverse_op H = (inverse_op G) | the carrier of H proof let G be Group; ::_thesis: for H being Subgroup of G holds inverse_op H = (inverse_op G) | the carrier of H let H be Subgroup of G; ::_thesis: inverse_op H = (inverse_op G) | the carrier of H the carrier of H c= the carrier of G by Def5; then A1: the carrier of G /\ the carrier of H = the carrier of H by XBOOLE_1:28; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(inverse_op_H)_holds_ (inverse_op_H)_._x_=_(inverse_op_G)_._x let x be set ; ::_thesis: ( x in dom (inverse_op H) implies (inverse_op H) . x = (inverse_op G) . x ) assume x in dom (inverse_op H) ; ::_thesis: (inverse_op H) . x = (inverse_op G) . x then reconsider a = x as Element of H ; reconsider b = a as Element of G by Th42; thus (inverse_op H) . x = a " by GROUP_1:def_6 .= b " by Th48 .= (inverse_op G) . x by GROUP_1:def_6 ; ::_thesis: verum end; ( dom (inverse_op H) = the carrier of H & dom (inverse_op G) = the carrier of G ) by FUNCT_2:def_1; hence inverse_op H = (inverse_op G) | the carrier of H by A1, A2, FUNCT_1:46; ::_thesis: verum end; theorem Th50: :: GROUP_2:50 for G being Group for g1, g2 being Element of G for H being Subgroup of G st g1 in H & g2 in H holds g1 * g2 in H proof let G be Group; ::_thesis: for g1, g2 being Element of G for H being Subgroup of G st g1 in H & g2 in H holds g1 * g2 in H let g1, g2 be Element of G; ::_thesis: for H being Subgroup of G st g1 in H & g2 in H holds g1 * g2 in H let H be Subgroup of G; ::_thesis: ( g1 in H & g2 in H implies g1 * g2 in H ) assume ( g1 in H & g2 in H ) ; ::_thesis: g1 * g2 in H then reconsider h1 = g1, h2 = g2 as Element of H by STRUCT_0:def_5; h1 * h2 in H by STRUCT_0:def_5; hence g1 * g2 in H by Th43; ::_thesis: verum end; theorem Th51: :: GROUP_2:51 for G being Group for g being Element of G for H being Subgroup of G st g in H holds g " in H proof let G be Group; ::_thesis: for g being Element of G for H being Subgroup of G st g in H holds g " in H let g be Element of G; ::_thesis: for H being Subgroup of G st g in H holds g " in H let H be Subgroup of G; ::_thesis: ( g in H implies g " in H ) assume g in H ; ::_thesis: g " in H then reconsider h = g as Element of H by STRUCT_0:def_5; h " in H by STRUCT_0:def_5; hence g " in H by Th48; ::_thesis: verum end; registration let G be Group; cluster non empty strict unital Group-like associative for Subgroup of G; existence ex b1 being Subgroup of G st b1 is strict proof set H = multMagma(# the carrier of G, the multF of G #); multMagma(# the carrier of G, the multF of G #) is Group-like proof reconsider t = 1_ G as Element of multMagma(# the carrier of G, the multF of G #) ; take t ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) holds ( b1 * t = b1 & t * b1 = b1 & ex b2 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st ( b1 * b2 = t & b2 * b1 = t ) ) let a be Element of multMagma(# the carrier of G, the multF of G #); ::_thesis: ( a * t = a & t * a = a & ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st ( a * b1 = t & b1 * a = t ) ) reconsider x = a as Element of G ; thus a * t = x * (1_ G) .= a by GROUP_1:def_4 ; ::_thesis: ( t * a = a & ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st ( a * b1 = t & b1 * a = t ) ) thus t * a = (1_ G) * x .= a by GROUP_1:def_4 ; ::_thesis: ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st ( a * b1 = t & b1 * a = t ) reconsider s = x " as Element of multMagma(# the carrier of G, the multF of G #) ; take s ; ::_thesis: ( a * s = t & s * a = t ) thus a * s = x * (x ") .= t by GROUP_1:def_5 ; ::_thesis: s * a = t thus s * a = (x ") * x .= t by GROUP_1:def_5 ; ::_thesis: verum end; then reconsider H = multMagma(# the carrier of G, the multF of G #) as non empty Group-like multMagma ; the multF of H = the multF of G || the carrier of H by RELSET_1:19; then H is Subgroup of G by Def5; hence ex b1 being Subgroup of G st b1 is strict ; ::_thesis: verum end; end; theorem Th52: :: GROUP_2:52 for G being Group for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A ) & ( for g being Element of G st g in A holds g " in A ) holds ex H being strict Subgroup of G st the carrier of H = A proof let G be Group; ::_thesis: for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A ) & ( for g being Element of G st g in A holds g " in A ) holds ex H being strict Subgroup of G st the carrier of H = A let A be Subset of G; ::_thesis: ( A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A ) & ( for g being Element of G st g in A holds g " in A ) implies ex H being strict Subgroup of G st the carrier of H = A ) assume that A1: A <> {} and A2: for g1, g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A and A3: for g being Element of G st g in A holds g " in A ; ::_thesis: ex H being strict Subgroup of G st the carrier of H = A reconsider D = A as non empty set by A1; set o = the multF of G || A; A4: dom ( the multF of G || A) = (dom the multF of G) /\ [:A,A:] by RELAT_1:61; dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1; then A5: dom ( the multF of G || A) = [:A,A:] by A4, XBOOLE_1:28; rng ( the multF of G || A) c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the multF of G || A) or x in A ) assume x in rng ( the multF of G || A) ; ::_thesis: x in A then consider y being set such that A6: y in dom ( the multF of G || A) and A7: ( the multF of G || A) . y = x by FUNCT_1:def_3; consider y1, y2 being set such that A8: [y1,y2] = y by A4, A6, RELAT_1:def_1; A9: ( y1 in A & y2 in A ) by A5, A6, A8, ZFMISC_1:87; reconsider y1 = y1, y2 = y2 as Element of G by A4, A6, A8, ZFMISC_1:87; x = y1 * y2 by A6, A7, A8, FUNCT_1:47; hence x in A by A2, A9; ::_thesis: verum end; then reconsider o = the multF of G || A as BinOp of D by A5, FUNCT_2:def_1, RELSET_1:4; set H = multMagma(# D,o #); A10: now__::_thesis:_for_g1,_g2_being_Element_of_G for_h1,_h2_being_Element_of_multMagma(#_D,o_#)_st_g1_=_h1_&_g2_=_h2_holds_ g1_*_g2_=_h1_*_h2 let g1, g2 be Element of G; ::_thesis: for h1, h2 being Element of multMagma(# D,o #) st g1 = h1 & g2 = h2 holds g1 * g2 = h1 * h2 let h1, h2 be Element of multMagma(# D,o #); ::_thesis: ( g1 = h1 & g2 = h2 implies g1 * g2 = h1 * h2 ) A11: h1 * h2 = ( the multF of G || A) . [h1,h2] ; assume ( g1 = h1 & g2 = h2 ) ; ::_thesis: g1 * g2 = h1 * h2 hence g1 * g2 = h1 * h2 by A11, FUNCT_1:49; ::_thesis: verum end; multMagma(# D,o #) is Group-like proof set a = the Element of multMagma(# D,o #); reconsider x = the Element of multMagma(# D,o #) as Element of G by Lm1; x " in A by A3; then x * (x ") in A by A2; then reconsider t = 1_ G as Element of multMagma(# D,o #) by GROUP_1:def_5; take t ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of multMagma(# D,o #) holds ( b1 * t = b1 & t * b1 = b1 & ex b2 being Element of the carrier of multMagma(# D,o #) st ( b1 * b2 = t & b2 * b1 = t ) ) let a be Element of multMagma(# D,o #); ::_thesis: ( a * t = a & t * a = a & ex b1 being Element of the carrier of multMagma(# D,o #) st ( a * b1 = t & b1 * a = t ) ) reconsider x = a as Element of G by Lm1; thus a * t = x * (1_ G) by A10 .= a by GROUP_1:def_4 ; ::_thesis: ( t * a = a & ex b1 being Element of the carrier of multMagma(# D,o #) st ( a * b1 = t & b1 * a = t ) ) thus t * a = (1_ G) * x by A10 .= a by GROUP_1:def_4 ; ::_thesis: ex b1 being Element of the carrier of multMagma(# D,o #) st ( a * b1 = t & b1 * a = t ) reconsider s = x " as Element of multMagma(# D,o #) by A3; take s ; ::_thesis: ( a * s = t & s * a = t ) thus a * s = x * (x ") by A10 .= t by GROUP_1:def_5 ; ::_thesis: s * a = t thus s * a = (x ") * x by A10 .= t by GROUP_1:def_5 ; ::_thesis: verum end; then reconsider H = multMagma(# D,o #) as non empty Group-like multMagma ; reconsider H = H as strict Subgroup of G by Def5; take H ; ::_thesis: the carrier of H = A thus the carrier of H = A ; ::_thesis: verum end; theorem Th53: :: GROUP_2:53 for G being Group for H being Subgroup of G st G is commutative Group holds H is commutative proof let G be Group; ::_thesis: for H being Subgroup of G st G is commutative Group holds H is commutative let H be Subgroup of G; ::_thesis: ( G is commutative Group implies H is commutative ) assume A1: G is commutative Group ; ::_thesis: H is commutative thus for h1, h2 being Element of H holds h1 * h2 = h2 * h1 :: according to GROUP_1:def_12 ::_thesis: verum proof let h1, h2 be Element of H; ::_thesis: h1 * h2 = h2 * h1 reconsider g1 = h1, g2 = h2 as Element of G by Th42; thus h1 * h2 = g1 * g2 by Th43 .= g2 * g1 by A1, Lm2 .= h2 * h1 by Th43 ; ::_thesis: verum end; end; registration let G be commutative Group; cluster -> commutative for Subgroup of G; coherence for b1 being Subgroup of G holds b1 is commutative by Th53; end; theorem Th54: :: GROUP_2:54 for G being Group holds G is Subgroup of G proof let G be Group; ::_thesis: G is Subgroup of G dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1; hence ( the carrier of G c= the carrier of G & the multF of G = the multF of G || the carrier of G ) by RELAT_1:68; :: according to GROUP_2:def_5 ::_thesis: verum end; theorem Th55: :: GROUP_2:55 for G1, G2 being Group st G1 is Subgroup of G2 & G2 is Subgroup of G1 holds multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) proof let G1, G2 be Group; ::_thesis: ( G1 is Subgroup of G2 & G2 is Subgroup of G1 implies multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) ) assume that A1: G1 is Subgroup of G2 and A2: G2 is Subgroup of G1 ; ::_thesis: multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) set g = the multF of G2; set f = the multF of G1; set B = the carrier of G2; set A = the carrier of G1; A3: ( the carrier of G1 c= the carrier of G2 & the carrier of G2 c= the carrier of G1 ) by A1, A2, Def5; then A4: the carrier of G1 = the carrier of G2 by XBOOLE_0:def_10; the multF of G1 = the multF of G2 || the carrier of G1 by A1, Def5 .= ( the multF of G1 || the carrier of G2) || the carrier of G1 by A2, Def5 .= the multF of G1 || the carrier of G2 by A4, RELAT_1:72 .= the multF of G2 by A2, Def5 ; hence multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th56: :: GROUP_2:56 for G1, G2, G3 being Group st G1 is Subgroup of G2 & G2 is Subgroup of G3 holds G1 is Subgroup of G3 proof let G1, G2, G3 be Group; ::_thesis: ( G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3 ) assume that A1: G1 is Subgroup of G2 and A2: G2 is Subgroup of G3 ; ::_thesis: G1 is Subgroup of G3 set h = the multF of G3; set C = the carrier of G3; set B = the carrier of G2; set A = the carrier of G1; A3: the carrier of G1 c= the carrier of G2 by A1, Def5; then A4: [: the carrier of G1, the carrier of G1:] c= [: the carrier of G2, the carrier of G2:] by ZFMISC_1:96; the carrier of G2 c= the carrier of G3 by A2, Def5; then A5: the carrier of G1 c= the carrier of G3 by A3, XBOOLE_1:1; the multF of G1 = the multF of G2 || the carrier of G1 by A1, Def5 .= ( the multF of G3 || the carrier of G2) || the carrier of G1 by A2, Def5 .= the multF of G3 || the carrier of G1 by A4, FUNCT_1:51 ; hence G1 is Subgroup of G3 by A5, Def5; ::_thesis: verum end; theorem Th57: :: GROUP_2:57 for G being Group for H1, H2 being Subgroup of G st the carrier of H1 c= the carrier of H2 holds H1 is Subgroup of H2 proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G st the carrier of H1 c= the carrier of H2 holds H1 is Subgroup of H2 let H1, H2 be Subgroup of G; ::_thesis: ( the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2 ) set A = the carrier of H1; set B = the carrier of H2; set h = the multF of G; assume A1: the carrier of H1 c= the carrier of H2 ; ::_thesis: H1 is Subgroup of H2 hence the carrier of H1 c= the carrier of H2 ; :: according to GROUP_2:def_5 ::_thesis: the multF of H1 = the multF of H2 || the carrier of H1 A2: [: the carrier of H1, the carrier of H1:] c= [: the carrier of H2, the carrier of H2:] by A1, ZFMISC_1:96; ( the multF of H1 = the multF of G || the carrier of H1 & the multF of H2 = the multF of G || the carrier of H2 ) by Def5; hence the multF of H1 = the multF of H2 || the carrier of H1 by A2, FUNCT_1:51; ::_thesis: verum end; theorem Th58: :: GROUP_2:58 for G being Group for H1, H2 being Subgroup of G st ( for g being Element of G st g in H1 holds g in H2 ) holds H1 is Subgroup of H2 proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G st ( for g being Element of G st g in H1 holds g in H2 ) holds H1 is Subgroup of H2 let H1, H2 be Subgroup of G; ::_thesis: ( ( for g being Element of G st g in H1 holds g in H2 ) implies H1 is Subgroup of H2 ) assume A1: for g being Element of G st g in H1 holds g in H2 ; ::_thesis: H1 is Subgroup of H2 the carrier of H1 c= the carrier of H2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of H1 or x in the carrier of H2 ) assume x in the carrier of H1 ; ::_thesis: x in the carrier of H2 then reconsider g = x as Element of H1 ; reconsider g = g as Element of G by Th42; g in H1 by STRUCT_0:def_5; then g in H2 by A1; hence x in the carrier of H2 by STRUCT_0:def_5; ::_thesis: verum end; hence H1 is Subgroup of H2 by Th57; ::_thesis: verum end; theorem Th59: :: GROUP_2:59 for G being Group for H1, H2 being Subgroup of G st the carrier of H1 = the carrier of H2 holds multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G st the carrier of H1 = the carrier of H2 holds multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) let H1, H2 be Subgroup of G; ::_thesis: ( the carrier of H1 = the carrier of H2 implies multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) ) assume the carrier of H1 = the carrier of H2 ; ::_thesis: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) then ( H1 is Subgroup of H2 & H2 is Subgroup of H1 ) by Th57; hence multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) by Th55; ::_thesis: verum end; theorem Th60: :: GROUP_2:60 for G being Group for H1, H2 being Subgroup of G st ( for g being Element of G holds ( g in H1 iff g in H2 ) ) holds multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G st ( for g being Element of G holds ( g in H1 iff g in H2 ) ) holds multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) let H1, H2 be Subgroup of G; ::_thesis: ( ( for g being Element of G holds ( g in H1 iff g in H2 ) ) implies multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) ) assume for g being Element of G holds ( g in H1 iff g in H2 ) ; ::_thesis: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) then ( H1 is Subgroup of H2 & H2 is Subgroup of H1 ) by Th58; hence multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) by Th55; ::_thesis: verum end; definition let G be Group; let H1, H2 be strict Subgroup of G; :: original: = redefine predH1 = H2 means :: GROUP_2:def 6 for g being Element of G holds ( g in H1 iff g in H2 ); compatibility ( H1 = H2 iff for g being Element of G holds ( g in H1 iff g in H2 ) ) by Th60; end; :: deftheorem defines = GROUP_2:def_6_:_ for G being Group for H1, H2 being strict Subgroup of G holds ( H1 = H2 iff for g being Element of G holds ( g in H1 iff g in H2 ) ); theorem Th61: :: GROUP_2:61 for G being Group for H being Subgroup of G st the carrier of G c= the carrier of H holds multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) proof let G be Group; ::_thesis: for H being Subgroup of G st the carrier of G c= the carrier of H holds multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) let H be Subgroup of G; ::_thesis: ( the carrier of G c= the carrier of H implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) ) assume A1: the carrier of G c= the carrier of H ; ::_thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) A2: G is Subgroup of G by Th54; the carrier of H c= the carrier of G by Def5; then the carrier of G = the carrier of H by A1, XBOOLE_0:def_10; hence multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by A2, Th59; ::_thesis: verum end; theorem Th62: :: GROUP_2:62 for G being Group for H being Subgroup of G st ( for g being Element of G holds g in H ) holds multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) proof let G be Group; ::_thesis: for H being Subgroup of G st ( for g being Element of G holds g in H ) holds multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) let H be Subgroup of G; ::_thesis: ( ( for g being Element of G holds g in H ) implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) ) assume for g being Element of G holds g in H ; ::_thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) then A1: for g being Element of G holds ( ( g in H implies g in G ) & ( g in G implies g in H ) ) by STRUCT_0:def_5; G is Subgroup of G by Th54; hence multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by A1, Th60; ::_thesis: verum end; definition let G be Group; func (1). G -> strict Subgroup of G means :Def7: :: GROUP_2:def 7 the carrier of it = {(1_ G)}; existence ex b1 being strict Subgroup of G st the carrier of b1 = {(1_ G)} proof A1: now__::_thesis:_for_g_being_Element_of_G_st_g_in_{(1__G)}_holds_ g_"_in_{(1__G)} let g be Element of G; ::_thesis: ( g in {(1_ G)} implies g " in {(1_ G)} ) assume g in {(1_ G)} ; ::_thesis: g " in {(1_ G)} then g = 1_ G by TARSKI:def_1; then g " = 1_ G by GROUP_1:8; hence g " in {(1_ G)} by TARSKI:def_1; ::_thesis: verum end; now__::_thesis:_for_g1,_g2_being_Element_of_G_st_g1_in_{(1__G)}_&_g2_in_{(1__G)}_holds_ g1_*_g2_in_{(1__G)} let g1, g2 be Element of G; ::_thesis: ( g1 in {(1_ G)} & g2 in {(1_ G)} implies g1 * g2 in {(1_ G)} ) assume ( g1 in {(1_ G)} & g2 in {(1_ G)} ) ; ::_thesis: g1 * g2 in {(1_ G)} then ( g1 = 1_ G & g2 = 1_ G ) by TARSKI:def_1; then g1 * g2 = 1_ G by GROUP_1:def_4; hence g1 * g2 in {(1_ G)} by TARSKI:def_1; ::_thesis: verum end; hence ex b1 being strict Subgroup of G st the carrier of b1 = {(1_ G)} by A1, Th52; ::_thesis: verum end; uniqueness for b1, b2 being strict Subgroup of G st the carrier of b1 = {(1_ G)} & the carrier of b2 = {(1_ G)} holds b1 = b2 by Th59; end; :: deftheorem Def7 defines (1). GROUP_2:def_7_:_ for G being Group for b2 being strict Subgroup of G holds ( b2 = (1). G iff the carrier of b2 = {(1_ G)} ); definition let G be Group; func (Omega). G -> strict Subgroup of G equals :: GROUP_2:def 8 multMagma(# the carrier of G, the multF of G #); coherence multMagma(# the carrier of G, the multF of G #) is strict Subgroup of G proof set H = multMagma(# the carrier of G, the multF of G #); multMagma(# the carrier of G, the multF of G #) is Group-like proof consider e9 being Element of G such that A1: for h being Element of G holds ( h * e9 = h & e9 * h = h & ex g being Element of G st ( h * g = e9 & g * h = e9 ) ) by GROUP_1:def_2; reconsider e = e9 as Element of multMagma(# the carrier of G, the multF of G #) ; take e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) holds ( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st ( b1 * b2 = e & b2 * b1 = e ) ) let h be Element of multMagma(# the carrier of G, the multF of G #); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st ( h * b1 = e & b1 * h = e ) ) reconsider h9 = h as Element of G ; consider g9 being Element of G such that A2: ( h9 * g9 = e9 & g9 * h9 = e9 ) by A1; ( h9 * e9 = h9 & e9 * h9 = h9 ) by A1; hence ( h * e = h & e * h = h ) ; ::_thesis: ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st ( h * b1 = e & b1 * h = e ) reconsider g = g9 as Element of multMagma(# the carrier of G, the multF of G #) ; take g ; ::_thesis: ( h * g = e & g * h = e ) thus ( h * g = e & g * h = e ) by A2; ::_thesis: verum end; then reconsider H = multMagma(# the carrier of G, the multF of G #) as non empty Group-like multMagma ; dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1; then the multF of H = the multF of G || the carrier of H by RELAT_1:68; hence multMagma(# the carrier of G, the multF of G #) is strict Subgroup of G by Def5; ::_thesis: verum end; projectivity for b1 being strict Subgroup of G for b2 being Group st b1 = multMagma(# the carrier of b2, the multF of b2 #) holds b1 = multMagma(# the carrier of b1, the multF of b1 #) ; end; :: deftheorem defines (Omega). GROUP_2:def_8_:_ for G being Group holds (Omega). G = multMagma(# the carrier of G, the multF of G #); theorem Th63: :: GROUP_2:63 for G being Group for H being Subgroup of G holds (1). H = (1). G proof let G be Group; ::_thesis: for H being Subgroup of G holds (1). H = (1). G let H be Subgroup of G; ::_thesis: (1). H = (1). G A1: 1_ H = 1_ G by Th44; ( (1). H is Subgroup of G & the carrier of ((1). H) = {(1_ H)} ) by Def7, Th56; hence (1). H = (1). G by A1, Def7; ::_thesis: verum end; theorem :: GROUP_2:64 for G being Group for H1, H2 being Subgroup of G holds (1). H1 = (1). H2 proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds (1). H1 = (1). H2 let H1, H2 be Subgroup of G; ::_thesis: (1). H1 = (1). H2 thus (1). H1 = (1). G by Th63 .= (1). H2 by Th63 ; ::_thesis: verum end; theorem Th65: :: GROUP_2:65 for G being Group for H being Subgroup of G holds (1). G is Subgroup of H proof let G be Group; ::_thesis: for H being Subgroup of G holds (1). G is Subgroup of H let H be Subgroup of G; ::_thesis: (1). G is Subgroup of H (1). G = (1). H by Th63; hence (1). G is Subgroup of H ; ::_thesis: verum end; theorem :: GROUP_2:66 for G being strict Group for H being Subgroup of G holds H is Subgroup of (Omega). G ; theorem :: GROUP_2:67 for G being strict Group holds G is Subgroup of (Omega). G ; theorem Th68: :: GROUP_2:68 for G being Group holds (1). G is finite proof let G be Group; ::_thesis: (1). G is finite the carrier of ((1). G) = {(1_ G)} by Def7; hence (1). G is finite ; ::_thesis: verum end; registration let G be Group; cluster (1). G -> finite strict ; coherence (1). G is finite by Th68; cluster non empty finite strict unital Group-like associative for Subgroup of G; existence ex b1 being Subgroup of G st ( b1 is strict & b1 is finite ) proof take (1). G ; ::_thesis: ( (1). G is strict & (1). G is finite ) thus ( (1). G is strict & (1). G is finite ) ; ::_thesis: verum end; end; registration cluster non empty finite strict unital Group-like associative for multMagma ; existence ex b1 being Group st ( b1 is strict & b1 is finite ) proof set G = the Group; take (1). the Group ; ::_thesis: ( (1). the Group is strict & (1). the Group is finite ) thus ( (1). the Group is strict & (1). the Group is finite ) ; ::_thesis: verum end; end; registration let G be finite Group; cluster -> finite for Subgroup of G; coherence for b1 being Subgroup of G holds b1 is finite by Th39; end; theorem Th69: :: GROUP_2:69 for G being Group holds card ((1). G) = 1 proof let G be Group; ::_thesis: card ((1). G) = 1 the carrier of ((1). G) = {(1_ G)} by Def7; hence card ((1). G) = 1 by CARD_1:30; ::_thesis: verum end; theorem Th70: :: GROUP_2:70 for G being Group for H being finite strict Subgroup of G st card H = 1 holds H = (1). G proof let G be Group; ::_thesis: for H being finite strict Subgroup of G st card H = 1 holds H = (1). G let H be finite strict Subgroup of G; ::_thesis: ( card H = 1 implies H = (1). G ) assume card H = 1 ; ::_thesis: H = (1). G then consider x being set such that A1: the carrier of H = {x} by CARD_2:42; 1_ G in H by Th46; then 1_ G in the carrier of H by STRUCT_0:def_5; then x = 1_ G by A1, TARSKI:def_1; hence H = (1). G by A1, Def7; ::_thesis: verum end; theorem :: GROUP_2:71 for G being Group for H being Subgroup of G holds card H c= card G proof let G be Group; ::_thesis: for H being Subgroup of G holds card H c= card G let H be Subgroup of G; ::_thesis: card H c= card G the carrier of H c= the carrier of G by Def5; hence card H c= card G by CARD_1:11; ::_thesis: verum end; theorem :: GROUP_2:72 for G being finite Group for H being Subgroup of G holds card H <= card G proof let G be finite Group; ::_thesis: for H being Subgroup of G holds card H <= card G let H be Subgroup of G; ::_thesis: card H <= card G the carrier of H c= the carrier of G by Def5; hence card H <= card G by NAT_1:43; ::_thesis: verum end; theorem :: GROUP_2:73 for G being finite Group for H being Subgroup of G st card G = card H holds multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) proof let G be finite Group; ::_thesis: for H being Subgroup of G st card G = card H holds multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) let H be Subgroup of G; ::_thesis: ( card G = card H implies multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) ) assume A1: card G = card H ; ::_thesis: multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) A2: the carrier of H c= the carrier of G by Def5; the carrier of H = the carrier of G proof assume the carrier of H <> the carrier of G ; ::_thesis: contradiction then the carrier of H c< the carrier of G by A2, XBOOLE_0:def_8; hence contradiction by A1, CARD_2:48; ::_thesis: verum end; hence multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by Th61; ::_thesis: verum end; definition let G be Group; let H be Subgroup of G; func carr H -> Subset of G equals :: GROUP_2:def 9 the carrier of H; coherence the carrier of H is Subset of G by Def5; end; :: deftheorem defines carr GROUP_2:def_9_:_ for G being Group for H being Subgroup of G holds carr H = the carrier of H; theorem Th74: :: GROUP_2:74 for G being Group for g1, g2 being Element of G for H being Subgroup of G st g1 in carr H & g2 in carr H holds g1 * g2 in carr H proof let G be Group; ::_thesis: for g1, g2 being Element of G for H being Subgroup of G st g1 in carr H & g2 in carr H holds g1 * g2 in carr H let g1, g2 be Element of G; ::_thesis: for H being Subgroup of G st g1 in carr H & g2 in carr H holds g1 * g2 in carr H let H be Subgroup of G; ::_thesis: ( g1 in carr H & g2 in carr H implies g1 * g2 in carr H ) assume ( g1 in carr H & g2 in carr H ) ; ::_thesis: g1 * g2 in carr H then ( g1 in H & g2 in H ) by STRUCT_0:def_5; then g1 * g2 in H by Th50; hence g1 * g2 in carr H by STRUCT_0:def_5; ::_thesis: verum end; theorem Th75: :: GROUP_2:75 for G being Group for g being Element of G for H being Subgroup of G st g in carr H holds g " in carr H proof let G be Group; ::_thesis: for g being Element of G for H being Subgroup of G st g in carr H holds g " in carr H let g be Element of G; ::_thesis: for H being Subgroup of G st g in carr H holds g " in carr H let H be Subgroup of G; ::_thesis: ( g in carr H implies g " in carr H ) assume g in carr H ; ::_thesis: g " in carr H then g in H by STRUCT_0:def_5; then g " in H by Th51; hence g " in carr H by STRUCT_0:def_5; ::_thesis: verum end; theorem :: GROUP_2:76 for G being Group for H being Subgroup of G holds (carr H) * (carr H) = carr H proof let G be Group; ::_thesis: for H being Subgroup of G holds (carr H) * (carr H) = carr H let H be Subgroup of G; ::_thesis: (carr H) * (carr H) = carr H A1: for g being Element of G st g in carr H holds g " in carr H by Th75; for g1, g2 being Element of G st g1 in carr H & g2 in carr H holds g1 * g2 in carr H by Th74; hence (carr H) * (carr H) = carr H by A1, Th22; ::_thesis: verum end; theorem :: GROUP_2:77 for G being Group for H being Subgroup of G holds (carr H) " = carr H proof let G be Group; ::_thesis: for H being Subgroup of G holds (carr H) " = carr H let H be Subgroup of G; ::_thesis: (carr H) " = carr H for g being Element of G st g in carr H holds g " in carr H by Th75; hence (carr H) " = carr H by Th23; ::_thesis: verum end; theorem Th78: :: GROUP_2:78 for G being Group for H1, H2 being Subgroup of G holds ( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) ) proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds ( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) ) let H1, H2 be Subgroup of G; ::_thesis: ( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) ) thus ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) ::_thesis: ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) proof assume A1: (carr H1) * (carr H2) = (carr H2) * (carr H1) ; ::_thesis: ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) A2: now__::_thesis:_for_g_being_Element_of_G_st_g_in_(carr_H1)_*_(carr_H2)_holds_ g_"_in_(carr_H1)_*_(carr_H2) let g be Element of G; ::_thesis: ( g in (carr H1) * (carr H2) implies g " in (carr H1) * (carr H2) ) assume A3: g in (carr H1) * (carr H2) ; ::_thesis: g " in (carr H1) * (carr H2) then consider a, b being Element of G such that A4: g = a * b and a in carr H1 and b in carr H2 ; consider b1, a1 being Element of G such that A5: a * b = b1 * a1 and A6: ( b1 in carr H2 & a1 in carr H1 ) by A1, A3, A4; A7: ( a1 " in carr H1 & b1 " in carr H2 ) by A6, Th75; g " = (a1 ") * (b1 ") by A4, A5, GROUP_1:17; hence g " in (carr H1) * (carr H2) by A7; ::_thesis: verum end; A8: now__::_thesis:_for_g1,_g2_being_Element_of_G_st_g1_in_(carr_H1)_*_(carr_H2)_&_g2_in_(carr_H1)_*_(carr_H2)_holds_ g1_*_g2_in_(carr_H1)_*_(carr_H2) let g1, g2 be Element of G; ::_thesis: ( g1 in (carr H1) * (carr H2) & g2 in (carr H1) * (carr H2) implies g1 * g2 in (carr H1) * (carr H2) ) assume that A9: g1 in (carr H1) * (carr H2) and A10: g2 in (carr H1) * (carr H2) ; ::_thesis: g1 * g2 in (carr H1) * (carr H2) consider a1, b1 being Element of G such that A11: g1 = a1 * b1 and A12: a1 in carr H1 and A13: b1 in carr H2 by A9; consider a2, b2 being Element of G such that A14: g2 = a2 * b2 and A15: a2 in carr H1 and A16: b2 in carr H2 by A10; b1 * a2 in (carr H1) * (carr H2) by A1, A13, A15; then consider a, b being Element of G such that A17: b1 * a2 = a * b and A18: a in carr H1 and A19: b in carr H2 ; A20: b * b2 in carr H2 by A16, A19, Th74; g1 * g2 = ((a1 * b1) * a2) * b2 by A11, A14, GROUP_1:def_3 .= (a1 * (b1 * a2)) * b2 by GROUP_1:def_3 ; then A21: g1 * g2 = ((a1 * a) * b) * b2 by A17, GROUP_1:def_3 .= (a1 * a) * (b * b2) by GROUP_1:def_3 ; a1 * a in carr H1 by A12, A18, Th74; hence g1 * g2 in (carr H1) * (carr H2) by A21, A20; ::_thesis: verum end; (carr H1) * (carr H2) <> {} by Th9; hence ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) by A8, A2, Th52; ::_thesis: verum end; given H being Subgroup of G such that A22: the carrier of H = (carr H1) * (carr H2) ; ::_thesis: (carr H1) * (carr H2) = (carr H2) * (carr H1) thus (carr H1) * (carr H2) c= (carr H2) * (carr H1) :: according to XBOOLE_0:def_10 ::_thesis: (carr H2) * (carr H1) c= (carr H1) * (carr H2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (carr H1) * (carr H2) or x in (carr H2) * (carr H1) ) assume A23: x in (carr H1) * (carr H2) ; ::_thesis: x in (carr H2) * (carr H1) then reconsider y = x as Element of G ; y " in carr H by A22, A23, Th75; then consider a, b being Element of G such that A24: y " = a * b and A25: ( a in carr H1 & b in carr H2 ) by A22; A26: y = (y ") " .= (b ") * (a ") by A24, GROUP_1:17 ; ( a " in carr H1 & b " in carr H2 ) by A25, Th75; hence x in (carr H2) * (carr H1) by A26; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (carr H2) * (carr H1) or x in (carr H1) * (carr H2) ) assume A27: x in (carr H2) * (carr H1) ; ::_thesis: x in (carr H1) * (carr H2) then reconsider y = x as Element of G ; consider a, b being Element of G such that A28: ( x = a * b & a in carr H2 ) and A29: b in carr H1 by A27; now__::_thesis:_y_"_in_carr_H A30: b " in carr H1 by A29, Th75; assume A31: not y " in carr H ; ::_thesis: contradiction ( y " = (b ") * (a ") & a " in carr H2 ) by A28, Th75, GROUP_1:17; hence contradiction by A22, A31, A30; ::_thesis: verum end; then (y ") " in carr H by Th75; hence x in (carr H1) * (carr H2) by A22; ::_thesis: verum end; theorem :: GROUP_2:79 for G being Group for H1, H2 being Subgroup of G st G is commutative Group holds ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G st G is commutative Group holds ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) let H1, H2 be Subgroup of G; ::_thesis: ( G is commutative Group implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) assume G is commutative Group ; ::_thesis: ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) then (carr H1) * (carr H2) = (carr H2) * (carr H1) by Th25; hence ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) by Th78; ::_thesis: verum end; definition let G be Group; let H1, H2 be Subgroup of G; funcH1 /\ H2 -> strict Subgroup of G means :Def10: :: GROUP_2:def 10 the carrier of it = (carr H1) /\ (carr H2); existence ex b1 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) proof set A = (carr H1) /\ (carr H2); 1_ G in H2 by Th46; then A1: 1_ G in the carrier of H2 by STRUCT_0:def_5; A2: now__::_thesis:_for_g1,_g2_being_Element_of_G_st_g1_in_(carr_H1)_/\_(carr_H2)_&_g2_in_(carr_H1)_/\_(carr_H2)_holds_ g1_*_g2_in_(carr_H1)_/\_(carr_H2) let g1, g2 be Element of G; ::_thesis: ( g1 in (carr H1) /\ (carr H2) & g2 in (carr H1) /\ (carr H2) implies g1 * g2 in (carr H1) /\ (carr H2) ) assume A3: ( g1 in (carr H1) /\ (carr H2) & g2 in (carr H1) /\ (carr H2) ) ; ::_thesis: g1 * g2 in (carr H1) /\ (carr H2) then ( g1 in carr H2 & g2 in carr H2 ) by XBOOLE_0:def_4; then A4: g1 * g2 in carr H2 by Th74; ( g1 in carr H1 & g2 in carr H1 ) by A3, XBOOLE_0:def_4; then g1 * g2 in carr H1 by Th74; hence g1 * g2 in (carr H1) /\ (carr H2) by A4, XBOOLE_0:def_4; ::_thesis: verum end; A5: now__::_thesis:_for_g_being_Element_of_G_st_g_in_(carr_H1)_/\_(carr_H2)_holds_ g_"_in_(carr_H1)_/\_(carr_H2) let g be Element of G; ::_thesis: ( g in (carr H1) /\ (carr H2) implies g " in (carr H1) /\ (carr H2) ) assume A6: g in (carr H1) /\ (carr H2) ; ::_thesis: g " in (carr H1) /\ (carr H2) then g in carr H2 by XBOOLE_0:def_4; then A7: g " in carr H2 by Th75; g in carr H1 by A6, XBOOLE_0:def_4; then g " in carr H1 by Th75; hence g " in (carr H1) /\ (carr H2) by A7, XBOOLE_0:def_4; ::_thesis: verum end; 1_ G in H1 by Th46; then 1_ G in the carrier of H1 by STRUCT_0:def_5; then (carr H1) /\ (carr H2) <> {} by A1, XBOOLE_0:def_4; hence ex b1 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) by A2, A5, Th52; ::_thesis: verum end; uniqueness for b1, b2 being strict Subgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) & the carrier of b2 = (carr H1) /\ (carr H2) holds b1 = b2 by Th59; end; :: deftheorem Def10 defines /\ GROUP_2:def_10_:_ for G being Group for H1, H2 being Subgroup of G for b4 being strict Subgroup of G holds ( b4 = H1 /\ H2 iff the carrier of b4 = (carr H1) /\ (carr H2) ); theorem Th80: :: GROUP_2:80 for G being Group for H1, H2 being Subgroup of G holds ( ( for H being Subgroup of G st H = H1 /\ H2 holds the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds H = H1 /\ H2 ) ) proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds ( ( for H being Subgroup of G st H = H1 /\ H2 holds the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds H = H1 /\ H2 ) ) let H1, H2 be Subgroup of G; ::_thesis: ( ( for H being Subgroup of G st H = H1 /\ H2 holds the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds H = H1 /\ H2 ) ) A1: ( the carrier of H1 = carr H1 & the carrier of H2 = carr H2 ) ; thus for H being Subgroup of G st H = H1 /\ H2 holds the carrier of H = the carrier of H1 /\ the carrier of H2 ::_thesis: for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds H = H1 /\ H2 proof let H be Subgroup of G; ::_thesis: ( H = H1 /\ H2 implies the carrier of H = the carrier of H1 /\ the carrier of H2 ) assume H = H1 /\ H2 ; ::_thesis: the carrier of H = the carrier of H1 /\ the carrier of H2 hence the carrier of H = (carr H1) /\ (carr H2) by Def10 .= the carrier of H1 /\ the carrier of H2 ; ::_thesis: verum end; let H be strict Subgroup of G; ::_thesis: ( the carrier of H = the carrier of H1 /\ the carrier of H2 implies H = H1 /\ H2 ) assume the carrier of H = the carrier of H1 /\ the carrier of H2 ; ::_thesis: H = H1 /\ H2 hence H = H1 /\ H2 by A1, Def10; ::_thesis: verum end; theorem :: GROUP_2:81 for G being Group for H1, H2 being Subgroup of G holds carr (H1 /\ H2) = (carr H1) /\ (carr H2) by Def10; theorem Th82: :: GROUP_2:82 for x being set for G being Group for H1, H2 being Subgroup of G holds ( x in H1 /\ H2 iff ( x in H1 & x in H2 ) ) proof let x be set ; ::_thesis: for G being Group for H1, H2 being Subgroup of G holds ( x in H1 /\ H2 iff ( x in H1 & x in H2 ) ) let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds ( x in H1 /\ H2 iff ( x in H1 & x in H2 ) ) let H1, H2 be Subgroup of G; ::_thesis: ( x in H1 /\ H2 iff ( x in H1 & x in H2 ) ) thus ( x in H1 /\ H2 implies ( x in H1 & x in H2 ) ) ::_thesis: ( x in H1 & x in H2 implies x in H1 /\ H2 ) proof assume x in H1 /\ H2 ; ::_thesis: ( x in H1 & x in H2 ) then x in the carrier of (H1 /\ H2) by STRUCT_0:def_5; then x in (carr H1) /\ (carr H2) by Def10; then ( x in carr H1 & x in carr H2 ) by XBOOLE_0:def_4; hence ( x in H1 & x in H2 ) by STRUCT_0:def_5; ::_thesis: verum end; assume ( x in H1 & x in H2 ) ; ::_thesis: x in H1 /\ H2 then ( x in carr H2 & x in carr H1 ) by STRUCT_0:def_5; then x in (carr H1) /\ (carr H2) by XBOOLE_0:def_4; then x in carr (H1 /\ H2) by Def10; hence x in H1 /\ H2 by STRUCT_0:def_5; ::_thesis: verum end; theorem :: GROUP_2:83 for G being Group for H being strict Subgroup of G holds H /\ H = H proof let G be Group; ::_thesis: for H being strict Subgroup of G holds H /\ H = H let H be strict Subgroup of G; ::_thesis: H /\ H = H the carrier of (H /\ H) = (carr H) /\ (carr H) by Def10 .= the carrier of H ; hence H /\ H = H by Th59; ::_thesis: verum end; definition let G be Group; let H1, H2 be Subgroup of G; :: original: /\ redefine funcH1 /\ H2 -> strict Subgroup of G; commutativity for H1, H2 being Subgroup of G holds H1 /\ H2 = H2 /\ H1 proof let H1, H2 be Subgroup of G; ::_thesis: H1 /\ H2 = H2 /\ H1 the carrier of (H1 /\ H2) = (carr H2) /\ (carr H1) by Def10 .= the carrier of (H2 /\ H1) by Def10 ; hence H1 /\ H2 = H2 /\ H1 by Th59; ::_thesis: verum end; end; theorem :: GROUP_2:84 for G being Group for H1, H2, H3 being Subgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3) proof let G be Group; ::_thesis: for H1, H2, H3 being Subgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3) let H1, H2, H3 be Subgroup of G; ::_thesis: (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3) the carrier of ((H1 /\ H2) /\ H3) = (carr (H1 /\ H2)) /\ (carr H3) by Def10 .= ((carr H1) /\ (carr H2)) /\ (carr H3) by Def10 .= (carr H1) /\ ((carr H2) /\ (carr H3)) by XBOOLE_1:16 .= (carr H1) /\ (carr (H2 /\ H3)) by Def10 .= the carrier of (H1 /\ (H2 /\ H3)) by Def10 ; hence (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3) by Th59; ::_thesis: verum end; Lm3: for G being Group for H2, H1 being Subgroup of G holds ( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ) proof let G be Group; ::_thesis: for H2, H1 being Subgroup of G holds ( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ) let H2, H1 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ) thus ( H1 is Subgroup of H2 implies multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ) ::_thesis: ( multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) implies H1 is Subgroup of H2 ) proof assume H1 is Subgroup of H2 ; ::_thesis: multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) then A1: the carrier of H1 c= the carrier of H2 by Def5; the carrier of (H1 /\ H2) = (carr H1) /\ (carr H2) by Def10; hence multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) by A1, Th59, XBOOLE_1:28; ::_thesis: verum end; assume multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ; ::_thesis: H1 is Subgroup of H2 then the carrier of H1 = (carr H1) /\ (carr H2) by Def10 .= the carrier of H1 /\ the carrier of H2 ; hence H1 is Subgroup of H2 by Th57, XBOOLE_1:17; ::_thesis: verum end; theorem :: GROUP_2:85 for G being Group for H being Subgroup of G holds ( ((1). G) /\ H = (1). G & H /\ ((1). G) = (1). G ) proof let G be Group; ::_thesis: for H being Subgroup of G holds ( ((1). G) /\ H = (1). G & H /\ ((1). G) = (1). G ) let H be Subgroup of G; ::_thesis: ( ((1). G) /\ H = (1). G & H /\ ((1). G) = (1). G ) A1: (1). G is Subgroup of H by Th65; hence ((1). G) /\ H = (1). G by Lm3; ::_thesis: H /\ ((1). G) = (1). G thus H /\ ((1). G) = (1). G by A1, Lm3; ::_thesis: verum end; theorem :: GROUP_2:86 for G being strict Group for H being strict Subgroup of G holds ( H /\ ((Omega). G) = H & ((Omega). G) /\ H = H ) by Lm3; theorem :: GROUP_2:87 for G being strict Group holds ((Omega). G) /\ ((Omega). G) = G by Lm3; Lm4: for G being Group for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1 proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1 let H1, H2 be Subgroup of G; ::_thesis: H1 /\ H2 is Subgroup of H1 the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2 by Th80; hence H1 /\ H2 is Subgroup of H1 by Th57, XBOOLE_1:17; ::_thesis: verum end; theorem :: GROUP_2:88 for G being Group for H1, H2 being Subgroup of G holds ( H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 ) by Lm4; theorem :: GROUP_2:89 for G being Group for H2, H1 being Subgroup of G holds ( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ) by Lm3; theorem :: GROUP_2:90 for G being Group for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds H1 /\ H3 is Subgroup of H2 proof let G be Group; ::_thesis: for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds H1 /\ H3 is Subgroup of H2 let H1, H2, H3 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 ) assume A1: H1 is Subgroup of H2 ; ::_thesis: H1 /\ H3 is Subgroup of H2 H1 /\ H3 is Subgroup of H1 by Lm4; hence H1 /\ H3 is Subgroup of H2 by A1, Th56; ::_thesis: verum end; theorem :: GROUP_2:91 for G being Group for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 & H1 is Subgroup of H3 holds H1 is Subgroup of H2 /\ H3 proof let G be Group; ::_thesis: for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 & H1 is Subgroup of H3 holds H1 is Subgroup of H2 /\ H3 let H1, H2, H3 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 & H1 is Subgroup of H3 implies H1 is Subgroup of H2 /\ H3 ) assume A1: ( H1 is Subgroup of H2 & H1 is Subgroup of H3 ) ; ::_thesis: H1 is Subgroup of H2 /\ H3 now__::_thesis:_for_g_being_Element_of_G_st_g_in_H1_holds_ g_in_H2_/\_H3 let g be Element of G; ::_thesis: ( g in H1 implies g in H2 /\ H3 ) assume g in H1 ; ::_thesis: g in H2 /\ H3 then ( g in H2 & g in H3 ) by A1, Th40; hence g in H2 /\ H3 by Th82; ::_thesis: verum end; hence H1 is Subgroup of H2 /\ H3 by Th58; ::_thesis: verum end; theorem :: GROUP_2:92 for G being Group for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds H1 /\ H3 is Subgroup of H2 /\ H3 proof let G be Group; ::_thesis: for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds H1 /\ H3 is Subgroup of H2 /\ H3 let H1, H2, H3 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3 ) assume H1 is Subgroup of H2 ; ::_thesis: H1 /\ H3 is Subgroup of H2 /\ H3 then the carrier of H1 c= the carrier of H2 by Def5; then the carrier of H1 /\ the carrier of H3 c= the carrier of H2 /\ the carrier of H3 by XBOOLE_1:26; then the carrier of (H1 /\ H3) c= the carrier of H2 /\ the carrier of H3 by Th80; then the carrier of (H1 /\ H3) c= the carrier of (H2 /\ H3) by Th80; hence H1 /\ H3 is Subgroup of H2 /\ H3 by Th57; ::_thesis: verum end; theorem :: GROUP_2:93 for G being Group for H1, H2 being Subgroup of G st ( H1 is finite or H2 is finite ) holds H1 /\ H2 is finite proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G st ( H1 is finite or H2 is finite ) holds H1 /\ H2 is finite let H1, H2 be Subgroup of G; ::_thesis: ( ( H1 is finite or H2 is finite ) implies H1 /\ H2 is finite ) assume A1: ( H1 is finite or H2 is finite ) ; ::_thesis: H1 /\ H2 is finite ( H1 /\ H2 is Subgroup of H1 & H1 /\ H2 is Subgroup of H2 ) by Lm4; hence H1 /\ H2 is finite by A1; ::_thesis: verum end; definition let G be Group; let H be Subgroup of G; let A be Subset of G; funcA * H -> Subset of G equals :: GROUP_2:def 11 A * (carr H); correctness coherence A * (carr H) is Subset of G; ; funcH * A -> Subset of G equals :: GROUP_2:def 12 (carr H) * A; correctness coherence (carr H) * A is Subset of G; ; end; :: deftheorem defines * GROUP_2:def_11_:_ for G being Group for H being Subgroup of G for A being Subset of G holds A * H = A * (carr H); :: deftheorem defines * GROUP_2:def_12_:_ for G being Group for H being Subgroup of G for A being Subset of G holds H * A = (carr H) * A; theorem :: GROUP_2:94 for x being set for G being Group for A being Subset of G for H being Subgroup of G holds ( x in A * H iff ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in A & g2 in H ) ) proof let x be set ; ::_thesis: for G being Group for A being Subset of G for H being Subgroup of G holds ( x in A * H iff ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in A & g2 in H ) ) let G be Group; ::_thesis: for A being Subset of G for H being Subgroup of G holds ( x in A * H iff ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in A & g2 in H ) ) let A be Subset of G; ::_thesis: for H being Subgroup of G holds ( x in A * H iff ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in A & g2 in H ) ) let H be Subgroup of G; ::_thesis: ( x in A * H iff ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in A & g2 in H ) ) thus ( x in A * H implies ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in A & g2 in H ) ) ::_thesis: ( ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in A & g2 in H ) implies x in A * H ) proof assume x in A * H ; ::_thesis: ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in A & g2 in H ) then consider g1, g2 being Element of G such that A1: ( x = g1 * g2 & g1 in A ) and A2: g2 in carr H ; g2 in H by A2, STRUCT_0:def_5; hence ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in A & g2 in H ) by A1; ::_thesis: verum end; given g1, g2 being Element of G such that A3: ( x = g1 * g2 & g1 in A ) and A4: g2 in H ; ::_thesis: x in A * H g2 in carr H by A4, STRUCT_0:def_5; hence x in A * H by A3; ::_thesis: verum end; theorem :: GROUP_2:95 for x being set for G being Group for A being Subset of G for H being Subgroup of G holds ( x in H * A iff ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in H & g2 in A ) ) proof let x be set ; ::_thesis: for G being Group for A being Subset of G for H being Subgroup of G holds ( x in H * A iff ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in H & g2 in A ) ) let G be Group; ::_thesis: for A being Subset of G for H being Subgroup of G holds ( x in H * A iff ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in H & g2 in A ) ) let A be Subset of G; ::_thesis: for H being Subgroup of G holds ( x in H * A iff ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in H & g2 in A ) ) let H be Subgroup of G; ::_thesis: ( x in H * A iff ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in H & g2 in A ) ) thus ( x in H * A implies ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in H & g2 in A ) ) ::_thesis: ( ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in H & g2 in A ) implies x in H * A ) proof assume x in H * A ; ::_thesis: ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in H & g2 in A ) then consider g1, g2 being Element of G such that A1: x = g1 * g2 and A2: g1 in carr H and A3: g2 in A ; g1 in H by A2, STRUCT_0:def_5; hence ex g1, g2 being Element of G st ( x = g1 * g2 & g1 in H & g2 in A ) by A1, A3; ::_thesis: verum end; given g1, g2 being Element of G such that A4: x = g1 * g2 and A5: g1 in H and A6: g2 in A ; ::_thesis: x in H * A g1 in carr H by A5, STRUCT_0:def_5; hence x in H * A by A4, A6; ::_thesis: verum end; theorem :: GROUP_2:96 for G being Group for A, B being Subset of G for H being Subgroup of G holds (A * B) * H = A * (B * H) by Th10; theorem :: GROUP_2:97 for G being Group for A, B being Subset of G for H being Subgroup of G holds (A * H) * B = A * (H * B) by Th10; theorem :: GROUP_2:98 for G being Group for A, B being Subset of G for H being Subgroup of G holds (H * A) * B = H * (A * B) by Th10; theorem :: GROUP_2:99 for G being Group for A being Subset of G for H1, H2 being Subgroup of G holds (A * H1) * H2 = A * (H1 * (carr H2)) by Th10; theorem :: GROUP_2:100 for G being Group for A being Subset of G for H1, H2 being Subgroup of G holds (H1 * A) * H2 = H1 * (A * H2) by Th10; theorem :: GROUP_2:101 for G being Group for A being Subset of G for H1, H2 being Subgroup of G holds (H1 * (carr H2)) * A = H1 * (H2 * A) by Th10; theorem :: GROUP_2:102 for G being Group for A being Subset of G for H being Subgroup of G st G is commutative Group holds A * H = H * A by Th25; definition let G be Group; let H be Subgroup of G; let a be Element of G; funca * H -> Subset of G equals :: GROUP_2:def 13 a * (carr H); correctness coherence a * (carr H) is Subset of G; ; funcH * a -> Subset of G equals :: GROUP_2:def 14 (carr H) * a; correctness coherence (carr H) * a is Subset of G; ; end; :: deftheorem defines * GROUP_2:def_13_:_ for G being Group for H being Subgroup of G for a being Element of G holds a * H = a * (carr H); :: deftheorem defines * GROUP_2:def_14_:_ for G being Group for H being Subgroup of G for a being Element of G holds H * a = (carr H) * a; theorem Th103: :: GROUP_2:103 for x being set for G being Group for a being Element of G for H being Subgroup of G holds ( x in a * H iff ex g being Element of G st ( x = a * g & g in H ) ) proof let x be set ; ::_thesis: for G being Group for a being Element of G for H being Subgroup of G holds ( x in a * H iff ex g being Element of G st ( x = a * g & g in H ) ) let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( x in a * H iff ex g being Element of G st ( x = a * g & g in H ) ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( x in a * H iff ex g being Element of G st ( x = a * g & g in H ) ) let H be Subgroup of G; ::_thesis: ( x in a * H iff ex g being Element of G st ( x = a * g & g in H ) ) thus ( x in a * H implies ex g being Element of G st ( x = a * g & g in H ) ) ::_thesis: ( ex g being Element of G st ( x = a * g & g in H ) implies x in a * H ) proof assume x in a * H ; ::_thesis: ex g being Element of G st ( x = a * g & g in H ) then consider g being Element of G such that A1: ( x = a * g & g in carr H ) by Th27; take g ; ::_thesis: ( x = a * g & g in H ) thus ( x = a * g & g in H ) by A1, STRUCT_0:def_5; ::_thesis: verum end; given g being Element of G such that A2: x = a * g and A3: g in H ; ::_thesis: x in a * H g in carr H by A3, STRUCT_0:def_5; hence x in a * H by A2, Th27; ::_thesis: verum end; theorem Th104: :: GROUP_2:104 for x being set for G being Group for a being Element of G for H being Subgroup of G holds ( x in H * a iff ex g being Element of G st ( x = g * a & g in H ) ) proof let x be set ; ::_thesis: for G being Group for a being Element of G for H being Subgroup of G holds ( x in H * a iff ex g being Element of G st ( x = g * a & g in H ) ) let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( x in H * a iff ex g being Element of G st ( x = g * a & g in H ) ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( x in H * a iff ex g being Element of G st ( x = g * a & g in H ) ) let H be Subgroup of G; ::_thesis: ( x in H * a iff ex g being Element of G st ( x = g * a & g in H ) ) thus ( x in H * a implies ex g being Element of G st ( x = g * a & g in H ) ) ::_thesis: ( ex g being Element of G st ( x = g * a & g in H ) implies x in H * a ) proof assume x in H * a ; ::_thesis: ex g being Element of G st ( x = g * a & g in H ) then consider g being Element of G such that A1: ( x = g * a & g in carr H ) by Th28; take g ; ::_thesis: ( x = g * a & g in H ) thus ( x = g * a & g in H ) by A1, STRUCT_0:def_5; ::_thesis: verum end; given g being Element of G such that A2: x = g * a and A3: g in H ; ::_thesis: x in H * a g in carr H by A3, STRUCT_0:def_5; hence x in H * a by A2, Th28; ::_thesis: verum end; theorem :: GROUP_2:105 for G being Group for a, b being Element of G for H being Subgroup of G holds (a * b) * H = a * (b * H) by Th32; theorem :: GROUP_2:106 for G being Group for a, b being Element of G for H being Subgroup of G holds (a * H) * b = a * (H * b) by Th10; theorem :: GROUP_2:107 for G being Group for a, b being Element of G for H being Subgroup of G holds (H * a) * b = H * (a * b) by Th34; theorem Th108: :: GROUP_2:108 for G being Group for a being Element of G for H being Subgroup of G holds ( a in a * H & a in H * a ) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( a in a * H & a in H * a ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( a in a * H & a in H * a ) let H be Subgroup of G; ::_thesis: ( a in a * H & a in H * a ) A1: (1_ G) * a = a by GROUP_1:def_4; ( 1_ G in H & a * (1_ G) = a ) by Th46, GROUP_1:def_4; hence ( a in a * H & a in H * a ) by A1, Th103, Th104; ::_thesis: verum end; theorem :: GROUP_2:109 for G being Group for H being Subgroup of G holds ( (1_ G) * H = carr H & H * (1_ G) = carr H ) by Th37; theorem Th110: :: GROUP_2:110 for G being Group for a being Element of G holds ( ((1). G) * a = {a} & a * ((1). G) = {a} ) proof let G be Group; ::_thesis: for a being Element of G holds ( ((1). G) * a = {a} & a * ((1). G) = {a} ) let a be Element of G; ::_thesis: ( ((1). G) * a = {a} & a * ((1). G) = {a} ) A1: the carrier of ((1). G) = {(1_ G)} by Def7; hence ((1). G) * a = {((1_ G) * a)} by Th18 .= {a} by GROUP_1:def_4 ; ::_thesis: a * ((1). G) = {a} thus a * ((1). G) = {(a * (1_ G))} by A1, Th18 .= {a} by GROUP_1:def_4 ; ::_thesis: verum end; theorem Th111: :: GROUP_2:111 for G being Group for a being Element of G holds ( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G ) proof let G be Group; ::_thesis: for a being Element of G holds ( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G ) let a be Element of G; ::_thesis: ( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G ) ([#] the carrier of G) * a = the carrier of G by Th17; hence ( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G ) by Th17; ::_thesis: verum end; theorem :: GROUP_2:112 for G being Group for a being Element of G for H being Subgroup of G st G is commutative Group holds a * H = H * a by Th25; theorem Th113: :: GROUP_2:113 for G being Group for a being Element of G for H being Subgroup of G holds ( a in H iff a * H = carr H ) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( a in H iff a * H = carr H ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( a in H iff a * H = carr H ) let H be Subgroup of G; ::_thesis: ( a in H iff a * H = carr H ) thus ( a in H implies a * H = carr H ) ::_thesis: ( a * H = carr H implies a in H ) proof assume A1: a in H ; ::_thesis: a * H = carr H thus a * H c= carr H :: according to XBOOLE_0:def_10 ::_thesis: carr H c= a * H proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a * H or x in carr H ) assume x in a * H ; ::_thesis: x in carr H then consider g being Element of G such that A2: x = a * g and A3: g in H by Th103; a * g in H by A1, A3, Th50; hence x in carr H by A2, STRUCT_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in carr H or x in a * H ) assume A4: x in carr H ; ::_thesis: x in a * H then A5: x in H by STRUCT_0:def_5; reconsider b = x as Element of G by A4; A6: a * ((a ") * b) = (a * (a ")) * b by GROUP_1:def_3 .= (1_ G) * b by GROUP_1:def_5 .= x by GROUP_1:def_4 ; a " in H by A1, Th51; then (a ") * b in H by A5, Th50; hence x in a * H by A6, Th103; ::_thesis: verum end; assume A7: a * H = carr H ; ::_thesis: a in H ( a * (1_ G) = a & 1_ G in H ) by Th46, GROUP_1:def_4; then a in carr H by A7, Th103; hence a in H by STRUCT_0:def_5; ::_thesis: verum end; theorem Th114: :: GROUP_2:114 for G being Group for a, b being Element of G for H being Subgroup of G holds ( a * H = b * H iff (b ") * a in H ) proof let G be Group; ::_thesis: for a, b being Element of G for H being Subgroup of G holds ( a * H = b * H iff (b ") * a in H ) let a, b be Element of G; ::_thesis: for H being Subgroup of G holds ( a * H = b * H iff (b ") * a in H ) let H be Subgroup of G; ::_thesis: ( a * H = b * H iff (b ") * a in H ) thus ( a * H = b * H implies (b ") * a in H ) ::_thesis: ( (b ") * a in H implies a * H = b * H ) proof assume A1: a * H = b * H ; ::_thesis: (b ") * a in H ((b ") * a) * H = (b ") * (a * H) by Th32 .= ((b ") * b) * H by A1, Th32 .= (1_ G) * H by GROUP_1:def_5 .= carr H by Th37 ; hence (b ") * a in H by Th113; ::_thesis: verum end; assume A2: (b ") * a in H ; ::_thesis: a * H = b * H thus a * H = (1_ G) * (a * H) by Th37 .= ((1_ G) * a) * H by Th32 .= ((b * (b ")) * a) * H by GROUP_1:def_5 .= (b * ((b ") * a)) * H by GROUP_1:def_3 .= b * (((b ") * a) * H) by Th32 .= b * H by A2, Th113 ; ::_thesis: verum end; theorem Th115: :: GROUP_2:115 for G being Group for a, b being Element of G for H being Subgroup of G holds ( a * H = b * H iff a * H meets b * H ) proof let G be Group; ::_thesis: for a, b being Element of G for H being Subgroup of G holds ( a * H = b * H iff a * H meets b * H ) let a, b be Element of G; ::_thesis: for H being Subgroup of G holds ( a * H = b * H iff a * H meets b * H ) let H be Subgroup of G; ::_thesis: ( a * H = b * H iff a * H meets b * H ) a * H <> {} by Th108; hence ( a * H = b * H implies a * H meets b * H ) by XBOOLE_1:66; ::_thesis: ( a * H meets b * H implies a * H = b * H ) assume a * H meets b * H ; ::_thesis: a * H = b * H then consider x being set such that A1: x in a * H and A2: x in b * H by XBOOLE_0:3; reconsider x = x as Element of G by A2; consider g being Element of G such that A3: x = a * g and A4: g in H by A1, Th103; A5: g " in H by A4, Th51; consider h being Element of G such that A6: x = b * h and A7: h in H by A2, Th103; a = (b * h) * (g ") by A3, A6, GROUP_1:14 .= b * (h * (g ")) by GROUP_1:def_3 ; then (b ") * a = h * (g ") by GROUP_1:13; then (b ") * a in H by A7, A5, Th50; hence a * H = b * H by Th114; ::_thesis: verum end; theorem Th116: :: GROUP_2:116 for G being Group for a, b being Element of G for H being Subgroup of G holds (a * b) * H c= (a * H) * (b * H) proof let G be Group; ::_thesis: for a, b being Element of G for H being Subgroup of G holds (a * b) * H c= (a * H) * (b * H) let a, b be Element of G; ::_thesis: for H being Subgroup of G holds (a * b) * H c= (a * H) * (b * H) let H be Subgroup of G; ::_thesis: (a * b) * H c= (a * H) * (b * H) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (a * b) * H or x in (a * H) * (b * H) ) assume x in (a * b) * H ; ::_thesis: x in (a * H) * (b * H) then consider g being Element of G such that A1: x = (a * b) * g and A2: g in H by Th103; A3: x = ((a * (1_ G)) * b) * g by A1, GROUP_1:def_4 .= (a * (1_ G)) * (b * g) by GROUP_1:def_3 ; 1_ G in H by Th46; then A4: a * (1_ G) in a * H by Th103; b * g in b * H by A2, Th103; hence x in (a * H) * (b * H) by A3, A4; ::_thesis: verum end; theorem :: GROUP_2:117 for G being Group for a being Element of G for H being Subgroup of G holds ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) ) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) ) let H be Subgroup of G; ::_thesis: ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) ) A1: ((a ") * a) * H = (1_ G) * H by GROUP_1:def_5 .= carr H by Th37 ; (a * (a ")) * H = (1_ G) * H by GROUP_1:def_5 .= carr H by Th37 ; hence ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) ) by A1, Th116; ::_thesis: verum end; theorem :: GROUP_2:118 for G being Group for a being Element of G for H being Subgroup of G holds (a |^ 2) * H c= (a * H) * (a * H) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds (a |^ 2) * H c= (a * H) * (a * H) let a be Element of G; ::_thesis: for H being Subgroup of G holds (a |^ 2) * H c= (a * H) * (a * H) let H be Subgroup of G; ::_thesis: (a |^ 2) * H c= (a * H) * (a * H) (a |^ 2) * H = (a * a) * H by GROUP_1:27; hence (a |^ 2) * H c= (a * H) * (a * H) by Th116; ::_thesis: verum end; theorem Th119: :: GROUP_2:119 for G being Group for a being Element of G for H being Subgroup of G holds ( a in H iff H * a = carr H ) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( a in H iff H * a = carr H ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( a in H iff H * a = carr H ) let H be Subgroup of G; ::_thesis: ( a in H iff H * a = carr H ) thus ( a in H implies H * a = carr H ) ::_thesis: ( H * a = carr H implies a in H ) proof assume A1: a in H ; ::_thesis: H * a = carr H thus H * a c= carr H :: according to XBOOLE_0:def_10 ::_thesis: carr H c= H * a proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H * a or x in carr H ) assume x in H * a ; ::_thesis: x in carr H then consider g being Element of G such that A2: x = g * a and A3: g in H by Th104; g * a in H by A1, A3, Th50; hence x in carr H by A2, STRUCT_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in carr H or x in H * a ) assume A4: x in carr H ; ::_thesis: x in H * a then A5: x in H by STRUCT_0:def_5; reconsider b = x as Element of G by A4; A6: (b * (a ")) * a = b * ((a ") * a) by GROUP_1:def_3 .= b * (1_ G) by GROUP_1:def_5 .= x by GROUP_1:def_4 ; a " in H by A1, Th51; then b * (a ") in H by A5, Th50; hence x in H * a by A6, Th104; ::_thesis: verum end; assume A7: H * a = carr H ; ::_thesis: a in H ( (1_ G) * a = a & 1_ G in H ) by Th46, GROUP_1:def_4; then a in carr H by A7, Th104; hence a in H by STRUCT_0:def_5; ::_thesis: verum end; theorem Th120: :: GROUP_2:120 for G being Group for a, b being Element of G for H being Subgroup of G holds ( H * a = H * b iff b * (a ") in H ) proof let G be Group; ::_thesis: for a, b being Element of G for H being Subgroup of G holds ( H * a = H * b iff b * (a ") in H ) let a, b be Element of G; ::_thesis: for H being Subgroup of G holds ( H * a = H * b iff b * (a ") in H ) let H be Subgroup of G; ::_thesis: ( H * a = H * b iff b * (a ") in H ) thus ( H * a = H * b implies b * (a ") in H ) ::_thesis: ( b * (a ") in H implies H * a = H * b ) proof assume A1: H * a = H * b ; ::_thesis: b * (a ") in H carr H = H * (1_ G) by Th37 .= H * (a * (a ")) by GROUP_1:def_5 .= (H * b) * (a ") by A1, Th34 .= H * (b * (a ")) by Th34 ; hence b * (a ") in H by Th119; ::_thesis: verum end; assume b * (a ") in H ; ::_thesis: H * a = H * b hence H * a = (H * (b * (a "))) * a by Th119 .= H * ((b * (a ")) * a) by Th34 .= H * (b * ((a ") * a)) by GROUP_1:def_3 .= H * (b * (1_ G)) by GROUP_1:def_5 .= H * b by GROUP_1:def_4 ; ::_thesis: verum end; theorem :: GROUP_2:121 for G being Group for a, b being Element of G for H being Subgroup of G holds ( H * a = H * b iff H * a meets H * b ) proof let G be Group; ::_thesis: for a, b being Element of G for H being Subgroup of G holds ( H * a = H * b iff H * a meets H * b ) let a, b be Element of G; ::_thesis: for H being Subgroup of G holds ( H * a = H * b iff H * a meets H * b ) let H be Subgroup of G; ::_thesis: ( H * a = H * b iff H * a meets H * b ) H * a <> {} by Th108; hence ( H * a = H * b implies H * a meets H * b ) by XBOOLE_1:66; ::_thesis: ( H * a meets H * b implies H * a = H * b ) assume H * a meets H * b ; ::_thesis: H * a = H * b then consider x being set such that A1: x in H * a and A2: x in H * b by XBOOLE_0:3; reconsider x = x as Element of G by A2; consider g being Element of G such that A3: x = g * a and A4: g in H by A1, Th104; A5: g " in H by A4, Th51; consider h being Element of G such that A6: x = h * b and A7: h in H by A2, Th104; a = (g ") * (h * b) by A3, A6, GROUP_1:13 .= ((g ") * h) * b by GROUP_1:def_3 ; then a * (b ") = (g ") * h by GROUP_1:14; then a * (b ") in H by A7, A5, Th50; hence H * a = H * b by Th120; ::_thesis: verum end; theorem Th122: :: GROUP_2:122 for G being Group for a, b being Element of G for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b) proof let G be Group; ::_thesis: for a, b being Element of G for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b) let a, b be Element of G; ::_thesis: for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b) let H be Subgroup of G; ::_thesis: (H * a) * b c= (H * a) * (H * b) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (H * a) * b or x in (H * a) * (H * b) ) 1_ G in H by Th46; then A1: (1_ G) * b in H * b by Th104; assume x in (H * a) * b ; ::_thesis: x in (H * a) * (H * b) then x in H * (a * b) by Th34; then consider g being Element of G such that A2: x = g * (a * b) and A3: g in H by Th104; A4: x = (g * a) * b by A2, GROUP_1:def_3 .= (g * a) * ((1_ G) * b) by GROUP_1:def_4 ; g * a in H * a by A3, Th104; hence x in (H * a) * (H * b) by A1, A4; ::_thesis: verum end; theorem :: GROUP_2:123 for G being Group for a being Element of G for H being Subgroup of G holds ( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) ) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) ) let H be Subgroup of G; ::_thesis: ( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) ) A1: (H * (a ")) * a = H * ((a ") * a) by Th34 .= H * (1_ G) by GROUP_1:def_5 .= carr H by Th37 ; (H * a) * (a ") = H * (a * (a ")) by Th34 .= H * (1_ G) by GROUP_1:def_5 .= carr H by Th37 ; hence ( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) ) by A1, Th122; ::_thesis: verum end; theorem :: GROUP_2:124 for G being Group for a being Element of G for H being Subgroup of G holds H * (a |^ 2) c= (H * a) * (H * a) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds H * (a |^ 2) c= (H * a) * (H * a) let a be Element of G; ::_thesis: for H being Subgroup of G holds H * (a |^ 2) c= (H * a) * (H * a) let H be Subgroup of G; ::_thesis: H * (a |^ 2) c= (H * a) * (H * a) ( a |^ 2 = a * a & (H * a) * a = H * (a * a) ) by Th34, GROUP_1:27; hence H * (a |^ 2) c= (H * a) * (H * a) by Th122; ::_thesis: verum end; theorem :: GROUP_2:125 for G being Group for a being Element of G for H1, H2 being Subgroup of G holds a * (H1 /\ H2) = (a * H1) /\ (a * H2) proof let G be Group; ::_thesis: for a being Element of G for H1, H2 being Subgroup of G holds a * (H1 /\ H2) = (a * H1) /\ (a * H2) let a be Element of G; ::_thesis: for H1, H2 being Subgroup of G holds a * (H1 /\ H2) = (a * H1) /\ (a * H2) let H1, H2 be Subgroup of G; ::_thesis: a * (H1 /\ H2) = (a * H1) /\ (a * H2) thus a * (H1 /\ H2) c= (a * H1) /\ (a * H2) :: according to XBOOLE_0:def_10 ::_thesis: (a * H1) /\ (a * H2) c= a * (H1 /\ H2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a * (H1 /\ H2) or x in (a * H1) /\ (a * H2) ) assume x in a * (H1 /\ H2) ; ::_thesis: x in (a * H1) /\ (a * H2) then consider g being Element of G such that A1: x = a * g and A2: g in H1 /\ H2 by Th103; g in H2 by A2, Th82; then A3: x in a * H2 by A1, Th103; g in H1 by A2, Th82; then x in a * H1 by A1, Th103; hence x in (a * H1) /\ (a * H2) by A3, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (a * H1) /\ (a * H2) or x in a * (H1 /\ H2) ) assume A4: x in (a * H1) /\ (a * H2) ; ::_thesis: x in a * (H1 /\ H2) then x in a * H1 by XBOOLE_0:def_4; then consider g being Element of G such that A5: x = a * g and A6: g in H1 by Th103; x in a * H2 by A4, XBOOLE_0:def_4; then consider g1 being Element of G such that A7: x = a * g1 and A8: g1 in H2 by Th103; g = g1 by A5, A7, GROUP_1:6; then g in H1 /\ H2 by A6, A8, Th82; hence x in a * (H1 /\ H2) by A5, Th103; ::_thesis: verum end; theorem :: GROUP_2:126 for G being Group for a being Element of G for H1, H2 being Subgroup of G holds (H1 /\ H2) * a = (H1 * a) /\ (H2 * a) proof let G be Group; ::_thesis: for a being Element of G for H1, H2 being Subgroup of G holds (H1 /\ H2) * a = (H1 * a) /\ (H2 * a) let a be Element of G; ::_thesis: for H1, H2 being Subgroup of G holds (H1 /\ H2) * a = (H1 * a) /\ (H2 * a) let H1, H2 be Subgroup of G; ::_thesis: (H1 /\ H2) * a = (H1 * a) /\ (H2 * a) thus (H1 /\ H2) * a c= (H1 * a) /\ (H2 * a) :: according to XBOOLE_0:def_10 ::_thesis: (H1 * a) /\ (H2 * a) c= (H1 /\ H2) * a proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (H1 /\ H2) * a or x in (H1 * a) /\ (H2 * a) ) assume x in (H1 /\ H2) * a ; ::_thesis: x in (H1 * a) /\ (H2 * a) then consider g being Element of G such that A1: x = g * a and A2: g in H1 /\ H2 by Th104; g in H2 by A2, Th82; then A3: x in H2 * a by A1, Th104; g in H1 by A2, Th82; then x in H1 * a by A1, Th104; hence x in (H1 * a) /\ (H2 * a) by A3, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (H1 * a) /\ (H2 * a) or x in (H1 /\ H2) * a ) assume A4: x in (H1 * a) /\ (H2 * a) ; ::_thesis: x in (H1 /\ H2) * a then x in H1 * a by XBOOLE_0:def_4; then consider g being Element of G such that A5: x = g * a and A6: g in H1 by Th104; x in H2 * a by A4, XBOOLE_0:def_4; then consider g1 being Element of G such that A7: x = g1 * a and A8: g1 in H2 by Th104; g = g1 by A5, A7, GROUP_1:6; then g in H1 /\ H2 by A6, A8, Th82; hence x in (H1 /\ H2) * a by A5, Th104; ::_thesis: verum end; theorem :: GROUP_2:127 for G being Group for a being Element of G for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ") proof let G be Group; ::_thesis: for a being Element of G for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ") let a be Element of G; ::_thesis: for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ") let H2 be Subgroup of G; ::_thesis: ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ") set A = (a * H2) * (a "); set x = the Element of a * H2; A1: a * H2 <> {} by Th108; then reconsider x = the Element of a * H2 as Element of G by Lm1; A2: now__::_thesis:_for_g_being_Element_of_G_st_g_in_(a_*_H2)_*_(a_")_holds_ g_"_in_(a_*_H2)_*_(a_") let g be Element of G; ::_thesis: ( g in (a * H2) * (a ") implies g " in (a * H2) * (a ") ) assume g in (a * H2) * (a ") ; ::_thesis: g " in (a * H2) * (a ") then consider g1 being Element of G such that A3: g = g1 * (a ") and A4: g1 in a * H2 by Th28; consider g2 being Element of G such that A5: g1 = a * g2 and A6: g2 in H2 by A4, Th103; g2 " in H2 by A6, Th51; then A7: (g2 ") * (a ") in H2 * (a ") by Th104; g " = ((a ") ") * ((a * g2) ") by A3, A5, GROUP_1:17 .= a * ((g2 ") * (a ")) by GROUP_1:17 ; then g " in a * (H2 * (a ")) by A7, Th27; hence g " in (a * H2) * (a ") by Th10; ::_thesis: verum end; A8: now__::_thesis:_for_g1,_g2_being_Element_of_G_st_g1_in_(a_*_H2)_*_(a_")_&_g2_in_(a_*_H2)_*_(a_")_holds_ g1_*_g2_in_(a_*_H2)_*_(a_") let g1, g2 be Element of G; ::_thesis: ( g1 in (a * H2) * (a ") & g2 in (a * H2) * (a ") implies g1 * g2 in (a * H2) * (a ") ) assume that A9: g1 in (a * H2) * (a ") and A10: g2 in (a * H2) * (a ") ; ::_thesis: g1 * g2 in (a * H2) * (a ") consider g being Element of G such that A11: g1 = g * (a ") and A12: g in a * H2 by A9, Th28; consider h being Element of G such that A13: g = a * h and A14: h in H2 by A12, Th103; (a * H2) * (a ") = a * (H2 * (a ")) by Th10; then consider b being Element of G such that A15: g2 = a * b and A16: b in H2 * (a ") by A10, Th27; consider c being Element of G such that A17: b = c * (a ") and A18: c in H2 by A16, Th104; h * c in H2 by A14, A18, Th50; then A19: a * (h * c) in a * H2 by Th103; g1 * g2 = (a * h) * ((a ") * (a * (c * (a ")))) by A11, A15, A13, A17, GROUP_1:def_3 .= (a * h) * (((a ") * a) * (c * (a "))) by GROUP_1:def_3 .= (a * h) * ((1_ G) * (c * (a "))) by GROUP_1:def_5 .= (a * h) * (c * (a ")) by GROUP_1:def_4 .= ((a * h) * c) * (a ") by GROUP_1:def_3 .= (a * (h * c)) * (a ") by GROUP_1:def_3 ; hence g1 * g2 in (a * H2) * (a ") by A19, Th28; ::_thesis: verum end; x * (a ") in (a * H2) * (a ") by A1, Th28; hence ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ") by A8, A2, Th52; ::_thesis: verum end; theorem Th128: :: GROUP_2:128 for G being Group for a, b being Element of G for H being Subgroup of G holds a * H,b * H are_equipotent proof let G be Group; ::_thesis: for a, b being Element of G for H being Subgroup of G holds a * H,b * H are_equipotent let a, b be Element of G; ::_thesis: for H being Subgroup of G holds a * H,b * H are_equipotent let H be Subgroup of G; ::_thesis: a * H,b * H are_equipotent defpred S1[ set , set ] means ex g1 being Element of G st ( \$1 = g1 & \$2 = (b * (a ")) * g1 ); A1: for x being set st x in a * H holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in a * H implies ex y being set st S1[x,y] ) assume x in a * H ; ::_thesis: ex y being set st S1[x,y] then reconsider g = x as Element of G ; reconsider y = (b * (a ")) * g as set ; take y ; ::_thesis: S1[x,y] take g ; ::_thesis: ( x = g & y = (b * (a ")) * g ) thus ( x = g & y = (b * (a ")) * g ) ; ::_thesis: verum end; consider f being Function such that A2: dom f = a * H and A3: for x being set st x in a * H holds S1[x,f . x] from CLASSES1:sch_1(A1); A4: rng f = b * H proof thus rng f c= b * H :: according to XBOOLE_0:def_10 ::_thesis: b * H c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in b * H ) assume x in rng f ; ::_thesis: x in b * H then consider y being set such that A5: y in dom f and A6: f . y = x by FUNCT_1:def_3; consider g being Element of G such that A7: y = g and A8: x = (b * (a ")) * g by A2, A3, A5, A6; consider g1 being Element of G such that A9: g = a * g1 and A10: g1 in H by A2, A5, A7, Th103; x = ((b * (a ")) * a) * g1 by A8, A9, GROUP_1:def_3 .= (b * ((a ") * a)) * g1 by GROUP_1:def_3 .= (b * (1_ G)) * g1 by GROUP_1:def_5 .= b * g1 by GROUP_1:def_4 ; hence x in b * H by A10, Th103; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in b * H or x in rng f ) assume x in b * H ; ::_thesis: x in rng f then consider g being Element of G such that A11: x = b * g and A12: g in H by Th103; A13: a * g in dom f by A2, A12, Th103; then ex g1 being Element of G st ( g1 = a * g & f . (a * g) = (b * (a ")) * g1 ) by A2, A3; then f . (a * g) = ((b * (a ")) * a) * g by GROUP_1:def_3 .= (b * ((a ") * a)) * g by GROUP_1:def_3 .= (b * (1_ G)) * g by GROUP_1:def_5 .= x by A11, GROUP_1:def_4 ; hence x in rng f by A13, FUNCT_1:def_3; ::_thesis: verum end; f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A14: ( x in dom f & y in dom f ) and A15: f . x = f . y ; ::_thesis: x = y ( ex g1 being Element of G st ( x = g1 & f . x = (b * (a ")) * g1 ) & ex g2 being Element of G st ( y = g2 & f . y = (b * (a ")) * g2 ) ) by A2, A3, A14; hence x = y by A15, GROUP_1:6; ::_thesis: verum end; hence a * H,b * H are_equipotent by A2, A4, WELLORD2:def_4; ::_thesis: verum end; theorem Th129: :: GROUP_2:129 for G being Group for a, b being Element of G for H being Subgroup of G holds a * H,H * b are_equipotent proof let G be Group; ::_thesis: for a, b being Element of G for H being Subgroup of G holds a * H,H * b are_equipotent let a, b be Element of G; ::_thesis: for H being Subgroup of G holds a * H,H * b are_equipotent let H be Subgroup of G; ::_thesis: a * H,H * b are_equipotent defpred S1[ set , set ] means ex g1 being Element of G st ( \$1 = g1 & \$2 = ((a ") * g1) * b ); A1: for x being set st x in a * H holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in a * H implies ex y being set st S1[x,y] ) assume x in a * H ; ::_thesis: ex y being set st S1[x,y] then reconsider g = x as Element of G ; reconsider y = ((a ") * g) * b as set ; take y ; ::_thesis: S1[x,y] take g ; ::_thesis: ( x = g & y = ((a ") * g) * b ) thus ( x = g & y = ((a ") * g) * b ) ; ::_thesis: verum end; consider f being Function such that A2: dom f = a * H and A3: for x being set st x in a * H holds S1[x,f . x] from CLASSES1:sch_1(A1); A4: rng f = H * b proof thus rng f c= H * b :: according to XBOOLE_0:def_10 ::_thesis: H * b c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in H * b ) assume x in rng f ; ::_thesis: x in H * b then consider y being set such that A5: y in dom f and A6: f . y = x by FUNCT_1:def_3; consider g being Element of G such that A7: y = g and A8: x = ((a ") * g) * b by A2, A3, A5, A6; consider g1 being Element of G such that A9: g = a * g1 and A10: g1 in H by A2, A5, A7, Th103; x = (((a ") * a) * g1) * b by A8, A9, GROUP_1:def_3 .= ((1_ G) * g1) * b by GROUP_1:def_5 .= g1 * b by GROUP_1:def_4 ; hence x in H * b by A10, Th104; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H * b or x in rng f ) assume x in H * b ; ::_thesis: x in rng f then consider g being Element of G such that A11: x = g * b and A12: g in H by Th104; A13: a * g in dom f by A2, A12, Th103; then ex g1 being Element of G st ( g1 = a * g & f . (a * g) = ((a ") * g1) * b ) by A2, A3; then f . (a * g) = (((a ") * a) * g) * b by GROUP_1:def_3 .= ((1_ G) * g) * b by GROUP_1:def_5 .= x by A11, GROUP_1:def_4 ; hence x in rng f by A13, FUNCT_1:def_3; ::_thesis: verum end; f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A14: x in dom f and A15: y in dom f and A16: f . x = f . y ; ::_thesis: x = y consider g2 being Element of G such that A17: y = g2 and A18: f . y = ((a ") * g2) * b by A2, A3, A15; consider g1 being Element of G such that A19: x = g1 and A20: f . x = ((a ") * g1) * b by A2, A3, A14; (a ") * g1 = (a ") * g2 by A16, A20, A18, GROUP_1:6; hence x = y by A19, A17, GROUP_1:6; ::_thesis: verum end; hence a * H,H * b are_equipotent by A2, A4, WELLORD2:def_4; ::_thesis: verum end; theorem Th130: :: GROUP_2:130 for G being Group for a, b being Element of G for H being Subgroup of G holds H * a,H * b are_equipotent proof let G be Group; ::_thesis: for a, b being Element of G for H being Subgroup of G holds H * a,H * b are_equipotent let a, b be Element of G; ::_thesis: for H being Subgroup of G holds H * a,H * b are_equipotent let H be Subgroup of G; ::_thesis: H * a,H * b are_equipotent ( H * a,b * H are_equipotent & b * H,H * b are_equipotent ) by Th129; hence H * a,H * b are_equipotent by WELLORD2:15; ::_thesis: verum end; theorem Th131: :: GROUP_2:131 for G being Group for a being Element of G for H being Subgroup of G holds ( carr H,a * H are_equipotent & carr H,H * a are_equipotent ) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( carr H,a * H are_equipotent & carr H,H * a are_equipotent ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( carr H,a * H are_equipotent & carr H,H * a are_equipotent ) let H be Subgroup of G; ::_thesis: ( carr H,a * H are_equipotent & carr H,H * a are_equipotent ) ( carr H = (1_ G) * H & carr H = H * (1_ G) ) by Th37; hence ( carr H,a * H are_equipotent & carr H,H * a are_equipotent ) by Th128, Th130; ::_thesis: verum end; theorem :: GROUP_2:132 for G being Group for a being Element of G for H being Subgroup of G holds ( card H = card (a * H) & card H = card (H * a) ) proof let G be Group; ::_thesis: for a being Element of G for H being Subgroup of G holds ( card H = card (a * H) & card H = card (H * a) ) let a be Element of G; ::_thesis: for H being Subgroup of G holds ( card H = card (a * H) & card H = card (H * a) ) let H be Subgroup of G; ::_thesis: ( card H = card (a * H) & card H = card (H * a) ) carr H,a * H are_equipotent by Th131; hence card H = card (a * H) by CARD_1:5; ::_thesis: card H = card (H * a) carr H,H * a are_equipotent by Th131; hence card H = card (H * a) by CARD_1:5; ::_thesis: verum end; theorem Th133: :: GROUP_2:133 for G being Group for a being Element of G for H being finite Subgroup of G ex B, C being finite set st ( B = a * H & C = H * a & card H = card B & card H = card C ) proof let G be Group; ::_thesis: for a being Element of G for H being finite Subgroup of G ex B, C being finite set st ( B = a * H & C = H * a & card H = card B & card H = card C ) let a be Element of G; ::_thesis: for H being finite Subgroup of G ex B, C being finite set st ( B = a * H & C = H * a & card H = card B & card H = card C ) let H be finite Subgroup of G; ::_thesis: ex B, C being finite set st ( B = a * H & C = H * a & card H = card B & card H = card C ) reconsider B = a * H, C = H * a as finite set by Th131, CARD_1:38; take B ; ::_thesis: ex C being finite set st ( B = a * H & C = H * a & card H = card B & card H = card C ) take C ; ::_thesis: ( B = a * H & C = H * a & card H = card B & card H = card C ) ( carr H,a * H are_equipotent & carr H,H * a are_equipotent ) by Th131; hence ( B = a * H & C = H * a & card H = card B & card H = card C ) by CARD_1:5; ::_thesis: verum end; definition let G be Group; let H be Subgroup of G; func Left_Cosets H -> Subset-Family of G means :Def15: :: GROUP_2:def 15 for A being Subset of G holds ( A in it iff ex a being Element of G st A = a * H ); existence ex b1 being Subset-Family of G st for A being Subset of G holds ( A in b1 iff ex a being Element of G st A = a * H ) proof defpred S1[ set ] means ex a being Element of G st \$1 = a * H; ex F being Subset-Family of G st for A being Subset of G holds ( A in F iff S1[A] ) from SUBSET_1:sch_3(); hence ex b1 being Subset-Family of G st for A being Subset of G holds ( A in b1 iff ex a being Element of G st A = a * H ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of G st ( for A being Subset of G holds ( A in b1 iff ex a being Element of G st A = a * H ) ) & ( for A being Subset of G holds ( A in b2 iff ex a being Element of G st A = a * H ) ) holds b1 = b2 proof defpred S1[ set ] means ex a being Element of G st \$1 = a * H; let F1, F2 be Subset-Family of G; ::_thesis: ( ( for A being Subset of G holds ( A in F1 iff ex a being Element of G st A = a * H ) ) & ( for A being Subset of G holds ( A in F2 iff ex a being Element of G st A = a * H ) ) implies F1 = F2 ) assume A1: for A being Subset of G holds ( A in F1 iff S1[A] ) ; ::_thesis: ( ex A being Subset of G st ( ( A in F2 implies ex a being Element of G st A = a * H ) implies ( ex a being Element of G st A = a * H & not A in F2 ) ) or F1 = F2 ) assume A2: for A being Subset of G holds ( A in F2 iff S1[A] ) ; ::_thesis: F1 = F2 thus F1 = F2 from SUBSET_1:sch_4(A1, A2); ::_thesis: verum end; func Right_Cosets H -> Subset-Family of G means :Def16: :: GROUP_2:def 16 for A being Subset of G holds ( A in it iff ex a being Element of G st A = H * a ); existence ex b1 being Subset-Family of G st for A being Subset of G holds ( A in b1 iff ex a being Element of G st A = H * a ) proof defpred S1[ set ] means ex a being Element of G st \$1 = H * a; ex F being Subset-Family of G st for A being Subset of G holds ( A in F iff S1[A] ) from SUBSET_1:sch_3(); hence ex b1 being Subset-Family of G st for A being Subset of G holds ( A in b1 iff ex a being Element of G st A = H * a ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of G st ( for A being Subset of G holds ( A in b1 iff ex a being Element of G st A = H * a ) ) & ( for A being Subset of G holds ( A in b2 iff ex a being Element of G st A = H * a ) ) holds b1 = b2 proof defpred S1[ set ] means ex a being Element of G st \$1 = H * a; let F1, F2 be Subset-Family of G; ::_thesis: ( ( for A being Subset of G holds ( A in F1 iff ex a being Element of G st A = H * a ) ) & ( for A being Subset of G holds ( A in F2 iff ex a being Element of G st A = H * a ) ) implies F1 = F2 ) assume A3: for A being Subset of G holds ( A in F1 iff S1[A] ) ; ::_thesis: ( ex A being Subset of G st ( ( A in F2 implies ex a being Element of G st A = H * a ) implies ( ex a being Element of G st A = H * a & not A in F2 ) ) or F1 = F2 ) assume A4: for A being Subset of G holds ( A in F2 iff S1[A] ) ; ::_thesis: F1 = F2 thus F1 = F2 from SUBSET_1:sch_4(A3, A4); ::_thesis: verum end; end; :: deftheorem Def15 defines Left_Cosets GROUP_2:def_15_:_ for G being Group for H being Subgroup of G for b3 being Subset-Family of G holds ( b3 = Left_Cosets H iff for A being Subset of G holds ( A in b3 iff ex a being Element of G st A = a * H ) ); :: deftheorem Def16 defines Right_Cosets GROUP_2:def_16_:_ for G being Group for H being Subgroup of G for b3 being Subset-Family of G holds ( b3 = Right_Cosets H iff for A being Subset of G holds ( A in b3 iff ex a being Element of G st A = H * a ) ); theorem :: GROUP_2:134 for G being Group for H being Subgroup of G st G is finite holds ( Right_Cosets H is finite & Left_Cosets H is finite ) ; theorem :: GROUP_2:135 for G being Group for H being Subgroup of G holds ( carr H in Left_Cosets H & carr H in Right_Cosets H ) proof let G be Group; ::_thesis: for H being Subgroup of G holds ( carr H in Left_Cosets H & carr H in Right_Cosets H ) let H be Subgroup of G; ::_thesis: ( carr H in Left_Cosets H & carr H in Right_Cosets H ) ( carr H = (1_ G) * H & carr H = H * (1_ G) ) by Th37; hence ( carr H in Left_Cosets H & carr H in Right_Cosets H ) by Def15, Def16; ::_thesis: verum end; theorem Th136: :: GROUP_2:136 for G being Group for H being Subgroup of G holds Left_Cosets H, Right_Cosets H are_equipotent proof let G be Group; ::_thesis: for H being Subgroup of G holds Left_Cosets H, Right_Cosets H are_equipotent let H be Subgroup of G; ::_thesis: Left_Cosets H, Right_Cosets H are_equipotent defpred S1[ set , set ] means ex g being Element of G st ( \$1 = g * H & \$2 = H * (g ") ); A1: for x being set st x in Left_Cosets H holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in Left_Cosets H implies ex y being set st S1[x,y] ) assume x in Left_Cosets H ; ::_thesis: ex y being set st S1[x,y] then consider g being Element of G such that A2: x = g * H by Def15; reconsider y = H * (g ") as set ; take y ; ::_thesis: S1[x,y] take g ; ::_thesis: ( x = g * H & y = H * (g ") ) thus ( x = g * H & y = H * (g ") ) by A2; ::_thesis: verum end; consider f being Function such that A3: dom f = Left_Cosets H and A4: for x being set st x in Left_Cosets H holds S1[x,f . x] from CLASSES1:sch_1(A1); A5: rng f = Right_Cosets H proof thus rng f c= Right_Cosets H :: according to XBOOLE_0:def_10 ::_thesis: Right_Cosets H c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Right_Cosets H ) assume x in rng f ; ::_thesis: x in Right_Cosets H then consider y being set such that A6: y in dom f and A7: f . y = x by FUNCT_1:def_3; ex g being Element of G st ( y = g * H & f . y = H * (g ") ) by A3, A4, A6; hence x in Right_Cosets H by A7, Def16; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Right_Cosets H or x in rng f ) assume A8: x in Right_Cosets H ; ::_thesis: x in rng f then reconsider A = x as Subset of G ; consider g being Element of G such that A9: A = H * g by A8, Def16; A10: (g ") * H in Left_Cosets H by Def15; then A11: f . ((g ") * H) in rng f by A3, FUNCT_1:def_3; consider a being Element of G such that A12: (g ") * H = a * H and A13: f . ((g ") * H) = H * (a ") by A4, A10; (a ") * (g ") in H by A12, Th114; hence x in rng f by A9, A11, A13, Th120; ::_thesis: verum end; f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A14: x in dom f and A15: y in dom f and A16: f . x = f . y ; ::_thesis: x = y consider b being Element of G such that A17: y = b * H and A18: f . y = H * (b ") by A3, A4, A15; consider a being Element of G such that A19: x = a * H and A20: f . x = H * (a ") by A3, A4, A14; (b ") * ((a ") ") in H by A16, A20, A18, Th120; hence x = y by A19, A17, Th114; ::_thesis: verum end; hence Left_Cosets H, Right_Cosets H are_equipotent by A3, A5, WELLORD2:def_4; ::_thesis: verum end; theorem Th137: :: GROUP_2:137 for G being Group for H being Subgroup of G holds ( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G ) proof let G be Group; ::_thesis: for H being Subgroup of G holds ( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G ) let H be Subgroup of G; ::_thesis: ( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G ) thus union (Left_Cosets H) = the carrier of G ::_thesis: union (Right_Cosets H) = the carrier of G proof set h = the Element of H; reconsider g = the Element of H as Element of G by Th42; thus union (Left_Cosets H) c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= union (Left_Cosets H) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in union (Left_Cosets H) ) assume x in the carrier of G ; ::_thesis: x in union (Left_Cosets H) then reconsider a = x as Element of G ; A1: a = a * (1_ G) by GROUP_1:def_4 .= a * ((g ") * g) by GROUP_1:def_5 .= (a * (g ")) * g by GROUP_1:def_3 ; A2: (a * (g ")) * H in Left_Cosets H by Def15; the Element of H in H by STRUCT_0:def_5; then a in (a * (g ")) * H by A1, Th103; hence x in union (Left_Cosets H) by A2, TARSKI:def_4; ::_thesis: verum end; set h = the Element of H; reconsider g = the Element of H as Element of G by Th42; thus union (Right_Cosets H) c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= union (Right_Cosets H) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in union (Right_Cosets H) ) assume x in the carrier of G ; ::_thesis: x in union (Right_Cosets H) then reconsider a = x as Element of G ; A3: a = (1_ G) * a by GROUP_1:def_4 .= (g * (g ")) * a by GROUP_1:def_5 .= g * ((g ") * a) by GROUP_1:def_3 ; A4: H * ((g ") * a) in Right_Cosets H by Def16; the Element of H in H by STRUCT_0:def_5; then a in H * ((g ") * a) by A3, Th104; hence x in union (Right_Cosets H) by A4, TARSKI:def_4; ::_thesis: verum end; theorem Th138: :: GROUP_2:138 for G being Group holds Left_Cosets ((1). G) = { {a} where a is Element of G : verum } proof let G be Group; ::_thesis: Left_Cosets ((1). G) = { {a} where a is Element of G : verum } set A = { {a} where a is Element of G : verum } ; thus Left_Cosets ((1). G) c= { {a} where a is Element of G : verum } :: according to XBOOLE_0:def_10 ::_thesis: { {a} where a is Element of G : verum } c= Left_Cosets ((1). G) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Left_Cosets ((1). G) or x in { {a} where a is Element of G : verum } ) assume A1: x in Left_Cosets ((1). G) ; ::_thesis: x in { {a} where a is Element of G : verum } then reconsider X = x as Subset of G ; consider g being Element of G such that A2: X = g * ((1). G) by A1, Def15; x = {g} by A2, Th110; hence x in { {a} where a is Element of G : verum } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { {a} where a is Element of G : verum } or x in Left_Cosets ((1). G) ) assume x in { {a} where a is Element of G : verum } ; ::_thesis: x in Left_Cosets ((1). G) then consider a being Element of G such that A3: x = {a} ; a * ((1). G) = {a} by Th110; hence x in Left_Cosets ((1). G) by A3, Def15; ::_thesis: verum end; theorem :: GROUP_2:139 for G being Group holds Right_Cosets ((1). G) = { {a} where a is Element of G : verum } proof let G be Group; ::_thesis: Right_Cosets ((1). G) = { {a} where a is Element of G : verum } set A = { {a} where a is Element of G : verum } ; thus Right_Cosets ((1). G) c= { {a} where a is Element of G : verum } :: according to XBOOLE_0:def_10 ::_thesis: { {a} where a is Element of G : verum } c= Right_Cosets ((1). G) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Right_Cosets ((1). G) or x in { {a} where a is Element of G : verum } ) assume A1: x in Right_Cosets ((1). G) ; ::_thesis: x in { {a} where a is Element of G : verum } then reconsider X = x as Subset of G ; consider g being Element of G such that A2: X = ((1). G) * g by A1, Def16; x = {g} by A2, Th110; hence x in { {a} where a is Element of G : verum } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { {a} where a is Element of G : verum } or x in Right_Cosets ((1). G) ) assume x in { {a} where a is Element of G : verum } ; ::_thesis: x in Right_Cosets ((1). G) then consider a being Element of G such that A3: x = {a} ; ((1). G) * a = {a} by Th110; hence x in Right_Cosets ((1). G) by A3, Def16; ::_thesis: verum end; theorem :: GROUP_2:140 for G being Group for H being strict Subgroup of G st Left_Cosets H = { {a} where a is Element of G : verum } holds H = (1). G proof let G be Group; ::_thesis: for H being strict Subgroup of G st Left_Cosets H = { {a} where a is Element of G : verum } holds H = (1). G let H be strict Subgroup of G; ::_thesis: ( Left_Cosets H = { {a} where a is Element of G : verum } implies H = (1). G ) assume A1: Left_Cosets H = { {a} where a is Element of G : verum } ; ::_thesis: H = (1). G A2: the carrier of H c= {(1_ G)} proof set a = the Element of G; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of H or x in {(1_ G)} ) assume x in the carrier of H ; ::_thesis: x in {(1_ G)} then reconsider h = x as Element of H ; A3: h in H by STRUCT_0:def_5; reconsider h = h as Element of G by Th42; the Element of G * H in Left_Cosets H by Def15; then consider b being Element of G such that A4: the Element of G * H = {b} by A1; the Element of G * h in the Element of G * H by A3, Th103; then A5: the Element of G * h = b by A4, TARSKI:def_1; 1_ G in H by Th46; then the Element of G * (1_ G) in the Element of G * H by Th103; then the Element of G * (1_ G) = b by A4, TARSKI:def_1; then h = 1_ G by A5, GROUP_1:6; hence x in {(1_ G)} by TARSKI:def_1; ::_thesis: verum end; 1_ G in H by Th46; then 1_ G in the carrier of H by STRUCT_0:def_5; then {(1_ G)} c= the carrier of H by ZFMISC_1:31; then {(1_ G)} = the carrier of H by A2, XBOOLE_0:def_10; hence H = (1). G by Def7; ::_thesis: verum end; theorem :: GROUP_2:141 for G being Group for H being strict Subgroup of G st Right_Cosets H = { {a} where a is Element of G : verum } holds H = (1). G proof let G be Group; ::_thesis: for H being strict Subgroup of G st Right_Cosets H = { {a} where a is Element of G : verum } holds H = (1). G let H be strict Subgroup of G; ::_thesis: ( Right_Cosets H = { {a} where a is Element of G : verum } implies H = (1). G ) assume A1: Right_Cosets H = { {a} where a is Element of G : verum } ; ::_thesis: H = (1). G A2: the carrier of H c= {(1_ G)} proof set a = the Element of G; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of H or x in {(1_ G)} ) assume x in the carrier of H ; ::_thesis: x in {(1_ G)} then reconsider h = x as Element of H ; A3: h in H by STRUCT_0:def_5; reconsider h = h as Element of G by Th42; H * the Element of G in Right_Cosets H by Def16; then consider b being Element of G such that A4: H * the Element of G = {b} by A1; h * the Element of G in H * the Element of G by A3, Th104; then A5: h * the Element of G = b by A4, TARSKI:def_1; 1_ G in H by Th46; then (1_ G) * the Element of G in H * the Element of G by Th104; then (1_ G) * the Element of G = b by A4, TARSKI:def_1; then h = 1_ G by A5, GROUP_1:6; hence x in {(1_ G)} by TARSKI:def_1; ::_thesis: verum end; 1_ G in H by Th46; then 1_ G in the carrier of H by STRUCT_0:def_5; then {(1_ G)} c= the carrier of H by ZFMISC_1:31; then {(1_ G)} = the carrier of H by A2, XBOOLE_0:def_10; hence H = (1). G by Def7; ::_thesis: verum end; theorem Th142: :: GROUP_2:142 for G being Group holds ( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} ) proof let G be Group; ::_thesis: ( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} ) set a = the Element of G; A1: Left_Cosets ((Omega). G) c= { the carrier of G} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Left_Cosets ((Omega). G) or x in { the carrier of G} ) assume A2: x in Left_Cosets ((Omega). G) ; ::_thesis: x in { the carrier of G} then reconsider X = x as Subset of G ; consider a being Element of G such that A3: X = a * ((Omega). G) by A2, Def15; a * ((Omega). G) = the carrier of G by Th111; hence x in { the carrier of G} by A3, TARSKI:def_1; ::_thesis: verum end; A4: Right_Cosets ((Omega). G) c= { the carrier of G} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Right_Cosets ((Omega). G) or x in { the carrier of G} ) assume A5: x in Right_Cosets ((Omega). G) ; ::_thesis: x in { the carrier of G} then reconsider X = x as Subset of G ; consider a being Element of G such that A6: X = ((Omega). G) * a by A5, Def16; ((Omega). G) * a = the carrier of G by Th111; hence x in { the carrier of G} by A6, TARSKI:def_1; ::_thesis: verum end; ((Omega). G) * the Element of G = the carrier of G by Th111; then the carrier of G in Right_Cosets ((Omega). G) by Def16; then A7: { the carrier of G} c= Right_Cosets ((Omega). G) by ZFMISC_1:31; the Element of G * ((Omega). G) = the carrier of G by Th111; then the carrier of G in Left_Cosets ((Omega). G) by Def15; then { the carrier of G} c= Left_Cosets ((Omega). G) by ZFMISC_1:31; hence ( Left_Cosets ((Omega). G) = { the carrier of G} & Right_Cosets ((Omega). G) = { the carrier of G} ) by A7, A1, A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th143: :: GROUP_2:143 for G being strict Group for H being strict Subgroup of G st Left_Cosets H = { the carrier of G} holds H = G proof let G be strict Group; ::_thesis: for H being strict Subgroup of G st Left_Cosets H = { the carrier of G} holds H = G let H be strict Subgroup of G; ::_thesis: ( Left_Cosets H = { the carrier of G} implies H = G ) assume Left_Cosets H = { the carrier of G} ; ::_thesis: H = G then A1: the carrier of G in Left_Cosets H by TARSKI:def_1; then reconsider T = the carrier of G as Subset of G ; consider a being Element of G such that A2: T = a * H by A1, Def15; now__::_thesis:_for_g_being_Element_of_G_holds_g_in_H let g be Element of G; ::_thesis: g in H ex b being Element of G st ( a * g = a * b & b in H ) by A2, Th103; hence g in H by GROUP_1:6; ::_thesis: verum end; hence H = G by Th62; ::_thesis: verum end; theorem :: GROUP_2:144 for G being strict Group for H being strict Subgroup of G st Right_Cosets H = { the carrier of G} holds H = G proof let G be strict Group; ::_thesis: for H being strict Subgroup of G st Right_Cosets H = { the carrier of G} holds H = G let H be strict Subgroup of G; ::_thesis: ( Right_Cosets H = { the carrier of G} implies H = G ) assume Right_Cosets H = { the carrier of G} ; ::_thesis: H = G then A1: the carrier of G in Right_Cosets H by TARSKI:def_1; then reconsider T = the carrier of G as Subset of G ; consider a being Element of G such that A2: T = H * a by A1, Def16; now__::_thesis:_for_g_being_Element_of_G_holds_g_in_H let g be Element of G; ::_thesis: g in H ex b being Element of G st ( g * a = b * a & b in H ) by A2, Th104; hence g in H by GROUP_1:6; ::_thesis: verum end; hence H = G by Th62; ::_thesis: verum end; definition let G be Group; let H be Subgroup of G; func Index H -> Cardinal equals :: GROUP_2:def 17 card (Left_Cosets H); correctness coherence card (Left_Cosets H) is Cardinal; ; end; :: deftheorem defines Index GROUP_2:def_17_:_ for G being Group for H being Subgroup of G holds Index H = card (Left_Cosets H); theorem :: GROUP_2:145 for G being Group for H being Subgroup of G holds ( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) ) proof let G be Group; ::_thesis: for H being Subgroup of G holds ( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) ) let H be Subgroup of G; ::_thesis: ( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) ) thus Index H = card (Left_Cosets H) ; ::_thesis: Index H = card (Right_Cosets H) Left_Cosets H, Right_Cosets H are_equipotent by Th136; hence Index H = card (Right_Cosets H) by CARD_1:5; ::_thesis: verum end; definition let G be Group; let H be Subgroup of G; assume A1: Left_Cosets H is finite ; func index H -> Element of NAT means :Def18: :: GROUP_2:def 18 ex B being finite set st ( B = Left_Cosets H & it = card B ); existence ex b1 being Element of NAT ex B being finite set st ( B = Left_Cosets H & b1 = card B ) proof reconsider B = Left_Cosets H as finite set by A1; take card B ; ::_thesis: ex B being finite set st ( B = Left_Cosets H & card B = card B ) take B ; ::_thesis: ( B = Left_Cosets H & card B = card B ) thus ( B = Left_Cosets H & card B = card B ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st ex B being finite set st ( B = Left_Cosets H & b1 = card B ) & ex B being finite set st ( B = Left_Cosets H & b2 = card B ) holds b1 = b2 ; end; :: deftheorem Def18 defines index GROUP_2:def_18_:_ for G being Group for H being Subgroup of G st Left_Cosets H is finite holds for b3 being Element of NAT holds ( b3 = index H iff ex B being finite set st ( B = Left_Cosets H & b3 = card B ) ); theorem :: GROUP_2:146 for G being Group for H being Subgroup of G st Left_Cosets H is finite holds ( ex B being finite set st ( B = Left_Cosets H & index H = card B ) & ex C being finite set st ( C = Right_Cosets H & index H = card C ) ) proof let G be Group; ::_thesis: for H being Subgroup of G st Left_Cosets H is finite holds ( ex B being finite set st ( B = Left_Cosets H & index H = card B ) & ex C being finite set st ( C = Right_Cosets H & index H = card C ) ) let H be Subgroup of G; ::_thesis: ( Left_Cosets H is finite implies ( ex B being finite set st ( B = Left_Cosets H & index H = card B ) & ex C being finite set st ( C = Right_Cosets H & index H = card C ) ) ) assume Left_Cosets H is finite ; ::_thesis: ( ex B being finite set st ( B = Left_Cosets H & index H = card B ) & ex C being finite set st ( C = Right_Cosets H & index H = card C ) ) then reconsider B = Left_Cosets H as finite set ; hereby ::_thesis: ex C being finite set st ( C = Right_Cosets H & index H = card C ) take B = B; ::_thesis: ( B = Left_Cosets H & index H = card B ) thus ( B = Left_Cosets H & index H = card B ) by Def18; ::_thesis: verum end; then reconsider C = Right_Cosets H as finite set by Th136, CARD_1:38; take C ; ::_thesis: ( C = Right_Cosets H & index H = card C ) ( index H = card B & B,C are_equipotent ) by Def18, Th136; hence ( C = Right_Cosets H & index H = card C ) by CARD_1:5; ::_thesis: verum end; Lm5: for k being Nat for X being finite set st ( for Y being set st Y in X holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ) holds ex C being finite set st ( C = union X & card C = k * (card X) ) proof let k be Nat; ::_thesis: for X being finite set st ( for Y being set st Y in X holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ) holds ex C being finite set st ( C = union X & card C = k * (card X) ) let X be finite set ; ::_thesis: ( ( for Y being set st Y in X holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st ( C = union X & card C = k * (card X) ) ) percases ( X = {} or X <> {} ) ; supposeA1: X = {} ; ::_thesis: ( ( for Y being set st Y in X holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st ( C = union X & card C = k * (card X) ) ) reconsider E = {} as finite set ; assume for Y being set st Y in X holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ; ::_thesis: ex C being finite set st ( C = union X & card C = k * (card X) ) take E ; ::_thesis: ( E = union X & card E = k * (card X) ) thus ( E = union X & card E = k * (card X) ) by A1, CARD_1:27, ZFMISC_1:2; ::_thesis: verum end; suppose X <> {} ; ::_thesis: ( ( for Y being set st Y in X holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st ( C = union X & card C = k * (card X) ) ) then reconsider D = X as non empty set ; defpred S1[ Element of Fin D] means ( ( for Y being set st Y in \$1 holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in \$1 & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st ( C = union \$1 & card C = k * (card \$1) ) ); A2: for S being Element of Fin D for s being Element of D st S1[S] & not s in S holds S1[S \/ {.s.}] proof let S be Element of Fin D; ::_thesis: for s being Element of D st S1[S] & not s in S holds S1[S \/ {.s.}] let s be Element of D; ::_thesis: ( S1[S] & not s in S implies S1[S \/ {.s.}] ) assume that A3: ( ( for Y being set st Y in S holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st ( C = union S & card C = k * (card S) ) ) and A4: not s in S and A5: for Y being set st Y in S \/ {s} holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ; ::_thesis: ex C being finite set st ( C = union (S \/ {.s.}) & card C = k * (card (S \/ {.s.})) ) A6: card (S \/ {s}) = (card S) + 1 by A4, CARD_2:41; now__::_thesis:_for_Y_being_set_st_Y_in_S_holds_ Y_is_finite let Y be set ; ::_thesis: ( Y in S implies Y is finite ) assume Y in S ; ::_thesis: Y is finite then Y in S \/ {s} by XBOOLE_0:def_3; then ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) by A5; hence Y is finite ; ::_thesis: verum end; then reconsider D1 = union S as finite set by FINSET_1:7; A7: now__::_thesis:_for_Y,_Z_being_set_st_Y_in_S_holds_ ex_B_being_finite_set_st_ (_B_=_Y_&_card_B_=_k_&_(_for_Z_being_set_st_Z_in_S_&_Y_<>_Z_holds_ (_Y,Z_are_equipotent_&_Y_misses_Z_)_)_) let Y, Z be set ; ::_thesis: ( Y in S implies ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ) assume Y in S ; ::_thesis: ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) then Y in S \/ {s} by XBOOLE_0:def_3; then consider B being finite set such that A8: ( B = Y & card B = k ) and A9: for Z being set st Z in S \/ {s} & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) by A5; take B = B; ::_thesis: ( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) thus ( B = Y & card B = k ) by A8; ::_thesis: for Z being set st Z in S & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) let Z be set ; ::_thesis: ( Z in S & Y <> Z implies ( Y,Z are_equipotent & Y misses Z ) ) assume that A10: Z in S and A11: Y <> Z ; ::_thesis: ( Y,Z are_equipotent & Y misses Z ) Z in S \/ {s} by A10, XBOOLE_0:def_3; hence ( Y,Z are_equipotent & Y misses Z ) by A9, A11; ::_thesis: verum end; s in {s} by TARSKI:def_1; then s in S \/ {s} by XBOOLE_0:def_3; then A12: ex B being finite set st ( B = s & card B = k & ( for Z being set st Z in S \/ {s} & s <> Z holds ( s,Z are_equipotent & s misses Z ) ) ) by A5; then reconsider T = s as finite set ; A13: union {s} = s by ZFMISC_1:25; then A14: union (S \/ {s}) = D1 \/ T by ZFMISC_1:78; then reconsider D2 = union (S \/ {s}) as finite set ; take D2 ; ::_thesis: ( D2 = union (S \/ {.s.}) & card D2 = k * (card (S \/ {.s.})) ) thus D2 = union (S \/ {s}) ; ::_thesis: card D2 = k * (card (S \/ {.s.})) now__::_thesis:_not_union_S_meets_union_{s} assume union S meets union {s} ; ::_thesis: contradiction then consider x being set such that A15: x in union S and A16: x in union {s} by XBOOLE_0:3; consider Y being set such that A17: x in Y and A18: Y in S by A15, TARSKI:def_4; consider Z being set such that A19: x in Z and A20: Z in {s} by A16, TARSKI:def_4; A21: Z in S \/ {s} by A20, XBOOLE_0:def_3; Y in S \/ {s} by A18, XBOOLE_0:def_3; then A22: ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) by A5; Z <> Y by A4, A18, A20, TARSKI:def_1; then Y misses Z by A21, A22; hence contradiction by A17, A19, XBOOLE_0:3; ::_thesis: verum end; hence card D2 = (k * (card S)) + (k * 1) by A3, A13, A12, A14, A7, CARD_2:40 .= k * (card (S \/ {s})) by A6 ; ::_thesis: verum end; A23: X is Element of Fin D by FINSUB_1:def_5; A24: S1[ {}. D] by ZFMISC_1:2; for B being Element of Fin D holds S1[B] from SETWISEO:sch_2(A24, A2); hence ( ( for Y being set st Y in X holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st ( C = union X & card C = k * (card X) ) ) by A23; ::_thesis: verum end; end; end; theorem Th147: :: GROUP_2:147 for G being finite Group for H being Subgroup of G holds card G = (card H) * (index H) proof let G be finite Group; ::_thesis: for H being Subgroup of G holds card G = (card H) * (index H) let H be Subgroup of G; ::_thesis: card G = (card H) * (index H) reconsider C = Left_Cosets H as finite set ; now__::_thesis:_for_X_being_set_st_X_in_C_holds_ ex_B_being_finite_set_st_ (_B_=_X_&_card_B_=_card_H_&_(_for_Y_being_set_st_Y_in_C_&_X_<>_Y_holds_ (_X,Y_are_equipotent_&_X_misses_Y_)_)_) let X be set ; ::_thesis: ( X in C implies ex B being finite set st ( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds ( X,Y are_equipotent & X misses Y ) ) ) ) assume A1: X in C ; ::_thesis: ex B being finite set st ( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds ( X,Y are_equipotent & X misses Y ) ) ) then reconsider x = X as Subset of G ; x is finite ; then reconsider B = X as finite set ; take B = B; ::_thesis: ( B = X & card B = card H & ( for Y being set st Y in C & X <> Y holds ( X,Y are_equipotent & X misses Y ) ) ) thus B = X ; ::_thesis: ( card B = card H & ( for Y being set st Y in C & X <> Y holds ( X,Y are_equipotent & X misses Y ) ) ) consider a being Element of G such that A2: x = a * H by A1, Def15; ex B, C being finite set st ( B = a * H & C = H * a & card H = card B & card H = card C ) by Th133; hence card B = card H by A2; ::_thesis: for Y being set st Y in C & X <> Y holds ( X,Y are_equipotent & X misses Y ) let Y be set ; ::_thesis: ( Y in C & X <> Y implies ( X,Y are_equipotent & X misses Y ) ) assume that A3: Y in C and A4: X <> Y ; ::_thesis: ( X,Y are_equipotent & X misses Y ) reconsider y = Y as Subset of G by A3; A5: ex b being Element of G st y = b * H by A3, Def15; hence X,Y are_equipotent by A2, Th128; ::_thesis: X misses Y thus X misses Y by A2, A4, A5, Th115; ::_thesis: verum end; then A6: ex D being finite set st ( D = union C & card D = (card H) * (card C) ) by Lm5; union (Left_Cosets H) = the carrier of G by Th137; hence card G = (card H) * (index H) by A6, Def18; ::_thesis: verum end; theorem :: GROUP_2:148 for G being finite Group for H being Subgroup of G holds card H divides card G proof let G be finite Group; ::_thesis: for H being Subgroup of G holds card H divides card G let H be Subgroup of G; ::_thesis: card H divides card G card G = (card H) * (index H) by Th147; hence card H divides card G by NAT_D:def_3; ::_thesis: verum end; theorem :: GROUP_2:149 for G being finite Group for I, H being Subgroup of G for J being Subgroup of H st I = J holds index I = (index J) * (index H) proof let G be finite Group; ::_thesis: for I, H being Subgroup of G for J being Subgroup of H st I = J holds index I = (index J) * (index H) let I, H be Subgroup of G; ::_thesis: for J being Subgroup of H st I = J holds index I = (index J) * (index H) let J be Subgroup of H; ::_thesis: ( I = J implies index I = (index J) * (index H) ) assume A1: I = J ; ::_thesis: index I = (index J) * (index H) ( card G = (card H) * (index H) & card H = (card J) * (index J) ) by Th147; then (card I) * ((index J) * (index H)) = (card I) * (index I) by A1, Th147; hence index I = (index J) * (index H) by XCMPLX_1:5; ::_thesis: verum end; theorem :: GROUP_2:150 for G being Group holds index ((Omega). G) = 1 proof let G be Group; ::_thesis: index ((Omega). G) = 1 Left_Cosets ((Omega). G) = { the carrier of G} by Th142; hence index ((Omega). G) = card { the carrier of G} by Def18 .= 1 by CARD_1:30 ; ::_thesis: verum end; theorem :: GROUP_2:151 for G being strict Group for H being strict Subgroup of G st Left_Cosets H is finite & index H = 1 holds H = G proof let G be strict Group; ::_thesis: for H being strict Subgroup of G st Left_Cosets H is finite & index H = 1 holds H = G let H be strict Subgroup of G; ::_thesis: ( Left_Cosets H is finite & index H = 1 implies H = G ) assume that A1: Left_Cosets H is finite and A2: index H = 1 ; ::_thesis: H = G reconsider B = Left_Cosets H as finite set by A1; card B = 1 by A2, Def18; then consider x being set such that A3: Left_Cosets H = {x} by CARD_2:42; ( union {x} = x & union (Left_Cosets H) = the carrier of G ) by Th137, ZFMISC_1:25; hence H = G by A3, Th143; ::_thesis: verum end; theorem :: GROUP_2:152 for G being Group holds Index ((1). G) = card G proof let G be Group; ::_thesis: Index ((1). G) = card G deffunc H1( set ) -> set = {\$1}; consider f being Function such that A1: dom f = the carrier of G and A2: for x being set st x in the carrier of G holds f . x = H1(x) from FUNCT_1:sch_3(); A3: rng f = Left_Cosets ((1). G) proof thus rng f c= Left_Cosets ((1). G) :: according to XBOOLE_0:def_10 ::_thesis: Left_Cosets ((1). G) c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Left_Cosets ((1). G) ) assume x in rng f ; ::_thesis: x in Left_Cosets ((1). G) then consider y being set such that A4: y in dom f and A5: f . y = x by FUNCT_1:def_3; reconsider y = y as Element of G by A1, A4; x = {y} by A2, A5; then x in { {a} where a is Element of G : verum } ; hence x in Left_Cosets ((1). G) by Th138; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Left_Cosets ((1). G) or x in rng f ) assume x in Left_Cosets ((1). G) ; ::_thesis: x in rng f then x in { {a} where a is Element of G : verum } by Th138; then consider a being Element of G such that A6: x = {a} ; f . a = {a} by A2; hence x in rng f by A1, A6, FUNCT_1:def_3; ::_thesis: verum end; f is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A7: ( x in dom f & y in dom f ) and A8: f . x = f . y ; ::_thesis: x = y ( f . y = {y} & f . x = {x} ) by A1, A2, A7; hence x = y by A8, ZFMISC_1:3; ::_thesis: verum end; then the carrier of G, Left_Cosets ((1). G) are_equipotent by A1, A3, WELLORD2:def_4; hence Index ((1). G) = card G by CARD_1:5; ::_thesis: verum end; theorem :: GROUP_2:153 for G being finite Group holds index ((1). G) = card G proof let G be finite Group; ::_thesis: index ((1). G) = card G thus card G = (card ((1). G)) * (index ((1). G)) by Th147 .= 1 * (index ((1). G)) by Th69 .= index ((1). G) ; ::_thesis: verum end; theorem Th154: :: GROUP_2:154 for G being finite Group for H being strict Subgroup of G st index H = card G holds H = (1). G proof let G be finite Group; ::_thesis: for H being strict Subgroup of G st index H = card G holds H = (1). G let H be strict Subgroup of G; ::_thesis: ( index H = card G implies H = (1). G ) assume index H = card G ; ::_thesis: H = (1). G then 1 * (card G) = (card H) * (card G) by Th147; hence H = (1). G by Th70, XCMPLX_1:5; ::_thesis: verum end; theorem :: GROUP_2:155 for G being Group for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds ( G is finite & H = (1). G ) proof let G be Group; ::_thesis: for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds ( G is finite & H = (1). G ) let H be strict Subgroup of G; ::_thesis: ( Left_Cosets H is finite & Index H = card G implies ( G is finite & H = (1). G ) ) assume that A1: Left_Cosets H is finite and A2: Index H = card G ; ::_thesis: ( G is finite & H = (1). G ) thus A3: G is finite by A1, A2; ::_thesis: H = (1). G ex B being finite set st ( B = Left_Cosets H & index H = card B ) by A1, Def18; hence H = (1). G by A2, A3, Th154; ::_thesis: verum end; theorem :: GROUP_2:156 for k being Nat for X being finite set st ( for Y being set st Y in X holds ex B being finite set st ( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds ( Y,Z are_equipotent & Y misses Z ) ) ) ) holds ex C being finite set st ( C = union X & card C = k * (card X) ) by Lm5;