:: 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;