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 M9 = multMagma(# the carrier of M, the multF of M #) as normal Subgroup of G by Lm7;
reconsider N9 = 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 MN99 = (N9,M9) `*` as normal Subgroup of N9 ;
reconsider MN9 = 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:
M9 is Subgroup of N9
by GROUP_2:def 5;
then A3:
(N9,M9) `*` = MN9
by A1, GROUP_6:def 1;
reconsider K = N9 ./. ((N9,M9) `*`) as normal Subgroup of G ./. M9 by A2, GROUP_6:29;
A4:
now let x be
set ;
( ( x in Cosets MN9 implies x in Cosets MN99 ) & ( x in Cosets MN99 implies x in Cosets MN9 ) )hereby ( x in Cosets MN99 implies x in Cosets MN9 )
assume
x in Cosets MN9
;
x in Cosets MN99then consider a being
Element of
N such that A5:
x = a * MN9
and
x = MN9 * a
by GROUP_6:13;
reconsider a9 =
a as
Element of
N9 ;
reconsider A =
{a} as
Subset of
N by ZFMISC_1:31;
reconsider A9 =
{a9} as
Subset of
N9 by ZFMISC_1:31;
now let y be
set ;
( ( y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) } implies y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) } ) & ( y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } implies y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } ) )hereby ( y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } implies y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } )
assume
y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) }
;
y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) } then consider g,
h being
Element of
N such that A6:
y = g * h
and A7:
(
g in A &
h in carr MN9 )
;
reconsider h9 =
h as
Element of
N9 ;
reconsider g9 =
g as
Element of
N9 ;
y = g9 * h9
by A6;
hence
y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) }
by A3, A7;
verum
end; assume
y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) }
;
y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } then consider g,
h being
Element of
N9 such that A8:
y = g * h
and A9:
(
g in A9 &
h in carr MN99 )
;
reconsider h9 =
h as
Element of
N ;
reconsider g9 =
g as
Element of
N ;
y = g9 * h9
by A8;
hence
y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) }
by A3, A9;
verum end; then
x = a9 * MN99
by A5, TARSKI:1;
hence
x in Cosets MN99
by GROUP_6:14;
verum
end; assume
x in Cosets MN99
;
x in Cosets MN9then consider a9 being
Element of
N9 such that A10:
x = a9 * MN99
and
x = MN99 * a9
by GROUP_6:13;
reconsider a =
a9 as
Element of
N ;
reconsider A9 =
{a9} as
Subset of
N9 by ZFMISC_1:31;
reconsider A =
{a} as
Subset of
N by ZFMISC_1:31;
now let y be
set ;
( ( y in { (g * h) where g, h is Element of N : ( g in A & h in carr MN9 ) } implies y in { (g99 * h99) where g99, h99 is Element of N9 : ( g99 in A9 & h99 in carr MN99 ) } ) & ( y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } implies y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } ) )hereby ( y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) } implies y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } )
end; assume
y in { (g * h) where g, h is Element of N9 : ( g in A9 & h in carr MN99 ) }
;
y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) } then consider g,
h being
Element of
N9 such that A13:
y = g * h
and A14:
(
g in A9 &
h in carr MN99 )
;
reconsider h9 =
h as
Element of
N ;
reconsider g9 =
g as
Element of
N ;
y = g9 * h9
by A13;
hence
y in { (g99 * h99) where g99, h99 is Element of N : ( g99 in A & h99 in carr MN9 ) }
by A3, A14;
verum end; then
x = a * MN9
by A10, TARSKI:1;
hence
x in Cosets MN9
by GROUP_6:14;
verum end;
then A15: the carrier of K =
Cosets MN9
by TARSKI:1
.=
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
(G ./. M);
a * H c= H * areconsider a9 =
a as
Element of
(G ./. M9) 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
(G ./. M) such that A18:
x = a * b
and A19:
b in carr H
by GROUP_2:27;
reconsider b9 =
b as
Element of
(G ./. M9) by Def14;
A20:
x = a9 * b9
by A18, Def15;
then reconsider x9 =
x as
Element of
(G ./. M9) ;
(
a9 * K c= K * a9 &
x9 in a9 * (carr K) )
by A15, A17, A19, A20, GROUP_2:27, GROUP_3:118;
then consider c9 being
Element of
(G ./. M9) such that A21:
x9 = c9 * a9
and A22:
c9 in carr K
by GROUP_2:28;
reconsider c =
c9 as
Element of
(G ./. M) by Def14;
x = c * a
by A21, Def15;
hence
x in (carr H) * a
by A15, A17, A22, GROUP_2:28;
verum end; hence
a * H c= H * a
by TARSKI:def 3;
verum end; hence
H is
normal
by GROUP_3:118;
verum end;
A23:
the carrier of (G ./. M) = the carrier of (G ./. M9)
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:5;
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 G 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:5;
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 N 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:1;
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
N st
(
a in A2 &
b in B2 &
b = (N ^ o) . a )
by A41;
A46:
A2 = x
by A44, ZFMISC_1:27;
[x,(f . x)] in f
by A24, A36, A39, A43, FUNCT_1:1;
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
G st
(
a in A1 &
b in B1 &
b = (G ^ o) . a )
by A37;
A49:
A1 = x
by A47, ZFMISC_1:27;
reconsider A29 =
A2,
B29 =
B2 as
Element of
Cosets MN9 by Def14;
reconsider A19 =
A1,
B19 =
B1 as
Element of
Cosets M9 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
N such that A51:
a2 in A2
and A52:
b2 in B2
and A53:
b2 = (N ^ o) . a2
by A45;
A54:
B29 = b2 * MN9
by A52, Lm9;
(
a2 in the
carrier of
N &
b2 in the
carrier of
N )
;
then reconsider a29 =
a2,
b29 =
b2 as
Element of
G by A50;
consider a1,
b1 being
Element of
G such that A55:
a1 in A1
and A56:
b1 in B1
and A57:
b1 = (G ^ o) . a1
by A48;
A58:
A19 = a1 * M9
by A55, Lm9;
then A63:
b29 * M9 = b2 * MN9
by TARSKI:1;
A64:
B2 = g . x
by A44, ZFMISC_1:27;
A65:
B1 = f . x
by A47, ZFMISC_1:27;
then A70:
a2 * MN9 = a29 * M9
by TARSKI:1;
A29 = a2 * MN9
by A51, Lm9;
then
(a1 ") * a29 in M9
by A49, A46, A58, A70, GROUP_2:114;
then
(a1 ") * a29 in the
carrier of
M
by STRUCT_0:def 5;
then
(a1 ") * a29 in M
by STRUCT_0:def 5;
then A71:
(G ^ o) . ((a1 ") * a29) in M
by Lm10;
A72:
b1 " = (G ^ o) . (a1 ")
by A57, GROUP_6:32;
b29 =
((G ^ o) | the carrier of N) . a2
by A53, Def7
.=
(G ^ o) . a29
by FUNCT_1:49
;
then
(b1 ") * b29 in M
by A72, A71, GROUP_6:def 6;
then
(b1 ") * b29 in the
carrier of
M
by STRUCT_0:def 5;
then A73:
(b1 ") * b29 in M9
by STRUCT_0:def 5;
B19 = b1 * M9
by A56, Lm9;
hence
g . x = f . x
by A65, A64, A63, A73, A54, GROUP_2:114;
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:46
.=
((G ./. M) ^ o) | the
carrier of
(N ./. MN)
by A34, A35, Def6
;
verum end; end;
Cosets MN99 = Cosets MN9
by A4, TARSKI:1;
then reconsider f = CosOp MN99 as BinOp of (Cosets MN9) ;
now let W1,
W2 be
Element of
Cosets MN9;
for A1, A2 being Subset of N st W1 = A1 & W2 = A2 holds
f . (W1,W2) = A1 * A2reconsider W19 =
W1,
W29 =
W2 as
Element of
Cosets MN99 by A4;
let A1,
A2 be
Subset of
N;
( W1 = A1 & W2 = A2 implies f . (W1,W2) = A1 * A2 )assume A74:
W1 = A1
;
( W2 = A2 implies f . (W1,W2) = A1 * A2 )reconsider A19 =
A1,
A29 =
A2 as
Subset of
N9 ;
assume A75:
W2 = A2
;
f . (W1,W2) = A1 * A2A76:
now let x be
set ;
( ( x in A1 * A2 implies x in A19 * A29 ) & ( x in A19 * A29 implies x in A1 * A2 ) )hereby ( x in A19 * A29 implies x in A1 * A2 )
assume
x in A1 * A2
;
x in A19 * A29then consider g,
h being
Element of
N such that A77:
x = g * h
and A78:
(
g in A1 &
h in A2 )
;
reconsider g9 =
g,
h9 =
h as
Element of
N9 ;
x = g9 * h9
by A77;
hence
x in A19 * A29
by A78;
verum
end; assume
x in A19 * A29
;
x in A1 * A2then consider g9,
h9 being
Element of
N9 such that A79:
x = g9 * h9
and A80:
(
g9 in A19 &
h9 in A29 )
;
reconsider g =
g9,
h =
h9 as
Element of
N ;
x = g * h
by A79;
hence
x in A1 * A2
by A80;
verum end; thus f . (
W1,
W2) =
f . (
W19,
W29)
.=
A19 * A29
by A74, A75, GROUP_6:def 3
.=
A1 * A2
by A76, TARSKI:1
;
verum end;
then the multF of K =
CosOp MN9
by GROUP_6:def 3
.=
the multF of (N ./. MN)
by Def15
;
then the multF of (N ./. MN) =
the multF of (G ./. M9) || 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