:: GROUP_11 semantic presentation begin theorem Th1: :: GROUP_11:1 for G being Group for N being normal Subgroup of G for x1, x2 being Element of G holds (x1 * N) * (x2 * N) = (x1 * x2) * N proof let G be Group; ::_thesis: for N being normal Subgroup of G for x1, x2 being Element of G holds (x1 * N) * (x2 * N) = (x1 * x2) * N let N be normal Subgroup of G; ::_thesis: for x1, x2 being Element of G holds (x1 * N) * (x2 * N) = (x1 * x2) * N let x1, x2 be Element of G; ::_thesis: (x1 * N) * (x2 * N) = (x1 * x2) * N (x1 * N) * (x2 * N) = ((x1 * N) * x2) * N by GROUP_2:10 .= (x1 * (N * x2)) * N by GROUP_2:29 .= (x1 * (x2 * N)) * N by GROUP_3:117 .= ((x1 * x2) * N) * N by GROUP_2:105 .= (x1 * x2) * (N * N) by GROUP_2:29 ; hence (x1 * N) * (x2 * N) = (x1 * x2) * N by GROUP_2:76; ::_thesis: verum end; theorem Th2: :: GROUP_11:2 for G being Group for N being Subgroup of G for x, y being Element of G st y in x * N holds x * N = y * N proof let G be Group; ::_thesis: for N being Subgroup of G for x, y being Element of G st y in x * N holds x * N = y * N let N be Subgroup of G; ::_thesis: for x, y being Element of G st y in x * N holds x * N = y * N let x, y be Element of G; ::_thesis: ( y in x * N implies x * N = y * N ) assume A1: y in x * N ; ::_thesis: x * N = y * N y in y * N by GROUP_2:108; then x * N meets y * N by A1, XBOOLE_0:3; hence x * N = y * N by GROUP_2:115; ::_thesis: verum end; theorem Th3: :: GROUP_11:3 for G being Group for N, H being Subgroup of G for x being Element of G st x * N meets carr H holds ex y being Element of G st ( y in x * N & y in H ) proof let G be Group; ::_thesis: for N, H being Subgroup of G for x being Element of G st x * N meets carr H holds ex y being Element of G st ( y in x * N & y in H ) let N, H be Subgroup of G; ::_thesis: for x being Element of G st x * N meets carr H holds ex y being Element of G st ( y in x * N & y in H ) let x be Element of G; ::_thesis: ( x * N meets carr H implies ex y being Element of G st ( y in x * N & y in H ) ) assume x * N meets carr H ; ::_thesis: ex y being Element of G st ( y in x * N & y in H ) then consider y being set such that A1: ( y in x * N & y in carr H ) by XBOOLE_0:3; reconsider y = y as Element of G by A1; y in H by A1, STRUCT_0:def_5; hence ex y being Element of G st ( y in x * N & y in H ) by A1; ::_thesis: verum end; theorem Th4: :: GROUP_11:4 for G being Group for x, y being Element of G for N being normal Subgroup of G st y in N holds (x * y) * (x ") in N proof let G be Group; ::_thesis: for x, y being Element of G for N being normal Subgroup of G st y in N holds (x * y) * (x ") in N let x, y be Element of G; ::_thesis: for N being normal Subgroup of G st y in N holds (x * y) * (x ") in N let N be normal Subgroup of G; ::_thesis: ( y in N implies (x * y) * (x ") in N ) assume y in N ; ::_thesis: (x * y) * (x ") in N then x * y in x * N by GROUP_2:103; then x * y in N * x by GROUP_3:117; then consider y1 being Element of G such that A1: ( x * y = y1 * x & y1 in N ) by GROUP_2:104; (x * y) * (x ") = y1 * (x * (x ")) by A1, GROUP_1:def_3 .= y1 * (1_ G) by GROUP_1:def_5 .= y1 by GROUP_1:def_4 ; hence (x * y) * (x ") in N by A1; ::_thesis: verum end; theorem Th5: :: GROUP_11:5 for G being Group for N being Subgroup of G st ( for x, y being Element of G st y in N holds (x * y) * (x ") in N ) holds N is normal proof let G be Group; ::_thesis: for N being Subgroup of G st ( for x, y being Element of G st y in N holds (x * y) * (x ") in N ) holds N is normal let N be Subgroup of G; ::_thesis: ( ( for x, y being Element of G st y in N holds (x * y) * (x ") in N ) implies N is normal ) assume A1: for x, y being Element of G st y in N holds (x * y) * (x ") in N ; ::_thesis: N is normal for x being Element of G holds x * N c= N * x proof let x be Element of G; ::_thesis: x * N c= N * x let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x * N or z in N * x ) assume A2: z in x * N ; ::_thesis: z in N * x then reconsider z = z as Element of G ; consider z1 being Element of G such that A3: ( z = x * z1 & z1 in N ) by A2, GROUP_2:103; A4: (x * z1) * (x ") in N by A1, A3; ((x * z1) * (x ")) * x = z by A3, GROUP_3:1; hence z in N * x by A4, GROUP_2:104; ::_thesis: verum end; hence N is normal by GROUP_3:118; ::_thesis: verum end; theorem Th6: :: GROUP_11:6 for G being Group for H1, H2 being Subgroup of G for x being Element of G holds ( x in H1 * H2 iff ex a, b being Element of G st ( x = a * b & a in H1 & b in H2 ) ) proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G for x being Element of G holds ( x in H1 * H2 iff ex a, b being Element of G st ( x = a * b & a in H1 & b in H2 ) ) let H1, H2 be Subgroup of G; ::_thesis: for x being Element of G holds ( x in H1 * H2 iff ex a, b being Element of G st ( x = a * b & a in H1 & b in H2 ) ) let x be Element of G; ::_thesis: ( x in H1 * H2 iff ex a, b being Element of G st ( x = a * b & a in H1 & b in H2 ) ) thus ( x in H1 * H2 implies ex a, b being Element of G st ( x = a * b & a in H1 & b in H2 ) ) ::_thesis: ( ex a, b being Element of G st ( x = a * b & a in H1 & b in H2 ) implies x in H1 * H2 ) proof assume x in H1 * H2 ; ::_thesis: ex a, b being Element of G st ( x = a * b & a in H1 & b in H2 ) then consider a, b being Element of G such that A1: ( x = a * b & a in carr H1 & b in carr H2 ) ; ( a in H1 & b in H2 ) by A1, STRUCT_0:def_5; hence ex a, b being Element of G st ( x = a * b & a in H1 & b in H2 ) by A1; ::_thesis: verum end; given a, b being Element of G such that A2: ( x = a * b & a in H1 & b in H2 ) ; ::_thesis: x in H1 * H2 ( a in carr H1 & b in carr H2 ) by A2, STRUCT_0:def_5; hence x in H1 * H2 by A2; ::_thesis: verum end; theorem Th7: :: GROUP_11:7 for G being Group for N1, N2 being strict normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N1 * N2 proof let G be Group; ::_thesis: for N1, N2 being strict normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N1 * N2 let N1, N2 be strict normal Subgroup of G; ::_thesis: ex M being strict Subgroup of G st the carrier of M = N1 * N2 A1: 1_ G in N1 * N2 proof A2: ( 1_ G in N1 & 1_ G in N2 ) by GROUP_2:46; (1_ G) * (1_ G) = 1_ G by GROUP_1:def_4; hence 1_ G in N1 * N2 by A2, Th6; ::_thesis: verum end; A3: for x, y being Element of G st x in N1 * N2 & y in N1 * N2 holds x * y in N1 * N2 proof let x, y be Element of G; ::_thesis: ( x in N1 * N2 & y in N1 * N2 implies x * y in N1 * N2 ) assume that A4: x in N1 * N2 and A5: y in N1 * N2 ; ::_thesis: x * y in N1 * N2 consider a, b being Element of G such that A6: ( x = a * b & a in N1 & b in N2 ) by A4, Th6; consider c, d being Element of G such that A7: ( y = c * d & c in N1 & d in N2 ) by A5, Th6; A8: x * y = ((a * b) * c) * d by A6, A7, GROUP_1:def_3 .= (a * (b * c)) * d by GROUP_1:def_3 ; b * c in N2 * N1 by A6, A7, Th6; then b * c in N1 * N2 by GROUP_3:125; then consider b9, c9 being Element of G such that A9: ( b * c = b9 * c9 & b9 in N1 & c9 in N2 ) by Th6; A10: x * y = ((a * b9) * c9) * d by A8, A9, GROUP_1:def_3 .= (a * b9) * (c9 * d) by GROUP_1:def_3 ; A11: a * b9 in N1 by A6, A9, GROUP_2:50; c9 * d in N2 by A7, A9, GROUP_2:50; hence x * y in N1 * N2 by A10, A11, Th6; ::_thesis: verum end; for x being Element of G st x in N1 * N2 holds x " in N1 * N2 proof let x be Element of G; ::_thesis: ( x in N1 * N2 implies x " in N1 * N2 ) assume x in N1 * N2 ; ::_thesis: x " in N1 * N2 then consider a, b being Element of G such that A12: ( x = a * b & a in N1 & b in N2 ) by Th6; A13: x " = (b ") * (a ") by A12, GROUP_1:17; ( b " in N2 & a " in N1 ) by A12, GROUP_2:51; then x " in N2 * N1 by A13, Th6; hence x " in N1 * N2 by GROUP_3:125; ::_thesis: verum end; hence ex M being strict Subgroup of G st the carrier of M = N1 * N2 by A1, A3, GROUP_2:52; ::_thesis: verum end; theorem Th8: :: GROUP_11:8 for G being Group for N1, N2 being strict normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N1 * N2 proof let G be Group; ::_thesis: for N1, N2 being strict normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N1 * N2 let N1, N2 be strict normal Subgroup of G; ::_thesis: ex M being strict normal Subgroup of G st the carrier of M = N1 * N2 consider M being strict Subgroup of G such that A1: the carrier of M = N1 * N2 by Th7; for x, y being Element of G st y in M holds (x * y) * (x ") in M proof let x, y be Element of G; ::_thesis: ( y in M implies (x * y) * (x ") in M ) assume y in M ; ::_thesis: (x * y) * (x ") in M then y in the carrier of M by STRUCT_0:def_5; then consider a, b being Element of G such that A2: ( y = a * b & a in N1 & b in N2 ) by A1, Th6; A3: (x * y) * (x ") = ((x * a) * b) * (x ") by A2, GROUP_1:def_3 .= (x * a) * (b * (x ")) by GROUP_1:def_3 .= ((x * a) * (1_ G)) * (b * (x ")) by GROUP_1:def_4 .= ((x * a) * ((x ") * x)) * (b * (x ")) by GROUP_1:def_5 .= (((x * a) * (x ")) * x) * (b * (x ")) by GROUP_1:def_3 .= ((x * a) * (x ")) * (x * (b * (x "))) by GROUP_1:def_3 .= ((x * a) * (x ")) * ((x * b) * (x ")) by GROUP_1:def_3 ; ( (x * a) * (x ") in N1 & (x * b) * (x ") in N2 ) by A2, Th4; then (x * y) * (x ") in N1 * N2 by A3, Th6; hence (x * y) * (x ") in M by A1, STRUCT_0:def_5; ::_thesis: verum end; then M is normal Subgroup of G by Th5; hence ex M being strict normal Subgroup of G st the carrier of M = N1 * N2 by A1; ::_thesis: verum end; theorem Th9: :: GROUP_11:9 for G being Group for N, N1, N2 being Subgroup of G st the carrier of N = N1 * N2 holds ( N1 is Subgroup of N & N2 is Subgroup of N ) proof let G be Group; ::_thesis: for N, N1, N2 being Subgroup of G st the carrier of N = N1 * N2 holds ( N1 is Subgroup of N & N2 is Subgroup of N ) let N, N1, N2 be Subgroup of G; ::_thesis: ( the carrier of N = N1 * N2 implies ( N1 is Subgroup of N & N2 is Subgroup of N ) ) assume A1: the carrier of N = N1 * N2 ; ::_thesis: ( N1 is Subgroup of N & N2 is Subgroup of N ) for x being Element of G st x in N1 holds x in N proof let x be Element of G; ::_thesis: ( x in N1 implies x in N ) assume A2: x in N1 ; ::_thesis: x in N A3: 1_ G in N2 by GROUP_2:46; x = x * (1_ G) by GROUP_1:def_4; then x in N1 * N2 by A2, A3, Th6; hence x in N by A1, STRUCT_0:def_5; ::_thesis: verum end; hence N1 is Subgroup of N by GROUP_2:58; ::_thesis: N2 is Subgroup of N for y being Element of G st y in N2 holds y in N proof let y be Element of G; ::_thesis: ( y in N2 implies y in N ) assume A4: y in N2 ; ::_thesis: y in N A5: 1_ G in N1 by GROUP_2:46; y = (1_ G) * y by GROUP_1:def_4; then y in N1 * N2 by A4, A5, Th6; hence y in N by A1, STRUCT_0:def_5; ::_thesis: verum end; hence N2 is Subgroup of N by GROUP_2:58; ::_thesis: verum end; theorem Th10: :: GROUP_11:10 for G being Group for N, N1, N2 being normal Subgroup of G for a, b being Element of G st the carrier of N = N1 * N2 holds (a * N1) * (b * N2) = (a * b) * N proof let G be Group; ::_thesis: for N, N1, N2 being normal Subgroup of G for a, b being Element of G st the carrier of N = N1 * N2 holds (a * N1) * (b * N2) = (a * b) * N let N, N1, N2 be normal Subgroup of G; ::_thesis: for a, b being Element of G st the carrier of N = N1 * N2 holds (a * N1) * (b * N2) = (a * b) * N let a, b be Element of G; ::_thesis: ( the carrier of N = N1 * N2 implies (a * N1) * (b * N2) = (a * b) * N ) assume A1: the carrier of N = N1 * N2 ; ::_thesis: (a * N1) * (b * N2) = (a * b) * N (a * N1) * (b * N2) = ((a * N1) * b) * N2 by GROUP_2:10 .= (a * (N1 * b)) * N2 by GROUP_2:29 .= (a * (b * N1)) * N2 by GROUP_3:117 .= ((a * b) * N1) * N2 by GROUP_2:105 .= (a * b) * (N1 * N2) by GROUP_4:45 ; hence (a * N1) * (b * N2) = (a * b) * N by A1; ::_thesis: verum end; theorem :: GROUP_11:11 for G being Group for N being normal Subgroup of G for x being Element of G holds (x * N) * (x ") c= carr N proof let G be Group; ::_thesis: for N being normal Subgroup of G for x being Element of G holds (x * N) * (x ") c= carr N let N be normal Subgroup of G; ::_thesis: for x being Element of G holds (x * N) * (x ") c= carr N let x be Element of G; ::_thesis: (x * N) * (x ") c= carr N x * N c= N * x by GROUP_3:118; then A1: (x * N) * (x ") c= (N * x) * (x ") by GROUP_3:5; (N * x) * (x ") = N * (x * (x ")) by GROUP_2:107 .= N * (1_ G) by GROUP_1:def_5 ; hence (x * N) * (x ") c= carr N by A1, GROUP_2:109; ::_thesis: verum end; definition let G be Group; let A be Subset of G; let N be Subgroup of G; funcN ` A -> Subset of G equals :: GROUP_11:def 1 { x where x is Element of G : x * N c= A } ; correctness coherence { x where x is Element of G : x * N c= A } is Subset of G; proof { x where x is Element of G : x * N c= A } c= the carrier of G proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Element of G : x * N c= A } or y in the carrier of G ) assume y in { x where x is Element of G : x * N c= A } ; ::_thesis: y in the carrier of G then ex x being Element of G st ( y = x & x * N c= A ) ; hence y in the carrier of G ; ::_thesis: verum end; hence { x where x is Element of G : x * N c= A } is Subset of G ; ::_thesis: verum end; funcN ~ A -> Subset of G equals :: GROUP_11:def 2 { x where x is Element of G : x * N meets A } ; correctness coherence { x where x is Element of G : x * N meets A } is Subset of G; proof { x where x is Element of G : x * N meets A } c= the carrier of G proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Element of G : x * N meets A } or y in the carrier of G ) assume y in { x where x is Element of G : x * N meets A } ; ::_thesis: y in the carrier of G then ex x being Element of G st ( y = x & x * N meets A ) ; hence y in the carrier of G ; ::_thesis: verum end; hence { x where x is Element of G : x * N meets A } is Subset of G ; ::_thesis: verum end; end; :: deftheorem defines ` GROUP_11:def_1_:_ for G being Group for A being Subset of G for N being Subgroup of G holds N ` A = { x where x is Element of G : x * N c= A } ; :: deftheorem defines ~ GROUP_11:def_2_:_ for G being Group for A being Subset of G for N being Subgroup of G holds N ~ A = { x where x is Element of G : x * N meets A } ; theorem Th12: :: GROUP_11:12 for G being Group for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ` A holds x * N c= A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ` A holds x * N c= A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G for x being Element of G st x in N ` A holds x * N c= A let N be Subgroup of G; ::_thesis: for x being Element of G st x in N ` A holds x * N c= A let x be Element of G; ::_thesis: ( x in N ` A implies x * N c= A ) assume x in N ` A ; ::_thesis: x * N c= A then ex x1 being Element of G st ( x1 = x & x1 * N c= A ) ; hence x * N c= A ; ::_thesis: verum end; theorem :: GROUP_11:13 for G being Group for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x * N c= A holds x in N ` A ; theorem Th14: :: GROUP_11:14 for G being Group for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ~ A holds x * N meets A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ~ A holds x * N meets A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G for x being Element of G st x in N ~ A holds x * N meets A let N be Subgroup of G; ::_thesis: for x being Element of G st x in N ~ A holds x * N meets A let x be Element of G; ::_thesis: ( x in N ~ A implies x * N meets A ) assume x in N ~ A ; ::_thesis: x * N meets A then ex x1 being Element of G st ( x = x1 & x1 * N meets A ) ; hence x * N meets A ; ::_thesis: verum end; theorem :: GROUP_11:15 for G being Group for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x * N meets A holds x in N ~ A ; theorem Th16: :: GROUP_11:16 for G being Group for A being non empty Subset of G for N being Subgroup of G holds N ` A c= A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds N ` A c= A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ` A c= A let N be Subgroup of G; ::_thesis: N ` A c= A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` A or x in A ) assume x in N ` A ; ::_thesis: x in A then consider y being Element of G such that A1: ( y = x & y * N c= A ) ; y in y * N by GROUP_2:108; hence x in A by A1; ::_thesis: verum end; theorem Th17: :: GROUP_11:17 for G being Group for A being non empty Subset of G for N being Subgroup of G holds A c= N ~ A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds A c= N ~ A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds A c= N ~ A let N be Subgroup of G; ::_thesis: A c= N ~ A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in N ~ A ) assume A1: x in A ; ::_thesis: x in N ~ A then reconsider x9 = x as Element of G ; x9 in x9 * N by GROUP_2:108; then x9 * N meets A by A1, XBOOLE_0:3; hence x in N ~ A ; ::_thesis: verum end; theorem Th18: :: GROUP_11:18 for G being Group for A being non empty Subset of G for N being Subgroup of G holds N ` A c= N ~ A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds N ` A c= N ~ A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ` A c= N ~ A let N be Subgroup of G; ::_thesis: N ` A c= N ~ A A1: N ` A c= A by Th16; A c= N ~ A by Th17; hence N ` A c= N ~ A by A1, XBOOLE_1:1; ::_thesis: verum end; theorem :: GROUP_11:19 for G being Group for A, B being non empty Subset of G for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B) proof let G be Group; ::_thesis: for A, B being non empty Subset of G for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B) let A, B be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B) let N be Subgroup of G; ::_thesis: N ~ (A \/ B) = (N ~ A) \/ (N ~ B) thus N ~ (A \/ B) c= (N ~ A) \/ (N ~ B) :: according to XBOOLE_0:def_10 ::_thesis: (N ~ A) \/ (N ~ B) c= N ~ (A \/ B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ (A \/ B) or x in (N ~ A) \/ (N ~ B) ) assume A1: x in N ~ (A \/ B) ; ::_thesis: x in (N ~ A) \/ (N ~ B) then reconsider x = x as Element of G ; x * N meets A \/ B by A1, Th14; then ( x * N meets A or x * N meets B ) by XBOOLE_1:70; then ( x in N ~ A or x in N ~ B ) ; hence x in (N ~ A) \/ (N ~ B) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N ~ A) \/ (N ~ B) or x in N ~ (A \/ B) ) assume A2: x in (N ~ A) \/ (N ~ B) ; ::_thesis: x in N ~ (A \/ B) then reconsider x = x as Element of G ; ( x in N ~ A or x in N ~ B ) by A2, XBOOLE_0:def_3; then ( x * N meets A or x * N meets B ) by Th14; then x * N meets A \/ B by XBOOLE_1:70; hence x in N ~ (A \/ B) ; ::_thesis: verum end; theorem :: GROUP_11:20 for G being Group for A, B being non empty Subset of G for N being Subgroup of G holds N ` (A /\ B) = (N ` A) /\ (N ` B) proof let G be Group; ::_thesis: for A, B being non empty Subset of G for N being Subgroup of G holds N ` (A /\ B) = (N ` A) /\ (N ` B) let A, B be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ` (A /\ B) = (N ` A) /\ (N ` B) let N be Subgroup of G; ::_thesis: N ` (A /\ B) = (N ` A) /\ (N ` B) thus N ` (A /\ B) c= (N ` A) /\ (N ` B) :: according to XBOOLE_0:def_10 ::_thesis: (N ` A) /\ (N ` B) c= N ` (A /\ B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` (A /\ B) or x in (N ` A) /\ (N ` B) ) assume A1: x in N ` (A /\ B) ; ::_thesis: x in (N ` A) /\ (N ` B) then reconsider x = x as Element of G ; consider x1 being Element of G such that A2: ( x1 = x & x1 * N c= A /\ B ) by A1; ( x * N c= A & x * N c= B ) by A2, XBOOLE_1:18; then ( x in N ` A & x in N ` B ) ; hence x in (N ` A) /\ (N ` B) by XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N ` A) /\ (N ` B) or x in N ` (A /\ B) ) assume A3: x in (N ` A) /\ (N ` B) ; ::_thesis: x in N ` (A /\ B) then reconsider x = x as Element of G ; ( x in N ` A & x in N ` B ) by A3, XBOOLE_0:def_4; then ( x * N c= A & x * N c= B ) by Th12; then x * N c= A /\ B by XBOOLE_1:19; hence x in N ` (A /\ B) ; ::_thesis: verum end; theorem :: GROUP_11:21 for G being Group for A, B being non empty Subset of G for N being Subgroup of G st A c= B holds N ` A c= N ` B proof let G be Group; ::_thesis: for A, B being non empty Subset of G for N being Subgroup of G st A c= B holds N ` A c= N ` B let A, B be non empty Subset of G; ::_thesis: for N being Subgroup of G st A c= B holds N ` A c= N ` B let N be Subgroup of G; ::_thesis: ( A c= B implies N ` A c= N ` B ) assume A1: A c= B ; ::_thesis: N ` A c= N ` B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` A or x in N ` B ) assume A2: x in N ` A ; ::_thesis: x in N ` B then reconsider x = x as Element of G ; x * N c= A by A2, Th12; then x * N c= B by A1, XBOOLE_1:1; hence x in N ` B ; ::_thesis: verum end; theorem :: GROUP_11:22 for G being Group for A, B being non empty Subset of G for N being Subgroup of G st A c= B holds N ~ A c= N ~ B proof let G be Group; ::_thesis: for A, B being non empty Subset of G for N being Subgroup of G st A c= B holds N ~ A c= N ~ B let A, B be non empty Subset of G; ::_thesis: for N being Subgroup of G st A c= B holds N ~ A c= N ~ B let N be Subgroup of G; ::_thesis: ( A c= B implies N ~ A c= N ~ B ) assume A1: A c= B ; ::_thesis: N ~ A c= N ~ B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ A or x in N ~ B ) assume A2: x in N ~ A ; ::_thesis: x in N ~ B then reconsider x = x as Element of G ; x * N meets A by A2, Th14; then x * N meets B by A1, XBOOLE_1:63; hence x in N ~ B ; ::_thesis: verum end; theorem :: GROUP_11:23 for G being Group for A, B being non empty Subset of G for N being Subgroup of G holds (N ` A) \/ (N ` B) c= N ` (A \/ B) proof let G be Group; ::_thesis: for A, B being non empty Subset of G for N being Subgroup of G holds (N ` A) \/ (N ` B) c= N ` (A \/ B) let A, B be non empty Subset of G; ::_thesis: for N being Subgroup of G holds (N ` A) \/ (N ` B) c= N ` (A \/ B) let N be Subgroup of G; ::_thesis: (N ` A) \/ (N ` B) c= N ` (A \/ B) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N ` A) \/ (N ` B) or x in N ` (A \/ B) ) assume A1: x in (N ` A) \/ (N ` B) ; ::_thesis: x in N ` (A \/ B) then reconsider x = x as Element of G ; percases ( x in N ` A or x in N ` B ) by A1, XBOOLE_0:def_3; suppose x in N ` A ; ::_thesis: x in N ` (A \/ B) then x * N c= A \/ B by Th12, XBOOLE_1:10; hence x in N ` (A \/ B) ; ::_thesis: verum end; suppose x in N ` B ; ::_thesis: x in N ` (A \/ B) then x * N c= A \/ B by Th12, XBOOLE_1:10; hence x in N ` (A \/ B) ; ::_thesis: verum end; end; end; theorem :: GROUP_11:24 for G being Group for A, B being non empty Subset of G for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B) proof let G be Group; ::_thesis: for A, B being non empty Subset of G for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B) let A, B be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B) let N be Subgroup of G; ::_thesis: N ~ (A \/ B) = (N ~ A) \/ (N ~ B) thus N ~ (A \/ B) c= (N ~ A) \/ (N ~ B) :: according to XBOOLE_0:def_10 ::_thesis: (N ~ A) \/ (N ~ B) c= N ~ (A \/ B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ (A \/ B) or x in (N ~ A) \/ (N ~ B) ) assume A1: x in N ~ (A \/ B) ; ::_thesis: x in (N ~ A) \/ (N ~ B) then reconsider x = x as Element of G ; x * N meets A \/ B by A1, Th14; then ( x * N meets A or x * N meets B ) by XBOOLE_1:70; then ( x in N ~ A or x in N ~ B ) ; hence x in (N ~ A) \/ (N ~ B) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N ~ A) \/ (N ~ B) or x in N ~ (A \/ B) ) assume A2: x in (N ~ A) \/ (N ~ B) ; ::_thesis: x in N ~ (A \/ B) then reconsider x = x as Element of G ; ( x in N ~ A or x in N ~ B ) by A2, XBOOLE_0:def_3; then ( x * N meets A or x * N meets B ) by Th14; then x * N meets A \/ B by XBOOLE_1:70; hence x in N ~ (A \/ B) ; ::_thesis: verum end; theorem Th25: :: GROUP_11:25 for G being Group for A being non empty Subset of G for N, H being Subgroup of G st N is Subgroup of H holds H ` A c= N ` A proof let G be Group; ::_thesis: for A being non empty Subset of G for N, H being Subgroup of G st N is Subgroup of H holds H ` A c= N ` A let A be non empty Subset of G; ::_thesis: for N, H being Subgroup of G st N is Subgroup of H holds H ` A c= N ` A let N, H be Subgroup of G; ::_thesis: ( N is Subgroup of H implies H ` A c= N ` A ) assume A1: N is Subgroup of H ; ::_thesis: H ` A c= N ` A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H ` A or x in N ` A ) assume A2: x in H ` A ; ::_thesis: x in N ` A then reconsider x = x as Element of G ; A3: x * N c= x * H by A1, GROUP_3:6; x * H c= A by A2, Th12; then x * N c= A by A3, XBOOLE_1:1; hence x in N ` A ; ::_thesis: verum end; theorem Th26: :: GROUP_11:26 for G being Group for A being non empty Subset of G for N, H being Subgroup of G st N is Subgroup of H holds N ~ A c= H ~ A proof let G be Group; ::_thesis: for A being non empty Subset of G for N, H being Subgroup of G st N is Subgroup of H holds N ~ A c= H ~ A let A be non empty Subset of G; ::_thesis: for N, H being Subgroup of G st N is Subgroup of H holds N ~ A c= H ~ A let N, H be Subgroup of G; ::_thesis: ( N is Subgroup of H implies N ~ A c= H ~ A ) assume A1: N is Subgroup of H ; ::_thesis: N ~ A c= H ~ A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ A or x in H ~ A ) assume A2: x in N ~ A ; ::_thesis: x in H ~ A then reconsider x = x as Element of G ; x * N meets A by A2, Th14; then x * H meets A by A1, GROUP_3:6, XBOOLE_1:63; hence x in H ~ A ; ::_thesis: verum end; theorem :: GROUP_11:27 for G being Group for A, B being non empty Subset of G for N being normal Subgroup of G holds (N ` A) * (N ` B) c= N ` (A * B) proof let G be Group; ::_thesis: for A, B being non empty Subset of G for N being normal Subgroup of G holds (N ` A) * (N ` B) c= N ` (A * B) let A, B be non empty Subset of G; ::_thesis: for N being normal Subgroup of G holds (N ` A) * (N ` B) c= N ` (A * B) let N be normal Subgroup of G; ::_thesis: (N ` A) * (N ` B) c= N ` (A * B) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N ` A) * (N ` B) or x in N ` (A * B) ) assume A1: x in (N ` A) * (N ` B) ; ::_thesis: x in N ` (A * B) then reconsider x = x as Element of G ; consider x1, x2 being Element of G such that A2: ( x = x1 * x2 & x1 in N ` A & x2 in N ` B ) by A1; ( x1 * N c= A & x2 * N c= B ) by A2, Th12; then (x1 * N) * (x2 * N) c= A * B by GROUP_3:4; then (x1 * x2) * N c= A * B by Th1; hence x in N ` (A * B) by A2; ::_thesis: verum end; theorem Th28: :: GROUP_11:28 for G being Group for A, B being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ~ (A * B) holds x * N meets A * B proof let G be Group; ::_thesis: for A, B being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ~ (A * B) holds x * N meets A * B let A, B be non empty Subset of G; ::_thesis: for N being Subgroup of G for x being Element of G st x in N ~ (A * B) holds x * N meets A * B let N be Subgroup of G; ::_thesis: for x being Element of G st x in N ~ (A * B) holds x * N meets A * B let x be Element of G; ::_thesis: ( x in N ~ (A * B) implies x * N meets A * B ) assume x in N ~ (A * B) ; ::_thesis: x * N meets A * B then consider x1 being Element of G such that A1: ( x = x1 & x1 * N meets A * B ) ; thus x * N meets A * B by A1; ::_thesis: verum end; theorem :: GROUP_11:29 for G being Group for A, B being non empty Subset of G for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = N ~ (A * B) proof let G be Group; ::_thesis: for A, B being non empty Subset of G for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = N ~ (A * B) let A, B be non empty Subset of G; ::_thesis: for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = N ~ (A * B) let N be normal Subgroup of G; ::_thesis: (N ~ A) * (N ~ B) = N ~ (A * B) thus (N ~ A) * (N ~ B) c= N ~ (A * B) :: according to XBOOLE_0:def_10 ::_thesis: N ~ (A * B) c= (N ~ A) * (N ~ B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N ~ A) * (N ~ B) or x in N ~ (A * B) ) assume A1: x in (N ~ A) * (N ~ B) ; ::_thesis: x in N ~ (A * B) then reconsider x = x as Element of G ; consider x1, x2 being Element of G such that A2: ( x = x1 * x2 & x1 in N ~ A & x2 in N ~ B ) by A1; A3: x1 * N meets A by A2, Th14; A4: x2 * N meets B by A2, Th14; consider x19 being set such that A5: ( x19 in x1 * N & x19 in A ) by A3, XBOOLE_0:3; consider x29 being set such that A6: ( x29 in x2 * N & x29 in B ) by A4, XBOOLE_0:3; reconsider x19 = x19 as Element of G by A5; reconsider x29 = x29 as Element of G by A6; A7: x19 * x29 in A * B by A5, A6; x19 * x29 in (x1 * N) * (x2 * N) by A5, A6; then (x1 * N) * (x2 * N) meets A * B by A7, XBOOLE_0:3; then (x1 * x2) * N meets A * B by Th1; hence x in N ~ (A * B) by A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ (A * B) or x in (N ~ A) * (N ~ B) ) assume A8: x in N ~ (A * B) ; ::_thesis: x in (N ~ A) * (N ~ B) then reconsider x = x as Element of G ; x * N meets A * B by A8, Th28; then consider x1 being set such that A9: ( x1 in x * N & x1 in A * B ) by XBOOLE_0:3; reconsider x1 = x1 as Element of G by A9; consider y1, y2 being Element of G such that A10: ( x1 = y1 * y2 & y1 in A & y2 in B ) by A9; x * N = (y1 * y2) * N by A9, A10, Th2 .= (y1 * N) * (y2 * N) by Th1 ; then x in (y1 * N) * (y2 * N) by GROUP_2:108; then consider g1, g2 being Element of G such that A11: ( x = g1 * g2 & g1 in y1 * N & g2 in y2 * N ) ; ( y1 * N = g1 * N & y2 * N = g2 * N ) by A11, Th2; then ( y1 in g1 * N & y2 in g2 * N ) by GROUP_2:108; then ( g1 * N meets A & g2 * N meets B ) by A10, XBOOLE_0:3; then ( g1 in N ~ A & g2 in N ~ B ) ; hence x in (N ~ A) * (N ~ B) by A11; ::_thesis: verum end; theorem Th30: :: GROUP_11:30 for G being Group for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ~ (N ` (N ~ A)) holds x * N meets N ` (N ~ A) proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ~ (N ` (N ~ A)) holds x * N meets N ` (N ~ A) let A be non empty Subset of G; ::_thesis: for N being Subgroup of G for x being Element of G st x in N ~ (N ` (N ~ A)) holds x * N meets N ` (N ~ A) let N be Subgroup of G; ::_thesis: for x being Element of G st x in N ~ (N ` (N ~ A)) holds x * N meets N ` (N ~ A) let x be Element of G; ::_thesis: ( x in N ~ (N ` (N ~ A)) implies x * N meets N ` (N ~ A) ) assume x in N ~ (N ` (N ~ A)) ; ::_thesis: x * N meets N ` (N ~ A) then ex x1 being Element of G st ( x = x1 & x1 * N meets N ` (N ~ A) ) ; hence x * N meets N ` (N ~ A) ; ::_thesis: verum end; theorem Th31: :: GROUP_11:31 for G being Group for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ` (N ~ A) holds x * N c= N ~ A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ` (N ~ A) holds x * N c= N ~ A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G for x being Element of G st x in N ` (N ~ A) holds x * N c= N ~ A let N be Subgroup of G; ::_thesis: for x being Element of G st x in N ` (N ~ A) holds x * N c= N ~ A let x be Element of G; ::_thesis: ( x in N ` (N ~ A) implies x * N c= N ~ A ) assume x in N ` (N ~ A) ; ::_thesis: x * N c= N ~ A then ex x1 being Element of G st ( x1 = x & x1 * N c= N ~ A ) ; hence x * N c= N ~ A ; ::_thesis: verum end; theorem Th32: :: GROUP_11:32 for G being Group for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ~ (N ~ A) holds x * N meets N ~ A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ~ (N ~ A) holds x * N meets N ~ A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G for x being Element of G st x in N ~ (N ~ A) holds x * N meets N ~ A let N be Subgroup of G; ::_thesis: for x being Element of G st x in N ~ (N ~ A) holds x * N meets N ~ A let x be Element of G; ::_thesis: ( x in N ~ (N ~ A) implies x * N meets N ~ A ) assume x in N ~ (N ~ A) ; ::_thesis: x * N meets N ~ A then ex x1 being Element of G st ( x = x1 & x1 * N meets N ~ A ) ; hence x * N meets N ~ A ; ::_thesis: verum end; theorem Th33: :: GROUP_11:33 for G being Group for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ~ (N ` A) holds x * N meets N ` A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ~ (N ` A) holds x * N meets N ` A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G for x being Element of G st x in N ~ (N ` A) holds x * N meets N ` A let N be Subgroup of G; ::_thesis: for x being Element of G st x in N ~ (N ` A) holds x * N meets N ` A let x be Element of G; ::_thesis: ( x in N ~ (N ` A) implies x * N meets N ` A ) assume x in N ~ (N ` A) ; ::_thesis: x * N meets N ` A then ex x1 being Element of G st ( x = x1 & x1 * N meets N ` A ) ; hence x * N meets N ` A ; ::_thesis: verum end; theorem Th34: :: GROUP_11:34 for G being Group for A being non empty Subset of G for N being Subgroup of G holds N ` (N ` A) = N ` A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds N ` (N ` A) = N ` A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ` (N ` A) = N ` A let N be Subgroup of G; ::_thesis: N ` (N ` A) = N ` A thus N ` (N ` A) c= N ` A :: according to XBOOLE_0:def_10 ::_thesis: N ` A c= N ` (N ` A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` (N ` A) or x in N ` A ) assume x in N ` (N ` A) ; ::_thesis: x in N ` A then consider y being Element of G such that A1: ( y = x & y * N c= N ` A ) ; y in y * N by GROUP_2:108; hence x in N ` A by A1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` A or x in N ` (N ` A) ) assume A2: x in N ` A ; ::_thesis: x in N ` (N ` A) then reconsider x9 = x as Element of G ; A3: x9 * N c= A by A2, Th12; x9 * N c= N ` A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x9 * N or y in N ` A ) assume A4: y in x9 * N ; ::_thesis: y in N ` A then reconsider y9 = y as Element of G ; x9 * N = y9 * N by A4, Th2; hence y in N ` A by A3; ::_thesis: verum end; hence x in N ` (N ` A) ; ::_thesis: verum end; theorem Th35: :: GROUP_11:35 for G being Group for A being non empty Subset of G for N being Subgroup of G holds N ~ A = N ~ (N ~ A) proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds N ~ A = N ~ (N ~ A) let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ~ A = N ~ (N ~ A) let N be Subgroup of G; ::_thesis: N ~ A = N ~ (N ~ A) thus N ~ A c= N ~ (N ~ A) :: according to XBOOLE_0:def_10 ::_thesis: N ~ (N ~ A) c= N ~ A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ A or x in N ~ (N ~ A) ) assume A1: x in N ~ A ; ::_thesis: x in N ~ (N ~ A) then reconsider x = x as Element of G ; x in x * N by GROUP_2:108; then x * N meets N ~ A by A1, XBOOLE_0:3; hence x in N ~ (N ~ A) ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ (N ~ A) or x in N ~ A ) assume A2: x in N ~ (N ~ A) ; ::_thesis: x in N ~ A then reconsider x9 = x as Element of G ; x9 * N meets N ~ A by A2, Th32; then consider y being set such that A3: ( y in x9 * N & y in N ~ A ) by XBOOLE_0:3; reconsider y9 = y as Element of G by A3; A4: y9 * N meets A by A3, Th14; y9 * N = x9 * N by A3, Th2; hence x in N ~ A by A4; ::_thesis: verum end; theorem :: GROUP_11:36 for G being Group for A being non empty Subset of G for N being Subgroup of G holds N ` (N ` A) c= N ~ (N ~ A) proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds N ` (N ` A) c= N ~ (N ~ A) let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ` (N ` A) c= N ~ (N ~ A) let N be Subgroup of G; ::_thesis: N ` (N ` A) c= N ~ (N ~ A) N ` A c= N ~ A by Th18; then N ` (N ` A) c= N ~ A by Th34; hence N ` (N ` A) c= N ~ (N ~ A) by Th35; ::_thesis: verum end; theorem :: GROUP_11:37 for G being Group for A being non empty Subset of G for N being Subgroup of G holds N ~ (N ` A) c= A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds N ~ (N ` A) c= A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ~ (N ` A) c= A let N be Subgroup of G; ::_thesis: N ~ (N ` A) c= A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ (N ` A) or x in A ) assume A1: x in N ~ (N ` A) ; ::_thesis: x in A then reconsider x9 = x as Element of G ; x9 * N meets N ` A by A1, Th33; then consider y being set such that A2: ( y in x9 * N & y in N ` A ) by XBOOLE_0:3; reconsider y9 = y as Element of G by A2; y9 * N c= A by A2, Th12; then A3: x9 * N c= A by A2, Th2; x9 in x9 * N by GROUP_2:108; hence x in A by A3; ::_thesis: verum end; theorem :: GROUP_11:38 for G being Group for A being non empty Subset of G for N being Subgroup of G holds N ` (N ~ (N ` A)) = N ` A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds N ` (N ~ (N ` A)) = N ` A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ` (N ~ (N ` A)) = N ` A let N be Subgroup of G; ::_thesis: N ` (N ~ (N ` A)) = N ` A thus N ` (N ~ (N ` A)) c= N ` A :: according to XBOOLE_0:def_10 ::_thesis: N ` A c= N ` (N ~ (N ` A)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` (N ~ (N ` A)) or x in N ` A ) assume x in N ` (N ~ (N ` A)) ; ::_thesis: x in N ` A then consider x1 being Element of G such that A1: ( x1 = x & x1 * N c= N ~ (N ` A) ) ; x1 in x1 * N by GROUP_2:108; then x1 * N meets N ` A by A1, Th33; then consider y being set such that A2: ( y in x1 * N & y in N ` A ) by XBOOLE_0:3; reconsider y = y as Element of G by A2; y * N c= A by A2, Th12; then x1 * N c= A by A2, Th2; hence x in N ` A by A1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` A or x in N ` (N ~ (N ` A)) ) assume A3: x in N ` A ; ::_thesis: x in N ` (N ~ (N ` A)) then reconsider x = x as Element of G ; x * N c= N ~ (N ` A) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x * N or y in N ~ (N ` A) ) assume A4: y in x * N ; ::_thesis: y in N ~ (N ` A) then reconsider y = y as Element of G ; y * N = x * N by A4, Th2; then x in y * N by GROUP_2:108; then y * N meets N ` A by A3, XBOOLE_0:3; hence y in N ~ (N ` A) ; ::_thesis: verum end; hence x in N ` (N ~ (N ` A)) ; ::_thesis: verum end; theorem Th39: :: GROUP_11:39 for G being Group for A being non empty Subset of G for N being Subgroup of G st A c= N ` (N ~ A) holds N ~ A c= N ~ (N ` (N ~ A)) proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G st A c= N ` (N ~ A) holds N ~ A c= N ~ (N ` (N ~ A)) let A be non empty Subset of G; ::_thesis: for N being Subgroup of G st A c= N ` (N ~ A) holds N ~ A c= N ~ (N ` (N ~ A)) let N be Subgroup of G; ::_thesis: ( A c= N ` (N ~ A) implies N ~ A c= N ~ (N ` (N ~ A)) ) assume A1: A c= N ` (N ~ A) ; ::_thesis: N ~ A c= N ~ (N ` (N ~ A)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ A or x in N ~ (N ` (N ~ A)) ) assume A2: x in N ~ A ; ::_thesis: x in N ~ (N ` (N ~ A)) then reconsider x = x as Element of G ; x * N meets A by A2, Th14; then x * N meets N ` (N ~ A) by A1, XBOOLE_1:63; hence x in N ~ (N ` (N ~ A)) ; ::_thesis: verum end; theorem :: GROUP_11:40 for G being Group for A being non empty Subset of G for N being Subgroup of G holds N ~ (N ` (N ~ A)) = N ~ A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds N ~ (N ` (N ~ A)) = N ~ A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ~ (N ` (N ~ A)) = N ~ A let N be Subgroup of G; ::_thesis: N ~ (N ` (N ~ A)) = N ~ A thus N ~ (N ` (N ~ A)) c= N ~ A :: according to XBOOLE_0:def_10 ::_thesis: N ~ A c= N ~ (N ` (N ~ A)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ (N ` (N ~ A)) or x in N ~ A ) assume A1: x in N ~ (N ` (N ~ A)) ; ::_thesis: x in N ~ A then reconsider x = x as Element of G ; x * N meets N ` (N ~ A) by A1, Th30; then consider y being set such that A2: ( y in x * N & y in N ` (N ~ A) ) by XBOOLE_0:3; reconsider y = y as Element of G by A2; y * N c= N ~ A by A2, Th31; then A3: x * N c= N ~ A by A2, Th2; x in x * N by GROUP_2:108; hence x in N ~ A by A3; ::_thesis: verum end; thus N ~ A c= N ~ (N ` (N ~ A)) ::_thesis: verum proof A c= N ` (N ~ A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in N ` (N ~ A) ) assume A4: x in A ; ::_thesis: x in N ` (N ~ A) then reconsider x = x as Element of G ; x * N c= N ~ A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x * N or y in N ~ A ) assume A5: y in x * N ; ::_thesis: y in N ~ A then reconsider y = y as Element of G ; y * N = x * N by A5, Th2; then x in y * N by GROUP_2:108; then y * N meets A by A4, XBOOLE_0:3; hence y in N ~ A ; ::_thesis: verum end; hence x in N ` (N ~ A) ; ::_thesis: verum end; hence N ~ A c= N ~ (N ` (N ~ A)) by Th39; ::_thesis: verum end; end; theorem Th41: :: GROUP_11:41 for G being Group for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ` (N ` A) holds x * N c= N ` A proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G for x being Element of G st x in N ` (N ` A) holds x * N c= N ` A let A be non empty Subset of G; ::_thesis: for N being Subgroup of G for x being Element of G st x in N ` (N ` A) holds x * N c= N ` A let N be Subgroup of G; ::_thesis: for x being Element of G st x in N ` (N ` A) holds x * N c= N ` A let x be Element of G; ::_thesis: ( x in N ` (N ` A) implies x * N c= N ` A ) assume x in N ` (N ` A) ; ::_thesis: x * N c= N ` A then ex x1 being Element of G st ( x1 = x & x1 * N c= N ` A ) ; hence x * N c= N ` A ; ::_thesis: verum end; theorem :: GROUP_11:42 for G being Group for A being non empty Subset of G for N being Subgroup of G holds N ` (N ` A) = N ~ (N ` A) proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds N ` (N ` A) = N ~ (N ` A) let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ` (N ` A) = N ~ (N ` A) let N be Subgroup of G; ::_thesis: N ` (N ` A) = N ~ (N ` A) thus N ` (N ` A) c= N ~ (N ` A) :: according to XBOOLE_0:def_10 ::_thesis: N ~ (N ` A) c= N ` (N ` A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` (N ` A) or x in N ~ (N ` A) ) assume A1: x in N ` (N ` A) ; ::_thesis: x in N ~ (N ` A) then reconsider x = x as Element of G ; A2: x * N c= N ` A by A1, Th41; x in x * N by GROUP_2:108; then x * N meets N ` A by A2, XBOOLE_0:3; hence x in N ~ (N ` A) ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ (N ` A) or x in N ` (N ` A) ) assume A3: x in N ~ (N ` A) ; ::_thesis: x in N ` (N ` A) then reconsider x = x as Element of G ; x * N meets N ` A by A3, Th33; then consider z being set such that A4: ( z in x * N & z in N ` A ) by XBOOLE_0:3; reconsider z = z as Element of G by A4; z * N c= A by A4, Th12; then A5: x * N c= A by A4, Th2; x * N c= N ` A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x * N or y in N ` A ) assume A6: y in x * N ; ::_thesis: y in N ` A then reconsider y = y as Element of G ; x * N = y * N by A6, Th2; hence y in N ` A by A5; ::_thesis: verum end; hence x in N ` (N ` A) ; ::_thesis: verum end; theorem :: GROUP_11:43 for G being Group for A being non empty Subset of G for N being Subgroup of G holds N ~ (N ~ A) = N ` (N ~ A) proof let G be Group; ::_thesis: for A being non empty Subset of G for N being Subgroup of G holds N ~ (N ~ A) = N ` (N ~ A) let A be non empty Subset of G; ::_thesis: for N being Subgroup of G holds N ~ (N ~ A) = N ` (N ~ A) let N be Subgroup of G; ::_thesis: N ~ (N ~ A) = N ` (N ~ A) thus N ~ (N ~ A) c= N ` (N ~ A) :: according to XBOOLE_0:def_10 ::_thesis: N ` (N ~ A) c= N ~ (N ~ A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ (N ~ A) or x in N ` (N ~ A) ) assume A1: x in N ~ (N ~ A) ; ::_thesis: x in N ` (N ~ A) then reconsider x = x as Element of G ; x * N meets N ~ A by A1, Th32; then consider z being set such that A2: ( z in x * N & z in N ~ A ) by XBOOLE_0:3; reconsider z = z as Element of G by A2; z * N meets A by A2, Th14; then A3: x * N meets A by A2, Th2; x * N c= N ~ A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x * N or y in N ~ A ) assume A4: y in x * N ; ::_thesis: y in N ~ A then reconsider y = y as Element of G ; x * N = y * N by A4, Th2; hence y in N ~ A by A3; ::_thesis: verum end; hence x in N ` (N ~ A) ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` (N ~ A) or x in N ~ (N ~ A) ) assume A5: x in N ` (N ~ A) ; ::_thesis: x in N ~ (N ~ A) then reconsider x = x as Element of G ; A6: x * N c= N ~ A by A5, Th31; x in x * N by GROUP_2:108; then x * N meets N ~ A by A6, XBOOLE_0:3; hence x in N ~ (N ~ A) ; ::_thesis: verum end; theorem :: GROUP_11:44 for G being Group for A being non empty Subset of G for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds N ~ A c= (N1 ~ A) /\ (N2 ~ A) proof let G be Group; ::_thesis: for A being non empty Subset of G for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds N ~ A c= (N1 ~ A) /\ (N2 ~ A) let A be non empty Subset of G; ::_thesis: for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds N ~ A c= (N1 ~ A) /\ (N2 ~ A) let N, N1, N2 be Subgroup of G; ::_thesis: ( N = N1 /\ N2 implies N ~ A c= (N1 ~ A) /\ (N2 ~ A) ) assume N = N1 /\ N2 ; ::_thesis: N ~ A c= (N1 ~ A) /\ (N2 ~ A) then A1: ( N is Subgroup of N1 & N is Subgroup of N2 ) by GROUP_2:88; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ A or x in (N1 ~ A) /\ (N2 ~ A) ) assume A2: x in N ~ A ; ::_thesis: x in (N1 ~ A) /\ (N2 ~ A) ( N ~ A c= N1 ~ A & N ~ A c= N2 ~ A ) by A1, Th26; hence x in (N1 ~ A) /\ (N2 ~ A) by A2, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: GROUP_11:45 for G being Group for A being non empty Subset of G for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds (N1 ` A) /\ (N2 ` A) c= N ` A proof let G be Group; ::_thesis: for A being non empty Subset of G for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds (N1 ` A) /\ (N2 ` A) c= N ` A let A be non empty Subset of G; ::_thesis: for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds (N1 ` A) /\ (N2 ` A) c= N ` A let N, N1, N2 be Subgroup of G; ::_thesis: ( N = N1 /\ N2 implies (N1 ` A) /\ (N2 ` A) c= N ` A ) assume N = N1 /\ N2 ; ::_thesis: (N1 ` A) /\ (N2 ` A) c= N ` A then A1: ( N is Subgroup of N1 & N is Subgroup of N2 ) by GROUP_2:88; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N1 ` A) /\ (N2 ` A) or x in N ` A ) assume x in (N1 ` A) /\ (N2 ` A) ; ::_thesis: x in N ` A then A2: ( x in N1 ` A & x in N2 ` A ) by XBOOLE_0:def_4; ( N1 ` A c= N ` A & N2 ` A c= N ` A ) by A1, Th25; hence x in N ` A by A2; ::_thesis: verum end; theorem :: GROUP_11:46 for G being Group for A being non empty Subset of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) ) proof let G be Group; ::_thesis: for A being non empty Subset of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) ) let A be non empty Subset of G; ::_thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) ) let N1, N2 be strict normal Subgroup of G; ::_thesis: ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) ) consider N being strict normal Subgroup of G such that A1: the carrier of N = N1 * N2 by Th8; ( N1 is Subgroup of N & N2 is Subgroup of N ) by A1, Th9; then A2: ( N ` A c= N1 ` A & N ` A c= N2 ` A ) by Th25; N ` A c= (N1 ` A) /\ (N2 ` A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` A or x in (N1 ` A) /\ (N2 ` A) ) assume x in N ` A ; ::_thesis: x in (N1 ` A) /\ (N2 ` A) hence x in (N1 ` A) /\ (N2 ` A) by A2, XBOOLE_0:def_4; ::_thesis: verum end; hence ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) ) by A1; ::_thesis: verum end; theorem :: GROUP_11:47 for G being Group for A being non empty Subset of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ A) \/ (N2 ~ A) c= N ~ A ) proof let G be Group; ::_thesis: for A being non empty Subset of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ A) \/ (N2 ~ A) c= N ~ A ) let A be non empty Subset of G; ::_thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ A) \/ (N2 ~ A) c= N ~ A ) let N1, N2 be strict normal Subgroup of G; ::_thesis: ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ A) \/ (N2 ~ A) c= N ~ A ) consider N being strict normal Subgroup of G such that A1: the carrier of N = N1 * N2 by Th8; ( N1 is Subgroup of N & N2 is Subgroup of N ) by A1, Th9; then A2: ( N1 ~ A c= N ~ A & N2 ~ A c= N ~ A ) by Th26; (N1 ~ A) \/ (N2 ~ A) c= N ~ A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N1 ~ A) \/ (N2 ~ A) or x in N ~ A ) assume x in (N1 ~ A) \/ (N2 ~ A) ; ::_thesis: x in N ~ A then ( x in N1 ~ A or x in N2 ~ A ) by XBOOLE_0:def_3; hence x in N ~ A by A2; ::_thesis: verum end; hence ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ A) \/ (N2 ~ A) c= N ~ A ) by A1; ::_thesis: verum end; theorem :: GROUP_11:48 for G being Group for A being non empty Subset of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) ) proof let G be Group; ::_thesis: for A being non empty Subset of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) ) let A be non empty Subset of G; ::_thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) ) let N1, N2 be strict normal Subgroup of G; ::_thesis: ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) ) consider N being strict normal Subgroup of G such that A1: the carrier of N = N1 * N2 by Th8; N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ A or x in ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) ) assume A2: x in N ~ A ; ::_thesis: x in ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) then reconsider x = x as Element of G ; x * N meets A by A2, Th14; then consider x1 being set such that A3: ( x1 in x * N & x1 in A ) by XBOOLE_0:3; reconsider x1 = x1 as Element of G by A3; consider y being Element of G such that A4: ( x1 = x * y & y in N ) by A3, GROUP_2:103; A5: y in N1 * N2 by A1, A4, STRUCT_0:def_5; then consider a, b being Element of G such that A6: ( y = a * b & a in N1 & b in N2 ) by Th6; A7: x1 = (x * a) * b by A4, A6, GROUP_1:def_3; a in carr N1 by A6, STRUCT_0:def_5; then A8: (x * a) * b in (x * N1) * b by GROUP_8:15; (x * N1) * b = x * (N1 * b) by GROUP_2:106 .= x * (b * N1) by GROUP_3:117 .= (x * b) * N1 by GROUP_2:105 ; then (x * b) * N1 meets A by A3, A7, A8, XBOOLE_0:3; then A9: x * b in N1 ~ A ; A10: (x * b) * (b ") = x * (b * (b ")) by GROUP_1:def_3 .= x * (1_ G) by GROUP_1:def_5 .= x by GROUP_1:def_4 ; b " in N2 by A6, GROUP_2:51; then A11: x in (N1 ~ A) * N2 by A9, A10, GROUP_2:94; y in N2 * N1 by A5, GROUP_3:125; then consider a, b being Element of G such that A12: ( y = a * b & a in N2 & b in N1 ) by Th6; A13: x1 = (x * a) * b by A4, A12, GROUP_1:def_3; a in carr N2 by A12, STRUCT_0:def_5; then A14: (x * a) * b in (x * N2) * b by GROUP_8:15; (x * N2) * b = x * (N2 * b) by GROUP_2:106 .= x * (b * N2) by GROUP_3:117 .= (x * b) * N2 by GROUP_2:105 ; then (x * b) * N2 meets A by A3, A13, A14, XBOOLE_0:3; then A15: x * b in N2 ~ A ; A16: (x * b) * (b ") = x * (b * (b ")) by GROUP_1:def_3 .= x * (1_ G) by GROUP_1:def_5 .= x by GROUP_1:def_4 ; b " in N1 by A12, GROUP_2:51; then x in (N2 ~ A) * N1 by A15, A16, GROUP_2:94; hence x in ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) by A11, XBOOLE_0:def_4; ::_thesis: verum end; hence ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) ) by A1; ::_thesis: verum end; definition let G be Group; let H, N be Subgroup of G; funcN ` H -> Subset of G equals :: GROUP_11:def 3 { x where x is Element of G : x * N c= carr H } ; coherence { x where x is Element of G : x * N c= carr H } is Subset of G proof { x where x is Element of G : x * N c= carr H } c= the carrier of G proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Element of G : x * N c= carr H } or y in the carrier of G ) assume y in { x where x is Element of G : x * N c= carr H } ; ::_thesis: y in the carrier of G then ex x being Element of G st ( y = x & x * N c= carr H ) ; hence y in the carrier of G ; ::_thesis: verum end; hence { x where x is Element of G : x * N c= carr H } is Subset of G ; ::_thesis: verum end; funcN ~ H -> Subset of G equals :: GROUP_11:def 4 { x where x is Element of G : x * N meets carr H } ; coherence { x where x is Element of G : x * N meets carr H } is Subset of G proof { x where x is Element of G : x * N meets carr H } c= the carrier of G proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Element of G : x * N meets carr H } or y in the carrier of G ) assume y in { x where x is Element of G : x * N meets carr H } ; ::_thesis: y in the carrier of G then ex x being Element of G st ( y = x & x * N meets carr H ) ; hence y in the carrier of G ; ::_thesis: verum end; hence { x where x is Element of G : x * N meets carr H } is Subset of G ; ::_thesis: verum end; end; :: deftheorem defines ` GROUP_11:def_3_:_ for G being Group for H, N being Subgroup of G holds N ` H = { x where x is Element of G : x * N c= carr H } ; :: deftheorem defines ~ GROUP_11:def_4_:_ for G being Group for H, N being Subgroup of G holds N ~ H = { x where x is Element of G : x * N meets carr H } ; theorem Th49: :: GROUP_11:49 for G being Group for N, H being Subgroup of G for x being Element of G st x in N ` H holds x * N c= carr H proof let G be Group; ::_thesis: for N, H being Subgroup of G for x being Element of G st x in N ` H holds x * N c= carr H let N, H be Subgroup of G; ::_thesis: for x being Element of G st x in N ` H holds x * N c= carr H let x be Element of G; ::_thesis: ( x in N ` H implies x * N c= carr H ) assume x in N ` H ; ::_thesis: x * N c= carr H then ex x1 being Element of G st ( x1 = x & x1 * N c= carr H ) ; hence x * N c= carr H ; ::_thesis: verum end; theorem :: GROUP_11:50 for G being Group for N, H being Subgroup of G for x being Element of G st x * N c= carr H holds x in N ` H ; theorem Th51: :: GROUP_11:51 for G being Group for N, H being Subgroup of G for x being Element of G st x in N ~ H holds x * N meets carr H proof let G be Group; ::_thesis: for N, H being Subgroup of G for x being Element of G st x in N ~ H holds x * N meets carr H let N, H be Subgroup of G; ::_thesis: for x being Element of G st x in N ~ H holds x * N meets carr H let x be Element of G; ::_thesis: ( x in N ~ H implies x * N meets carr H ) assume x in N ~ H ; ::_thesis: x * N meets carr H then ex x1 being Element of G st ( x = x1 & x1 * N meets carr H ) ; hence x * N meets carr H ; ::_thesis: verum end; theorem :: GROUP_11:52 for G being Group for N, H being Subgroup of G for x being Element of G st x * N meets carr H holds x in N ~ H ; theorem Th53: :: GROUP_11:53 for G being Group for N, H being Subgroup of G holds N ` H c= carr H proof let G be Group; ::_thesis: for N, H being Subgroup of G holds N ` H c= carr H let N, H be Subgroup of G; ::_thesis: N ` H c= carr H let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` H or x in carr H ) assume x in N ` H ; ::_thesis: x in carr H then consider y1 being Element of G such that A1: ( y1 = x & y1 * N c= carr H ) ; y1 in y1 * N by GROUP_2:108; hence x in carr H by A1; ::_thesis: verum end; theorem Th54: :: GROUP_11:54 for G being Group for H, N being Subgroup of G holds carr H c= N ~ H proof let G be Group; ::_thesis: for H, N being Subgroup of G holds carr H c= N ~ H let H, N be Subgroup of G; ::_thesis: carr H c= N ~ H let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in carr H or x in N ~ H ) assume x in carr H ; ::_thesis: x in N ~ H then reconsider x = x as Element of H ; reconsider x = x as Element of G by GROUP_2:42; x in x * N by GROUP_2:108; then x * N meets carr H by XBOOLE_0:3; hence x in N ~ H ; ::_thesis: verum end; theorem Th55: :: GROUP_11:55 for G being Group for N, H being Subgroup of G holds N ` H c= N ~ H proof let G be Group; ::_thesis: for N, H being Subgroup of G holds N ` H c= N ~ H let N, H be Subgroup of G; ::_thesis: N ` H c= N ~ H A1: N ` H c= carr H by Th53; carr H c= N ~ H by Th54; hence N ` H c= N ~ H by A1, XBOOLE_1:1; ::_thesis: verum end; theorem Th56: :: GROUP_11:56 for G being Group for H1, H2, N being Subgroup of G st H1 is Subgroup of H2 holds N ~ H1 c= N ~ H2 proof let G be Group; ::_thesis: for H1, H2, N being Subgroup of G st H1 is Subgroup of H2 holds N ~ H1 c= N ~ H2 let H1, H2, N be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 implies N ~ H1 c= N ~ H2 ) assume H1 is Subgroup of H2 ; ::_thesis: N ~ H1 c= N ~ H2 then A1: carr H1 c= carr H2 by GROUP_2:def_5; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ H1 or x in N ~ H2 ) assume A2: x in N ~ H1 ; ::_thesis: x in N ~ H2 then reconsider x = x as Element of G ; x * N meets carr H1 by A2, Th51; then x * N meets carr H2 by A1, XBOOLE_1:63; hence x in N ~ H2 ; ::_thesis: verum end; theorem Th57: :: GROUP_11:57 for G being Group for H, N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds N1 ~ H c= N2 ~ H proof let G be Group; ::_thesis: for H, N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds N1 ~ H c= N2 ~ H let H, N1, N2 be Subgroup of G; ::_thesis: ( N1 is Subgroup of N2 implies N1 ~ H c= N2 ~ H ) assume A1: N1 is Subgroup of N2 ; ::_thesis: N1 ~ H c= N2 ~ H let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 ~ H or x in N2 ~ H ) assume A2: x in N1 ~ H ; ::_thesis: x in N2 ~ H then reconsider x = x as Element of G ; x * N1 meets carr H by A2, Th51; then x * N2 meets carr H by A1, GROUP_3:6, XBOOLE_1:63; hence x in N2 ~ H ; ::_thesis: verum end; theorem :: GROUP_11:58 for G being Group for N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds N1 ~ N1 c= N2 ~ N2 proof let G be Group; ::_thesis: for N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds N1 ~ N1 c= N2 ~ N2 let N1, N2 be Subgroup of G; ::_thesis: ( N1 is Subgroup of N2 implies N1 ~ N1 c= N2 ~ N2 ) assume A1: N1 is Subgroup of N2 ; ::_thesis: N1 ~ N1 c= N2 ~ N2 then A2: N2 ~ N1 c= N2 ~ N2 by Th56; N1 ~ N1 c= N2 ~ N1 by A1, Th57; hence N1 ~ N1 c= N2 ~ N2 by A2, XBOOLE_1:1; ::_thesis: verum end; theorem Th59: :: GROUP_11:59 for G being Group for H1, H2, N being Subgroup of G st H1 is Subgroup of H2 holds N ` H1 c= N ` H2 proof let G be Group; ::_thesis: for H1, H2, N being Subgroup of G st H1 is Subgroup of H2 holds N ` H1 c= N ` H2 let H1, H2, N be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 implies N ` H1 c= N ` H2 ) assume H1 is Subgroup of H2 ; ::_thesis: N ` H1 c= N ` H2 then A1: carr H1 c= carr H2 by GROUP_2:def_5; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` H1 or x in N ` H2 ) assume A2: x in N ` H1 ; ::_thesis: x in N ` H2 then reconsider x = x as Element of G ; x * N c= carr H1 by A2, Th49; then x * N c= carr H2 by A1, XBOOLE_1:1; hence x in N ` H2 ; ::_thesis: verum end; theorem Th60: :: GROUP_11:60 for G being Group for H, N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds N2 ` H c= N1 ` H proof let G be Group; ::_thesis: for H, N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds N2 ` H c= N1 ` H let H, N1, N2 be Subgroup of G; ::_thesis: ( N1 is Subgroup of N2 implies N2 ` H c= N1 ` H ) assume A1: N1 is Subgroup of N2 ; ::_thesis: N2 ` H c= N1 ` H let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N2 ` H or x in N1 ` H ) assume A2: x in N2 ` H ; ::_thesis: x in N1 ` H then reconsider x = x as Element of G ; A3: x * N1 c= x * N2 by A1, GROUP_3:6; x * N2 c= carr H by A2, Th49; then x * N1 c= carr H by A3, XBOOLE_1:1; hence x in N1 ` H ; ::_thesis: verum end; theorem :: GROUP_11:61 for G being Group for N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds N2 ` N1 c= N1 ` N2 proof let G be Group; ::_thesis: for N1, N2 being Subgroup of G st N1 is Subgroup of N2 holds N2 ` N1 c= N1 ` N2 let N1, N2 be Subgroup of G; ::_thesis: ( N1 is Subgroup of N2 implies N2 ` N1 c= N1 ` N2 ) assume A1: N1 is Subgroup of N2 ; ::_thesis: N2 ` N1 c= N1 ` N2 then A2: N2 ` N1 c= N2 ` N2 by Th59; N2 ` N2 c= N1 ` N2 by A1, Th60; hence N2 ` N1 c= N1 ` N2 by A2, XBOOLE_1:1; ::_thesis: verum end; theorem :: GROUP_11:62 for G being Group for H1, H2 being Subgroup of G for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2) proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2) let H1, H2 be Subgroup of G; ::_thesis: for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2) let N be normal Subgroup of G; ::_thesis: (N ` H1) * (N ` H2) c= N ` (H1 * H2) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N ` H1) * (N ` H2) or x in N ` (H1 * H2) ) assume A1: x in (N ` H1) * (N ` H2) ; ::_thesis: x in N ` (H1 * H2) then reconsider x = x as Element of G ; consider x1, x2 being Element of G such that A2: ( x = x1 * x2 & x1 in N ` H1 & x2 in N ` H2 ) by A1; ( x1 * N c= carr H1 & x2 * N c= carr H2 ) by A2, Th49; then (x1 * N) * (x2 * N) c= (carr H1) * (carr H2) by GROUP_3:4; then (x1 * x2) * N c= (carr H1) * (carr H2) by Th1; hence x in N ` (H1 * H2) by A2; ::_thesis: verum end; theorem :: GROUP_11:63 for G being Group for H1, H2 being Subgroup of G for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2) proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2) let H1, H2 be Subgroup of G; ::_thesis: for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2) let N be normal Subgroup of G; ::_thesis: (N ~ H1) * (N ~ H2) = N ~ (H1 * H2) thus (N ~ H1) * (N ~ H2) c= N ~ (H1 * H2) :: according to XBOOLE_0:def_10 ::_thesis: N ~ (H1 * H2) c= (N ~ H1) * (N ~ H2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N ~ H1) * (N ~ H2) or x in N ~ (H1 * H2) ) assume A1: x in (N ~ H1) * (N ~ H2) ; ::_thesis: x in N ~ (H1 * H2) then reconsider x = x as Element of G ; consider x1, x2 being Element of G such that A2: ( x = x1 * x2 & x1 in N ~ H1 & x2 in N ~ H2 ) by A1; A3: x1 * N meets carr H1 by A2, Th51; A4: x2 * N meets carr H2 by A2, Th51; consider x19 being set such that A5: ( x19 in x1 * N & x19 in carr H1 ) by A3, XBOOLE_0:3; consider x29 being set such that A6: ( x29 in x2 * N & x29 in carr H2 ) by A4, XBOOLE_0:3; reconsider x19 = x19 as Element of G by A5; reconsider x29 = x29 as Element of G by A6; A7: x19 * x29 in (carr H1) * (carr H2) by A5, A6; x19 * x29 in (x1 * N) * (x2 * N) by A5, A6; then (x1 * N) * (x2 * N) meets (carr H1) * (carr H2) by A7, XBOOLE_0:3; then (x1 * x2) * N meets (carr H1) * (carr H2) by Th1; hence x in N ~ (H1 * H2) by A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ (H1 * H2) or x in (N ~ H1) * (N ~ H2) ) assume A8: x in N ~ (H1 * H2) ; ::_thesis: x in (N ~ H1) * (N ~ H2) then reconsider x = x as Element of G ; x * N meets (carr H1) * (carr H2) by A8, Th28; then consider x1 being set such that A9: ( x1 in x * N & x1 in (carr H1) * (carr H2) ) by XBOOLE_0:3; reconsider x1 = x1 as Element of G by A9; consider y1, y2 being Element of G such that A10: ( x1 = y1 * y2 & y1 in carr H1 & y2 in carr H2 ) by A9; x * N = (y1 * y2) * N by A9, A10, Th2 .= (y1 * N) * (y2 * N) by Th1 ; then x in (y1 * N) * (y2 * N) by GROUP_2:108; then consider g1, g2 being Element of G such that A11: ( x = g1 * g2 & g1 in y1 * N & g2 in y2 * N ) ; ( y1 * N = g1 * N & y2 * N = g2 * N ) by A11, Th2; then ( y1 in g1 * N & y2 in g2 * N ) by GROUP_2:108; then ( g1 * N meets carr H1 & g2 * N meets carr H2 ) by A10, XBOOLE_0:3; then ( g1 in N ~ H1 & g2 in N ~ H2 ) ; hence x in (N ~ H1) * (N ~ H2) by A11; ::_thesis: verum end; theorem :: GROUP_11:64 for G being Group for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds N ~ H c= (N1 ~ H) /\ (N2 ~ H) proof let G be Group; ::_thesis: for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds N ~ H c= (N1 ~ H) /\ (N2 ~ H) let H be Subgroup of G; ::_thesis: for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds N ~ H c= (N1 ~ H) /\ (N2 ~ H) let N, N1, N2 be Subgroup of G; ::_thesis: ( N = N1 /\ N2 implies N ~ H c= (N1 ~ H) /\ (N2 ~ H) ) assume N = N1 /\ N2 ; ::_thesis: N ~ H c= (N1 ~ H) /\ (N2 ~ H) then A1: ( N is Subgroup of N1 & N is Subgroup of N2 ) by GROUP_2:88; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ H or x in (N1 ~ H) /\ (N2 ~ H) ) assume A2: x in N ~ H ; ::_thesis: x in (N1 ~ H) /\ (N2 ~ H) ( N ~ H c= N1 ~ H & N ~ H c= N2 ~ H ) by A1, Th57; hence x in (N1 ~ H) /\ (N2 ~ H) by A2, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: GROUP_11:65 for G being Group for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds (N1 ` H) /\ (N2 ` H) c= N ` H proof let G be Group; ::_thesis: for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds (N1 ` H) /\ (N2 ` H) c= N ` H let H be Subgroup of G; ::_thesis: for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds (N1 ` H) /\ (N2 ` H) c= N ` H let N, N1, N2 be Subgroup of G; ::_thesis: ( N = N1 /\ N2 implies (N1 ` H) /\ (N2 ` H) c= N ` H ) assume N = N1 /\ N2 ; ::_thesis: (N1 ` H) /\ (N2 ` H) c= N ` H then A1: ( N is Subgroup of N1 & N is Subgroup of N2 ) by GROUP_2:88; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N1 ` H) /\ (N2 ` H) or x in N ` H ) assume x in (N1 ` H) /\ (N2 ` H) ; ::_thesis: x in N ` H then A2: ( x in N1 ` H & x in N2 ` H ) by XBOOLE_0:def_4; ( N1 ` H c= N ` H & N2 ` H c= N ` H ) by A1, Th60; hence x in N ` H by A2; ::_thesis: verum end; theorem :: GROUP_11:66 for G being Group for H being Subgroup of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ` H c= (N1 ` H) /\ (N2 ` H) ) proof let G be Group; ::_thesis: for H being Subgroup of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ` H c= (N1 ` H) /\ (N2 ` H) ) let H be Subgroup of G; ::_thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ` H c= (N1 ` H) /\ (N2 ` H) ) let N1, N2 be strict normal Subgroup of G; ::_thesis: ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ` H c= (N1 ` H) /\ (N2 ` H) ) consider N being strict normal Subgroup of G such that A1: the carrier of N = N1 * N2 by Th8; ( N1 is Subgroup of N & N2 is Subgroup of N ) by A1, Th9; then A2: ( N ` H c= N1 ` H & N ` H c= N2 ` H ) by Th60; N ` H c= (N1 ` H) /\ (N2 ` H) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ` H or x in (N1 ` H) /\ (N2 ` H) ) assume x in N ` H ; ::_thesis: x in (N1 ` H) /\ (N2 ` H) hence x in (N1 ` H) /\ (N2 ` H) by A2, XBOOLE_0:def_4; ::_thesis: verum end; hence ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ` H c= (N1 ` H) /\ (N2 ` H) ) by A1; ::_thesis: verum end; theorem :: GROUP_11:67 for G being Group for H being Subgroup of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ H) \/ (N2 ~ H) c= N ~ H ) proof let G be Group; ::_thesis: for H being Subgroup of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ H) \/ (N2 ~ H) c= N ~ H ) let H be Subgroup of G; ::_thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ H) \/ (N2 ~ H) c= N ~ H ) let N1, N2 be strict normal Subgroup of G; ::_thesis: ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ H) \/ (N2 ~ H) c= N ~ H ) consider N being strict normal Subgroup of G such that A1: the carrier of N = N1 * N2 by Th8; ( N1 is Subgroup of N & N2 is Subgroup of N ) by A1, Th9; then A2: ( N1 ~ H c= N ~ H & N2 ~ H c= N ~ H ) by Th57; (N1 ~ H) \/ (N2 ~ H) c= N ~ H proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N1 ~ H) \/ (N2 ~ H) or x in N ~ H ) assume x in (N1 ~ H) \/ (N2 ~ H) ; ::_thesis: x in N ~ H then ( x in N1 ~ H or x in N2 ~ H ) by XBOOLE_0:def_3; hence x in N ~ H by A2; ::_thesis: verum end; hence ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ H) \/ (N2 ~ H) c= N ~ H ) by A1; ::_thesis: verum end; theorem :: GROUP_11:68 for G being Group for H being Subgroup of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ` H) * (N2 ` H) c= N ` H ) proof let G be Group; ::_thesis: for H being Subgroup of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ` H) * (N2 ` H) c= N ` H ) let H be Subgroup of G; ::_thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ` H) * (N2 ` H) c= N ` H ) let N1, N2 be strict normal Subgroup of G; ::_thesis: ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ` H) * (N2 ` H) c= N ` H ) consider N being strict normal Subgroup of G such that A1: the carrier of N = N1 * N2 by Th8; (N1 ` H) * (N2 ` H) c= N ` H proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N1 ` H) * (N2 ` H) or x in N ` H ) assume A2: x in (N1 ` H) * (N2 ` H) ; ::_thesis: x in N ` H then reconsider x = x as Element of G ; consider a, b being Element of G such that A3: ( x = a * b & a in N1 ` H & b in N2 ` H ) by A2; ( a * N1 c= carr H & b * N2 c= carr H ) by A3, Th49; then (a * N1) * (b * N2) c= (carr H) * (carr H) by GROUP_3:4; then A4: (a * N1) * (b * N2) c= carr H by GROUP_2:76; (a * N1) * (b * N2) = (a * b) * N by A1, Th10; hence x in N ` H by A3, A4; ::_thesis: verum end; hence ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ` H) * (N2 ` H) c= N ` H ) by A1; ::_thesis: verum end; theorem :: GROUP_11:69 for G being Group for H being Subgroup of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H ) proof let G be Group; ::_thesis: for H being Subgroup of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H ) let H be Subgroup of G; ::_thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H ) let N1, N2 be strict normal Subgroup of G; ::_thesis: ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H ) consider N being strict normal Subgroup of G such that A1: the carrier of N = N1 * N2 by Th8; (N1 ~ H) * (N2 ~ H) c= N ~ H proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (N1 ~ H) * (N2 ~ H) or x in N ~ H ) assume A2: x in (N1 ~ H) * (N2 ~ H) ; ::_thesis: x in N ~ H then reconsider x = x as Element of G ; consider a, b being Element of G such that A3: ( x = a * b & a in N1 ~ H & b in N2 ~ H ) by A2; A4: a * N1 meets carr H by A3, Th51; A5: b * N2 meets carr H by A3, Th51; consider x1 being set such that A6: ( x1 in a * N1 & x1 in carr H ) by A4, XBOOLE_0:3; consider x2 being set such that A7: ( x2 in b * N2 & x2 in carr H ) by A5, XBOOLE_0:3; reconsider x1 = x1 as Element of G by A6; reconsider x2 = x2 as Element of G by A7; A8: x1 * x2 in (carr H) * (carr H) by A6, A7; A9: x1 * x2 in (a * N1) * (b * N2) by A6, A7; (carr H) * (carr H) = carr H by GROUP_2:76; then A10: (a * N1) * (b * N2) meets carr H by A8, A9, XBOOLE_0:3; (a * N1) * (b * N2) = (a * b) * N by A1, Th10; hence x in N ~ H by A3, A10; ::_thesis: verum end; hence ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H ) by A1; ::_thesis: verum end; theorem :: GROUP_11:70 for G being Group for H being Subgroup of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) ) proof let G be Group; ::_thesis: for H being Subgroup of G for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) ) let H be Subgroup of G; ::_thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) ) let N1, N2 be strict normal Subgroup of G; ::_thesis: ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) ) consider N being strict normal Subgroup of G such that A1: the carrier of N = N1 * N2 by Th8; N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N ~ H or x in ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) ) assume A2: x in N ~ H ; ::_thesis: x in ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) then reconsider x = x as Element of G ; x * N meets carr H by A2, Th51; then consider x1 being set such that A3: ( x1 in x * N & x1 in carr H ) by XBOOLE_0:3; reconsider x1 = x1 as Element of G by A3; consider y being Element of G such that A4: ( x1 = x * y & y in N ) by A3, GROUP_2:103; A5: y in N1 * N2 by A1, A4, STRUCT_0:def_5; then consider a, b being Element of G such that A6: ( y = a * b & a in N1 & b in N2 ) by Th6; A7: x1 = (x * a) * b by A4, A6, GROUP_1:def_3; a in carr N1 by A6, STRUCT_0:def_5; then A8: (x * a) * b in (x * N1) * b by GROUP_8:15; (x * N1) * b = x * (N1 * b) by GROUP_2:106 .= x * (b * N1) by GROUP_3:117 .= (x * b) * N1 by GROUP_2:105 ; then (x * b) * N1 meets carr H by A3, A7, A8, XBOOLE_0:3; then A9: x * b in N1 ~ H ; A10: (x * b) * (b ") = x * (b * (b ")) by GROUP_1:def_3 .= x * (1_ G) by GROUP_1:def_5 .= x by GROUP_1:def_4 ; b " in N2 by A6, GROUP_2:51; then A11: x in (N1 ~ H) * N2 by A9, A10, GROUP_2:94; y in N2 * N1 by A5, GROUP_3:125; then consider a, b being Element of G such that A12: ( y = a * b & a in N2 & b in N1 ) by Th6; A13: x1 = (x * a) * b by A4, A12, GROUP_1:def_3; a in carr N2 by A12, STRUCT_0:def_5; then A14: (x * a) * b in (x * N2) * b by GROUP_8:15; (x * N2) * b = x * (N2 * b) by GROUP_2:106 .= x * (b * N2) by GROUP_3:117 .= (x * b) * N2 by GROUP_2:105 ; then (x * b) * N2 meets carr H by A3, A13, A14, XBOOLE_0:3; then A15: x * b in N2 ~ H ; A16: (x * b) * (b ") = x * (b * (b ")) by GROUP_1:def_3 .= x * (1_ G) by GROUP_1:def_5 .= x by GROUP_1:def_4 ; b " in N1 by A12, GROUP_2:51; then x in (N2 ~ H) * N1 by A15, A16, GROUP_2:94; hence x in ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) by A11, XBOOLE_0:def_4; ::_thesis: verum end; hence ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) ) by A1; ::_thesis: verum end; theorem Th71: :: GROUP_11:71 for G being Group for H being Subgroup of G for N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H proof let G be Group; ::_thesis: for H being Subgroup of G for N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H let H be Subgroup of G; ::_thesis: for N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H let N be normal Subgroup of G; ::_thesis: ex M being strict Subgroup of G st the carrier of M = N ~ H A1: 1_ G in N ~ H proof 1_ G in H by GROUP_2:46; then A2: 1_ G in carr H by STRUCT_0:def_5; 1_ G in (1_ G) * N by GROUP_2:108; then (1_ G) * N meets carr H by A2, XBOOLE_0:3; hence 1_ G in N ~ H ; ::_thesis: verum end; A3: for x, y being Element of G st x in N ~ H & y in N ~ H holds x * y in N ~ H proof let x, y be Element of G; ::_thesis: ( x in N ~ H & y in N ~ H implies x * y in N ~ H ) assume that A4: x in N ~ H and A5: y in N ~ H ; ::_thesis: x * y in N ~ H consider a being Element of G such that A6: ( a in x * N & a in H ) by A4, Th51, Th3; consider b being Element of G such that A7: ( b in y * N & b in H ) by A5, Th51, Th3; ( (x * N) * (y * N) = (x * y) * N & (a * N) * (b * N) = (a * b) * N ) by Th1; then A8: a * b in (x * y) * N by A6, A7; a * b in H by A6, A7, GROUP_2:50; then a * b in carr H by STRUCT_0:def_5; then (x * y) * N meets carr H by A8, XBOOLE_0:3; hence x * y in N ~ H ; ::_thesis: verum end; for x being Element of G st x in N ~ H holds x " in N ~ H proof let x be Element of G; ::_thesis: ( x in N ~ H implies x " in N ~ H ) assume x in N ~ H ; ::_thesis: x " in N ~ H then consider a being Element of G such that A9: ( a in x * N & a in H ) by Th3, Th51; consider a1 being Element of G such that A10: ( a = x * a1 & a1 in N ) by A9, GROUP_2:103; A11: a1 " in N by A10, GROUP_2:51; a " = (a1 ") * (x ") by A10, GROUP_1:17; then a " in N * (x ") by A11, GROUP_2:104; then A12: a " in (x ") * N by GROUP_3:117; a " in H by A9, GROUP_2:51; then a " in carr H by STRUCT_0:def_5; then (x ") * N meets carr H by A12, XBOOLE_0:3; hence x " in N ~ H ; ::_thesis: verum end; hence ex M being strict Subgroup of G st the carrier of M = N ~ H by A1, A3, GROUP_2:52; ::_thesis: verum end; theorem Th72: :: GROUP_11:72 for G being Group for H being Subgroup of G for N being normal Subgroup of G st N is Subgroup of H holds ex M being strict Subgroup of G st the carrier of M = N ` H proof let G be Group; ::_thesis: for H being Subgroup of G for N being normal Subgroup of G st N is Subgroup of H holds ex M being strict Subgroup of G st the carrier of M = N ` H let H be Subgroup of G; ::_thesis: for N being normal Subgroup of G st N is Subgroup of H holds ex M being strict Subgroup of G st the carrier of M = N ` H let N be normal Subgroup of G; ::_thesis: ( N is Subgroup of H implies ex M being strict Subgroup of G st the carrier of M = N ` H ) assume A1: N is Subgroup of H ; ::_thesis: ex M being strict Subgroup of G st the carrier of M = N ` H A2: 1_ G in N ` H proof 1_ G in N by GROUP_2:46; then A3: (1_ G) * N = carr N by GROUP_2:113; carr N c= carr H by A1, GROUP_2:def_5; hence 1_ G in N ` H by A3; ::_thesis: verum end; A4: for x, y being Element of G st x in N ` H & y in N ` H holds x * y in N ` H proof let x, y be Element of G; ::_thesis: ( x in N ` H & y in N ` H implies x * y in N ` H ) assume ( x in N ` H & y in N ` H ) ; ::_thesis: x * y in N ` H then ( x * N c= carr H & y * N c= carr H ) by Th49; then A5: (x * N) * (y * N) c= (carr H) * (carr H) by GROUP_3:4; A6: (x * N) * (y * N) = (x * y) * N by Th1; (carr H) * (carr H) = carr H by GROUP_2:76; hence x * y in N ` H by A5, A6; ::_thesis: verum end; for x being Element of G st x in N ` H holds x " in N ` H proof let x be Element of G; ::_thesis: ( x in N ` H implies x " in N ` H ) assume x in N ` H ; ::_thesis: x " in N ` H then A7: x * N c= carr H by Th49; x in x * N by GROUP_2:108; then x in H by A7, STRUCT_0:def_5; then x " in H by GROUP_2:51; then A8: (x ") * H = carr H by GROUP_2:113; (x ") * N c= (x ") * H by A1, GROUP_3:6; hence x " in N ` H by A8; ::_thesis: verum end; hence ex M being strict Subgroup of G st the carrier of M = N ` H by A2, A4, GROUP_2:52; ::_thesis: verum end; theorem Th73: :: GROUP_11:73 for G being Group for H, N being normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N ~ H proof let G be Group; ::_thesis: for H, N being normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N ~ H let H, N be normal Subgroup of G; ::_thesis: ex M being strict normal Subgroup of G st the carrier of M = N ~ H consider M being strict Subgroup of G such that A1: the carrier of M = N ~ H by Th71; for x being Element of G holds x * M c= M * x proof let x be Element of G; ::_thesis: x * M c= M * x let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x * M or y in M * x ) assume A2: y in x * M ; ::_thesis: y in M * x then reconsider y = y as Element of G ; consider z being Element of G such that A3: ( y = x * z & z in M ) by A2, GROUP_2:103; z in the carrier of M by A3, STRUCT_0:def_5; then consider z9 being Element of G such that A4: ( z9 in z * N & z9 in H ) by Th3, A1, Th51; (x * z9) * (x ") in H by A4, Th4; then A5: (x * z9) * (x ") in carr H by STRUCT_0:def_5; A6: (x * z9) * (x ") in (x * (z * N)) * (x ") by A4, GROUP_8:15; (x * (z * N)) * (x ") = x * ((z * N) * (x ")) by GROUP_2:33 .= x * (z * (N * (x "))) by GROUP_2:33 .= x * (z * ((x ") * N)) by GROUP_3:117 .= x * ((z * (x ")) * N) by GROUP_2:32 .= (x * (z * (x "))) * N by GROUP_2:32 .= ((x * z) * (x ")) * N by GROUP_1:def_3 ; then ((x * z) * (x ")) * N meets carr H by A5, A6, XBOOLE_0:3; then (x * z) * (x ") in N ~ H ; then A7: (x * z) * (x ") in M by A1, STRUCT_0:def_5; ((x * z) * (x ")) * x = y by A3, GROUP_3:1; hence y in M * x by A7, GROUP_2:104; ::_thesis: verum end; then M is normal Subgroup of G by GROUP_3:118; hence ex M being strict normal Subgroup of G st the carrier of M = N ~ H by A1; ::_thesis: verum end; theorem Th74: :: GROUP_11:74 for G being Group for H, N being normal Subgroup of G st N is Subgroup of H holds ex M being strict normal Subgroup of G st the carrier of M = N ` H proof let G be Group; ::_thesis: for H, N being normal Subgroup of G st N is Subgroup of H holds ex M being strict normal Subgroup of G st the carrier of M = N ` H let H, N be normal Subgroup of G; ::_thesis: ( N is Subgroup of H implies ex M being strict normal Subgroup of G st the carrier of M = N ` H ) assume A1: N is Subgroup of H ; ::_thesis: ex M being strict normal Subgroup of G st the carrier of M = N ` H then consider M being strict Subgroup of G such that A2: the carrier of M = N ` H by Th72; for x being Element of G holds x * M c= M * x proof let x be Element of G; ::_thesis: x * M c= M * x let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x * M or y in M * x ) assume A3: y in x * M ; ::_thesis: y in M * x then reconsider y = y as Element of G ; consider z being Element of G such that A4: ( y = x * z & z in M ) by A3, GROUP_2:103; z in the carrier of M by A4, STRUCT_0:def_5; then A5: z * N c= carr H by A2, Th49; z in z * N by GROUP_2:108; then z in H by A5, STRUCT_0:def_5; then (x * z) * (x ") in H by Th4; then A6: ((x * z) * (x ")) * H = carr H by GROUP_2:113; ((x * z) * (x ")) * N c= ((x * z) * (x ")) * H by A1, GROUP_3:6; then (x * z) * (x ") in N ` H by A6; then A7: (x * z) * (x ") in M by A2, STRUCT_0:def_5; ((x * z) * (x ")) * x = y by A4, GROUP_3:1; hence y in M * x by A7, GROUP_2:104; ::_thesis: verum end; then M is normal Subgroup of G by GROUP_3:118; hence ex M being strict normal Subgroup of G st the carrier of M = N ` H by A2; ::_thesis: verum end; theorem Th75: :: GROUP_11:75 for G being Group for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N ) proof let G be Group; ::_thesis: for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N ) let N, N1 be normal Subgroup of G; ::_thesis: ( N1 is Subgroup of N implies ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N ) ) assume A1: N1 is Subgroup of N ; ::_thesis: ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N ) consider N2 being strict normal Subgroup of G such that A2: the carrier of N2 = N1 ~ N by Th73; consider N3 being strict normal Subgroup of G such that A3: the carrier of N3 = N1 ` N by A1, Th74; N3 is Subgroup of N2 by A2, A3, Th55, GROUP_2:57; then N2 ` N c= N3 ` N by Th60; hence ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N ) by A2, A3; ::_thesis: verum end; theorem Th76: :: GROUP_11:76 for G being Group for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ~ N c= N2 ~ N ) proof let G be Group; ::_thesis: for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ~ N c= N2 ~ N ) let N, N1 be normal Subgroup of G; ::_thesis: ( N1 is Subgroup of N implies ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ~ N c= N2 ~ N ) ) assume A1: N1 is Subgroup of N ; ::_thesis: ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ~ N c= N2 ~ N ) consider N2 being strict normal Subgroup of G such that A2: the carrier of N2 = N1 ~ N by Th73; consider N3 being strict normal Subgroup of G such that A3: the carrier of N3 = N1 ` N by A1, Th74; N3 is Subgroup of N2 by A2, A3, Th55, GROUP_2:57; then N3 ~ N c= N2 ~ N by Th57; hence ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ~ N c= N2 ~ N ) by A2, A3; ::_thesis: verum end; theorem :: GROUP_11:77 for G being Group for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ~ N ) proof let G be Group; ::_thesis: for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ~ N ) let N, N1 be normal Subgroup of G; ::_thesis: ( N1 is Subgroup of N implies ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ~ N ) ) assume N1 is Subgroup of N ; ::_thesis: ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ~ N ) then consider N2, N3 being strict normal Subgroup of G such that A1: the carrier of N2 = N1 ~ N and A2: the carrier of N3 = N1 ` N and A3: N2 ` N c= N3 ` N by Th75; N3 ` N c= N3 ~ N by Th55; hence ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ~ N ) by A1, A2, A3, XBOOLE_1:1; ::_thesis: verum end; theorem :: GROUP_11:78 for G being Group for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ` N c= N2 ~ N ) proof let G be Group; ::_thesis: for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ` N c= N2 ~ N ) let N, N1 be normal Subgroup of G; ::_thesis: ( N1 is Subgroup of N implies ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ` N c= N2 ~ N ) ) assume N1 is Subgroup of N ; ::_thesis: ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ` N c= N2 ~ N ) then consider N2, N3 being strict normal Subgroup of G such that A1: the carrier of N2 = N1 ~ N and A2: the carrier of N3 = N1 ` N and A3: N3 ~ N c= N2 ~ N by Th76; N3 ` N c= N3 ~ N by Th55; hence ex N2, N3 being strict normal Subgroup of G st ( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ` N c= N2 ~ N ) by A1, A2, A3, XBOOLE_1:1; ::_thesis: verum end; theorem :: GROUP_11:79 for G being Group for N, N1, N2 being normal Subgroup of G st N1 is Subgroup of N2 holds ex N3, N4 being strict normal Subgroup of G st ( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 ) proof let G be Group; ::_thesis: for N, N1, N2 being normal Subgroup of G st N1 is Subgroup of N2 holds ex N3, N4 being strict normal Subgroup of G st ( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 ) let N, N1, N2 be normal Subgroup of G; ::_thesis: ( N1 is Subgroup of N2 implies ex N3, N4 being strict normal Subgroup of G st ( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 ) ) assume A1: N1 is Subgroup of N2 ; ::_thesis: ex N3, N4 being strict normal Subgroup of G st ( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 ) consider N3 being strict normal Subgroup of G such that A2: the carrier of N3 = N ~ N1 by Th73; consider N4 being strict normal Subgroup of G such that A3: the carrier of N4 = N ~ N2 by Th73; N3 is Subgroup of N4 by A1, A2, A3, Th56, GROUP_2:57; then N3 ~ N1 c= N4 ~ N1 by Th57; hence ex N3, N4 being strict normal Subgroup of G st ( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 ) by A2, A3; ::_thesis: verum end; theorem :: GROUP_11:80 for G being Group for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st ( the carrier of N2 = N ` N & N ` N1 c= N2 ` N1 ) proof let G be Group; ::_thesis: for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st ( the carrier of N2 = N ` N & N ` N1 c= N2 ` N1 ) let N, N1 be normal Subgroup of G; ::_thesis: ex N2 being strict normal Subgroup of G st ( the carrier of N2 = N ` N & N ` N1 c= N2 ` N1 ) N is Subgroup of N by GROUP_2:54; then consider N2 being strict normal Subgroup of G such that A1: the carrier of N2 = N ` N by Th74; N2 is Subgroup of N by A1, Th53, GROUP_2:57; then N ` N1 c= N2 ` N1 by Th60; hence ex N2 being strict normal Subgroup of G st ( the carrier of N2 = N ` N & N ` N1 c= N2 ` N1 ) by A1; ::_thesis: verum end; theorem :: GROUP_11:81 for G being Group for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st ( the carrier of N2 = N ~ N & N ~ N1 c= N2 ~ N1 ) proof let G be Group; ::_thesis: for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st ( the carrier of N2 = N ~ N & N ~ N1 c= N2 ~ N1 ) let N, N1 be normal Subgroup of G; ::_thesis: ex N2 being strict normal Subgroup of G st ( the carrier of N2 = N ~ N & N ~ N1 c= N2 ~ N1 ) consider N2 being strict normal Subgroup of G such that A1: the carrier of N2 = N ~ N by Th73; N is Subgroup of N2 by A1, Th54, GROUP_2:57; then N ~ N1 c= N2 ~ N1 by Th57; hence ex N2 being strict normal Subgroup of G st ( the carrier of N2 = N ~ N & N ~ N1 c= N2 ~ N1 ) by A1; ::_thesis: verum end;