let O be set ; for G being GroupWithOperators of O
for M, N being strict normal StableSubgroup of G
for MN being normal StableSubgroup of N st MN = M & M is StableSubgroup of N holds
N ./. MN is normal StableSubgroup of G ./. M
let G be GroupWithOperators of O; for M, N being strict normal StableSubgroup of G
for MN being normal StableSubgroup of N st MN = M & M is StableSubgroup of N holds
N ./. MN is normal StableSubgroup of G ./. M
let M, N be strict normal StableSubgroup of G; for MN being normal StableSubgroup of N st MN = M & M is StableSubgroup of N holds
N ./. MN is normal StableSubgroup of G ./. M
reconsider M' = multMagma(# the carrier of M,the multF of M #) as normal Subgroup of G by Lm7;
reconsider N' = multMagma(# the carrier of N,the multF of N #) as normal Subgroup of G by Lm7;
let MN be normal StableSubgroup of N; ( MN = M & M is StableSubgroup of N implies N ./. MN is normal StableSubgroup of G ./. M )
assume A1:
MN = M
; ( not M is StableSubgroup of N or N ./. MN is normal StableSubgroup of G ./. M )
reconsider MN'' = N',M' `*` as normal Subgroup of N' ;
reconsider MN' = multMagma(# the carrier of MN,the multF of MN #) as normal Subgroup of N by Lm7;
assume
M is StableSubgroup of N
; N ./. MN is normal StableSubgroup of G ./. M
then
M is Subgroup of N
by Def7;
then
( the carrier of M c= the carrier of N & the multF of M = the multF of N || the carrier of M )
by GROUP_2:def 5;
then A2:
M' is Subgroup of N'
by GROUP_2:def 5;
then A3:
N',M' `*` = MN'
by A1, GROUP_6:def 1;
reconsider K = N' ./. (N',M' `*` ) as normal Subgroup of G ./. M' by A2, GROUP_6:35;
then A15: the carrier of K =
Cosets MN'
by TARSKI:2
.=
the carrier of (N ./. MN)
by Def14
;
A16:
now let H be
strict Subgroup of
G ./. M;
( H = multMagma(# the carrier of (N ./. MN),the multF of (N ./. MN) #) implies H is normal )assume A17:
H = multMagma(# the
carrier of
(N ./. MN),the
multF of
(N ./. MN) #)
;
H is normal now let a be
Element of ;
a * H c= H * areconsider a' =
a as
Element of
by Def14;
now let x be
set ;
( x in a * (carr H) implies x in (carr H) * a )assume
x in a * (carr H)
;
x in (carr H) * athen consider b being
Element of
such that A18:
x = a * b
and A19:
b in carr H
by GROUP_2:33;
reconsider b' =
b as
Element of
by Def14;
A20:
x = a' * b'
by A18, Def15;
then reconsider x' =
x as
Element of ;
(
a' * K c= K * a' &
x' in a' * (carr K) )
by A15, A17, A19, A20, GROUP_2:33, GROUP_3:141;
then consider c' being
Element of
such that A21:
x' = c' * a'
and A22:
c' in carr K
by GROUP_2:34;
reconsider c =
c' as
Element of
by Def14;
x = c * a
by A21, Def15;
hence
x in (carr H) * a
by A15, A17, A22, GROUP_2:34;
verum end; hence
a * H c= H * a
by TARSKI:def 3;
verum end; hence
H is
normal
by GROUP_3:141;
verum end;
A23:
the carrier of (G ./. M) = the carrier of (G ./. M')
by Def14;
then A24:
the carrier of (N ./. MN) c= the carrier of (G ./. M)
by A15, GROUP_2:def 5;
A25:
now let o be
Element of
O;
(N ./. MN) ^ b1 = ((G ./. M) ^ b1) | the carrier of (N ./. MN)per cases
( not o in O or o in O )
;
suppose A26:
not
o in O
;
(N ./. MN) ^ b1 = ((G ./. M) ^ b1) | the carrier of (N ./. MN)A27:
the
carrier of
(N ./. MN) c= the
carrier of
(G ./. M)
by A23, A15, GROUP_2:def 5;
A28:
now let x,
y be
set ;
( [x,y] in id the carrier of (N ./. MN) implies [x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN) )assume A29:
[x,y] in id the
carrier of
(N ./. MN)
;
[x,y] in (id the carrier of (G ./. M)) | the carrier of (N ./. MN)then A30:
x in the
carrier of
(N ./. MN)
by RELAT_1:def 10;
x = y
by A29, RELAT_1:def 10;
then
[x,y] in id the
carrier of
(G ./. M)
by A27, A30, RELAT_1:def 10;
hence
[x,y] in (id the carrier of (G ./. M)) | the
carrier of
(N ./. MN)
by A30, RELAT_1:def 11;
verum end; thus (N ./. MN) ^ o =
id the
carrier of
(N ./. MN)
by A26, Def6
.=
(id the carrier of (G ./. M)) | the
carrier of
(N ./. MN)
by A28, A31, RELAT_1:def 2
.=
((G ./. M) ^ o) | the
carrier of
(N ./. MN)
by A26, Def6
;
verum end; suppose A34:
o in O
;
(N ./. MN) ^ b1 = ((G ./. M) ^ b1) | the carrier of (N ./. MN)then
the
action of
(G ./. M) . o in Funcs the
carrier of
(G ./. M),the
carrier of
(G ./. M)
by FUNCT_2:7;
then consider f being
Function such that A35:
f = the
action of
(G ./. M) . o
and A36:
dom f = the
carrier of
(G ./. M)
and
rng f c= the
carrier of
(G ./. M)
by FUNCT_2:def 2;
A37:
f = { [A,B] where A, B is Element of Cosets M : ex a, b being Element of st
( a in A & b in B & b = (G ^ o) . a ) }
by A34, A35, Def16;
the
action of
(N ./. MN) . o in Funcs the
carrier of
(N ./. MN),the
carrier of
(N ./. MN)
by A34, FUNCT_2:7;
then consider g being
Function such that A38:
g = the
action of
(N ./. MN) . o
and A39:
dom g = the
carrier of
(N ./. MN)
and
rng g c= the
carrier of
(N ./. MN)
by FUNCT_2:def 2;
A40:
dom g = (dom f) /\ the
carrier of
(N ./. MN)
by A24, A36, A39, XBOOLE_1:28;
A41:
g = { [A,B] where A, B is Element of Cosets MN : ex a, b being Element of st
( a in A & b in B & b = (N ^ o) . a ) }
by A34, A38, Def16;
A42:
now let x be
set ;
( x in dom g implies g . x = f . x )assume A43:
x in dom g
;
g . x = f . xthen
[x,(g . x)] in g
by FUNCT_1:8;
then consider A2,
B2 being
Element of
Cosets MN such that A44:
[x,(g . x)] = [A2,B2]
and A45:
ex
a,
b being
Element of st
(
a in A2 &
b in B2 &
b = (N ^ o) . a )
by A41;
A46:
A2 = x
by A44, ZFMISC_1:33;
[x,(f . x)] in f
by A24, A36, A39, A43, FUNCT_1:8;
then consider A1,
B1 being
Element of
Cosets M such that A47:
[x,(f . x)] = [A1,B1]
and A48:
ex
a,
b being
Element of st
(
a in A1 &
b in B1 &
b = (G ^ o) . a )
by A37;
A49:
A1 = x
by A47, ZFMISC_1:33;
reconsider A2' =
A2,
B2' =
B2 as
Element of
Cosets MN' by Def14;
reconsider A1' =
A1,
B1' =
B1 as
Element of
Cosets M' by Def14;
set fo =
G ^ o;
N is
Subgroup of
G
by Def7;
then A50:
the
carrier of
N c= the
carrier of
G
by GROUP_2:def 5;
consider a2,
b2 being
Element of
such that A51:
a2 in A2
and A52:
b2 in B2
and A53:
b2 = (N ^ o) . a2
by A45;
A54:
B2' = b2 * MN'
by A52, Lm9;
(
a2 in the
carrier of
N &
b2 in the
carrier of
N )
;
then reconsider a2' =
a2,
b2' =
b2 as
Element of
by A50;
consider a1,
b1 being
Element of
such that A55:
a1 in A1
and A56:
b1 in B1
and A57:
b1 = (G ^ o) . a1
by A48;
A58:
A1' = a1 * M'
by A55, Lm9;
then A63:
b2' * M' = b2 * MN'
by TARSKI:2;
A64:
B2 = g . x
by A44, ZFMISC_1:33;
A65:
B1 = f . x
by A47, ZFMISC_1:33;
then A70:
a2 * MN' = a2' * M'
by TARSKI:2;
A2' = a2 * MN'
by A51, Lm9;
then
(a1 " ) * a2' in M'
by A49, A46, A58, A70, GROUP_2:137;
then
(a1 " ) * a2' in the
carrier of
M
by STRUCT_0:def 5;
then
(a1 " ) * a2' in M
by STRUCT_0:def 5;
then A71:
(G ^ o) . ((a1 " ) * a2') in M
by Lm10;
A72:
b1 " = (G ^ o) . (a1 " )
by A57, GROUP_6:41;
b2' =
((G ^ o) | the carrier of N) . a2
by A53, Def7
.=
(G ^ o) . a2'
by FUNCT_1:72
;
then
(b1 " ) * b2' in M
by A72, A71, GROUP_6:def 7;
then
(b1 " ) * b2' in the
carrier of
M
by STRUCT_0:def 5;
then A73:
(b1 " ) * b2' in M'
by STRUCT_0:def 5;
B1' = b1 * M'
by A56, Lm9;
hence
g . x = f . x
by A65, A64, A63, A73, A54, GROUP_2:137;
verum end; thus (N ./. MN) ^ o =
the
action of
(N ./. MN) . o
by A34, Def6
.=
f | the
carrier of
(N ./. MN)
by A38, A40, A42, FUNCT_1:68
.=
((G ./. M) ^ o) | the
carrier of
(N ./. MN)
by A34, A35, Def6
;
verum end; end;
Cosets MN'' = Cosets MN'
by A4, TARSKI:2;
then reconsider f = CosOp MN'' as BinOp of Cosets MN' ;
now let W1,
W2 be
Element of
Cosets MN';
for A1, A2 being Subset of st W1 = A1 & W2 = A2 holds
f . W1,W2 = A1 * A2reconsider W1' =
W1,
W2' =
W2 as
Element of
Cosets MN'' by A4;
let A1,
A2 be
Subset of ;
( W1 = A1 & W2 = A2 implies f . W1,W2 = A1 * A2 )assume A74:
W1 = A1
;
( W2 = A2 implies f . W1,W2 = A1 * A2 )reconsider A1' =
A1,
A2' =
A2 as
Subset of ;
assume A75:
W2 = A2
;
f . W1,W2 = A1 * A2A76:
now let x be
set ;
( ( x in A1 * A2 implies x in A1' * A2' ) & ( x in A1' * A2' implies x in A1 * A2 ) )hereby ( x in A1' * A2' implies x in A1 * A2 )
assume
x in A1 * A2
;
x in A1' * A2'then consider g,
h being
Element of
such that A77:
x = g * h
and A78:
(
g in A1 &
h in A2 )
;
reconsider g' =
g,
h' =
h as
Element of ;
x = g' * h'
by A77;
hence
x in A1' * A2'
by A78;
verum
end; assume
x in A1' * A2'
;
x in A1 * A2then consider g',
h' being
Element of
such that A79:
x = g' * h'
and A80:
(
g' in A1' &
h' in A2' )
;
reconsider g =
g',
h =
h' as
Element of ;
x = g * h
by A79;
hence
x in A1 * A2
by A80;
verum end; thus f . W1,
W2 =
f . W1',
W2'
.=
A1' * A2'
by A74, A75, GROUP_6:def 4
.=
A1 * A2
by A76, TARSKI:2
;
verum end;
then the multF of K =
CosOp MN'
by GROUP_6:def 4
.=
the multF of (N ./. MN)
by Def15
;
then the multF of (N ./. MN) =
the multF of (G ./. M') || the carrier of K
by GROUP_2:def 5
.=
the multF of (G ./. M) || the carrier of (N ./. MN)
by A15, Def15
;
then
N ./. MN is Subgroup of G ./. M
by A24, GROUP_2:def 5;
hence
N ./. MN is normal StableSubgroup of G ./. M
by A16, A25, Def7, Def10; verum