let O be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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 MN be normal StableSubgroup of N; :: thesis: ( MN = M & M is StableSubgroup of N implies N ./. MN is normal StableSubgroup of G ./. M )
assume A1:
MN = M
; :: thesis: ( not M is StableSubgroup of N or N ./. MN is normal StableSubgroup of G ./. M )
assume A2:
M is StableSubgroup of N
; :: thesis: N ./. MN is normal StableSubgroup of G ./. M
reconsider N' = multMagma(# the carrier of N,the multF of N #) as normal Subgroup of G by Lm7;
reconsider M' = multMagma(# the carrier of M,the multF of M #) as normal Subgroup of G by Lm7;
reconsider MN' = multMagma(# the carrier of MN,the multF of MN #) as normal Subgroup of N by Lm7;
M is Subgroup of N
by A2, 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 A3:
M' is Subgroup of N'
by GROUP_2:def 5;
then reconsider K = N' ./. (N',M' `*` ) as normal Subgroup of G ./. M' by GROUP_6:35;
A4:
N',M' `*` = MN'
by A1, A3, GROUP_6:def 1;
reconsider MN'' = N',M' `*` as normal Subgroup of N' ;
A5:
the carrier of (G ./. M) = the carrier of (G ./. M')
by Def14;
then
Cosets MN'' = Cosets MN'
by TARSKI:2;
then reconsider f = CosOp MN'' as BinOp of Cosets MN' ;
A13:
now let W1,
W2 be
Element of
Cosets MN';
:: thesis: for A1, A2 being Subset of N st W1 = A1 & W2 = A2 holds
f . W1,W2 = A1 * A2let A1,
A2 be
Subset of
N;
:: thesis: ( W1 = A1 & W2 = A2 implies f . W1,W2 = A1 * A2 )assume A14:
W1 = A1
;
:: thesis: ( W2 = A2 implies f . W1,W2 = A1 * A2 )assume A15:
W2 = A2
;
:: thesis: f . W1,W2 = A1 * A2reconsider W1' =
W1,
W2' =
W2 as
Element of
Cosets MN'' by A6;
reconsider A1' =
A1,
A2' =
A2 as
Subset of
N' ;
thus f . W1,
W2 =
f . W1',
W2'
.=
A1' * A2'
by A14, A15, GROUP_6:def 4
.=
A1 * A2
by A16, TARSKI:2
;
:: thesis: verum end;
A19: the carrier of K =
Cosets MN'
by A6, TARSKI:2
.=
the carrier of (N ./. MN)
by Def14
;
A20: the multF of K =
CosOp MN'
by A13, GROUP_6:def 4
.=
the multF of (N ./. MN)
by Def15
;
A21:
now let H be
strict Subgroup of
G ./. M;
:: thesis: ( H = multMagma(# the carrier of (N ./. MN),the multF of (N ./. MN) #) implies H is normal )assume A22:
H = multMagma(# the
carrier of
(N ./. MN),the
multF of
(N ./. MN) #)
;
:: thesis: H is normalnow let a be
Element of
(G ./. M);
:: thesis: a * H c= H * areconsider a' =
a as
Element of
(G ./. M') by Def14;
now let x be
set ;
:: thesis: ( x in a * (carr H) implies x in (carr H) * a )assume
x in a * (carr H)
;
:: thesis: x in (carr H) * athen consider b being
Element of
(G ./. M) such that A23:
(
x = a * b &
b in carr H )
by GROUP_2:33;
reconsider b' =
b as
Element of
(G ./. M') by Def14;
A24:
x = a' * b'
by A23, Def15;
then reconsider x' =
x as
Element of
(G ./. M') ;
A25:
a' * K c= K * a'
by GROUP_3:141;
x' in a' * (carr K)
by A19, A22, A23, A24, GROUP_2:33;
then consider c' being
Element of
(G ./. M') such that A26:
(
x' = c' * a' &
c' in carr K )
by A25, GROUP_2:34;
reconsider c =
c' as
Element of
(G ./. M) by Def14;
x = c * a
by A26, Def15;
hence
x in (carr H) * a
by A19, A22, A26, GROUP_2:34;
:: thesis: verum end; hence
a * H c= H * a
by TARSKI:def 3;
:: thesis: verum end; hence
H is
normal
by GROUP_3:141;
:: thesis: verum end;
A27:
the carrier of (N ./. MN) c= the carrier of (G ./. M)
by A5, A19, GROUP_2:def 5;
the multF of (N ./. MN) =
the multF of (G ./. M') || the carrier of K
by A20, GROUP_2:def 5
.=
the multF of (G ./. M) || the carrier of (N ./. MN)
by A19, Def15
;
then A28:
N ./. MN is Subgroup of G ./. M
by A27, GROUP_2:def 5;
now let o be
Element of
O;
:: thesis: (N ./. MN) ^ b1 = ((G ./. M) ^ b1) | the carrier of (N ./. MN)per cases
( not o in O or o in O )
;
suppose A35:
o in O
;
:: thesis: (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 A36:
(
f = the
action of
(G ./. M) . o &
dom f = the
carrier of
(G ./. M) &
rng f c= the
carrier of
(G ./. M) )
by FUNCT_2:def 2;
the
action of
(N ./. MN) . o in Funcs the
carrier of
(N ./. MN),the
carrier of
(N ./. MN)
by A35, FUNCT_2:7;
then consider g being
Function such that A37:
(
g = the
action of
(N ./. MN) . o &
dom g = the
carrier of
(N ./. MN) &
rng g c= the
carrier of
(N ./. MN) )
by FUNCT_2:def 2;
A38:
g = { [A,B] where A, B is Element of Cosets MN : ex a, b being Element of N st
( a in A & b in B & b = (N ^ o) . a ) }
by A35, A37, Def16;
A39:
f = { [A,B] where A, B is Element of Cosets M : ex a, b being Element of G st
( a in A & b in B & b = (G ^ o) . a ) }
by A35, A36, Def16;
A40:
dom g = (dom f) /\ the
carrier of
(N ./. MN)
by A27, A36, A37, XBOOLE_1:28;
A41:
now let x be
set ;
:: thesis: ( x in dom g implies g . x = f . x )assume A42:
x in dom g
;
:: thesis: g . x = f . xthen
[x,(f . x)] in f
by A27, A36, A37, FUNCT_1:8;
then consider A1,
B1 being
Element of
Cosets M such that A43:
(
[x,(f . x)] = [A1,B1] & ex
a,
b being
Element of
G st
(
a in A1 &
b in B1 &
b = (G ^ o) . a ) )
by A39;
[x,(g . x)] in g
by A42, FUNCT_1:8;
then consider A2,
B2 being
Element of
Cosets MN such that A44:
(
[x,(g . x)] = [A2,B2] & ex
a,
b being
Element of
N st
(
a in A2 &
b in B2 &
b = (N ^ o) . a ) )
by A38;
consider a1,
b1 being
Element of
G such that A45:
(
a1 in A1 &
b1 in B1 &
b1 = (G ^ o) . a1 )
by A43;
consider a2,
b2 being
Element of
N such that A46:
(
a2 in A2 &
b2 in B2 &
b2 = (N ^ o) . a2 )
by A44;
A47:
(
A1 = x &
A2 = x &
B1 = f . x &
B2 = g . x )
by A43, A44, ZFMISC_1:33;
reconsider A1' =
A1,
B1' =
B1 as
Element of
Cosets M' by Def14;
reconsider A2' =
A2,
B2' =
B2 as
Element of
Cosets MN' by Def14;
A48:
(
a2 in the
carrier of
N &
b2 in the
carrier of
N )
;
N is
Subgroup of
G
by Def7;
then A49:
the
carrier of
N c= the
carrier of
G
by GROUP_2:def 5;
then reconsider a2' =
a2,
b2' =
b2 as
Element of
G by A48;
set fo =
G ^ o;
A56:
A1' = a1 * M'
by A45, Lm9;
A57:
A2' = a2 * MN'
by A46, Lm9;
A58:
a2 * MN' = a2' * M'
by A50, TARSKI:2;
A59:
b1 " = (G ^ o) . (a1 " )
by A45, GROUP_6:41;
A60:
b2' =
((G ^ o) | the carrier of N) . a2
by A46, Def7
.=
(G ^ o) . a2'
by FUNCT_1:72
;
A61:
b2' * M' = b2 * MN'
by A53, TARSKI:2;
(a1 " ) * a2' in M'
by A47, A56, A57, A58, 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
(G ^ o) . ((a1 " ) * a2') in M
by Lm10;
then
(b1 " ) * b2' in M
by A59, A60, GROUP_6:def 7;
then
(b1 " ) * b2' in the
carrier of
M
by STRUCT_0:def 5;
then A62:
(b1 " ) * b2' in M'
by STRUCT_0:def 5;
A63:
B1' = b1 * M'
by A45, Lm9;
B2' = b2 * MN'
by A46, Lm9;
hence
g . x = f . x
by A47, A61, A62, A63, GROUP_2:137;
:: thesis: verum end; thus (N ./. MN) ^ o =
the
action of
(N ./. MN) . o
by A35, Def6
.=
f | the
carrier of
(N ./. MN)
by A37, A40, A41, FUNCT_1:68
.=
((G ./. M) ^ o) | the
carrier of
(N ./. MN)
by A35, A36, Def6
;
:: thesis: verum end; end;
hence
N ./. MN is normal StableSubgroup of G ./. M
by A21, A28, Def7, Def10; :: thesis: verum