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