set G' = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #);
reconsider H = multMagma(# the carrier of N,the multF of N #) as strict normal Subgroup of G by Lm7;
the carrier of (G ./. N) = the carrier of (G ./. H)
by Def14;
then A1:
( multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) is Group-like & multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) is associative )
by Def15;
now let G' be
Group;
:: thesis: for a being Action of O,the carrier of G' st a = the action of (G ./. N) & multMagma(# the carrier of G',the multF of G' #) = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) holds
a is distributive let a be
Action of
O,the
carrier of
G';
:: thesis: ( a = the action of (G ./. N) & multMagma(# the carrier of G',the multF of G' #) = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) implies a is distributive )assume A5:
a = the
action of
(G ./. N)
;
:: thesis: ( multMagma(# the carrier of G',the multF of G' #) = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) implies a is distributive )assume A6:
multMagma(# the
carrier of
G',the
multF of
G' #)
= multMagma(# the
carrier of
(G ./. N),the
multF of
(G ./. N) #)
;
:: thesis: a is distributive now let o be
Element of
O;
:: thesis: ( o in O implies a . o is Homomorphism of G',G' )assume A7:
o in O
;
:: thesis: a . o is Homomorphism of G',G'then A8:
a . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) }
by A5, Def16;
a . o in Funcs (Cosets N),
(Cosets N)
by A5, A7, FUNCT_2:7;
then consider f being
Function such that A9:
(
a . o = f &
dom f = Cosets N &
rng f c= Cosets N )
by FUNCT_2:def 2;
reconsider f =
f as
Function of the
carrier of
G',the
carrier of
G' by A6, A9, FUNCT_2:4;
now let A1,
A2 be
Element of
G';
:: thesis: f . (A1 * A2) = (f . A1) * (f . A2)set A3 =
A1 * A2;
set B1 =
f . A1;
set B2 =
f . A2;
set B3 =
f . (A1 * A2);
A10:
(
[A1,(f . A1)] in f &
[A2,(f . A2)] in f &
[(A1 * A2),(f . (A1 * A2))] in f )
by A6, A9, FUNCT_1:8;
then consider A1',
B1' being
Element of
Cosets N such that A11:
(
[A1,(f . A1)] = [A1',B1'] & ex
g1,
h1 being
Element of
G st
(
g1 in A1' &
h1 in B1' &
h1 = (G ^ o) . g1 ) )
by A8, A9;
consider A2',
B2' being
Element of
Cosets N such that A12:
(
[A2,(f . A2)] = [A2',B2'] & ex
g2,
h2 being
Element of
G st
(
g2 in A2' &
h2 in B2' &
h2 = (G ^ o) . g2 ) )
by A8, A9, A10;
consider A3',
B3' being
Element of
Cosets N such that A13:
(
[(A1 * A2),(f . (A1 * A2))] = [A3',B3'] & ex
g3,
h3 being
Element of
G st
(
g3 in A3' &
h3 in B3' &
h3 = (G ^ o) . g3 ) )
by A8, A9, A10;
consider g1,
h1 being
Element of
G such that A14:
(
g1 in A1' &
h1 in B1' &
h1 = (G ^ o) . g1 )
by A11;
consider g2,
h2 being
Element of
G such that A15:
(
g2 in A2' &
h2 in B2' &
h2 = (G ^ o) . g2 )
by A12;
consider g3,
h3 being
Element of
G such that A16:
(
g3 in A3' &
h3 in B3' &
h3 = (G ^ o) . g3 )
by A13;
reconsider A1' =
A1',
A2' =
A2',
A3' =
A3',
B1' =
B1',
B2' =
B2',
B3' =
B3' as
Element of
Cosets H by Def14;
A17:
(
A2' = g2 * H &
B2' = h2 * H )
by A15, Lm9;
A18:
(
A3' = g3 * H &
B3' = h3 * H )
by A16, Lm9;
reconsider A1' =
A1',
A2' =
A2',
B1' =
B1',
B2' =
B2' as
Element of
(G ./. H) ;
A19:
(
A2 = g2 * H &
f . A2 = h2 * H )
by A12, A17, ZFMISC_1:33;
A20:
(
A1 * A2 = g3 * H &
f . (A1 * A2) = h3 * H )
by A13, A18, ZFMISC_1:33;
A21:
@ ((nat_hom H) . g1) = (nat_hom H) . g1
;
A22:
@ ((nat_hom H) . g2) = (nat_hom H) . g2
;
A23:
(nat_hom H) . g1 = g1 * H
by GROUP_6:def 9;
A24:
(nat_hom H) . g2 = g2 * H
by GROUP_6:def 9;
A1 * A2 =
the
multF of
G' . A1',
A2'
by A11, A17, A19, ZFMISC_1:33
.=
@ (A1' * A2')
by A6, Def15
.=
(@ A1') * (@ A2')
by GROUP_6:25
;
then A1 * A2 =
(g1 * H) * (g2 * H)
by A14, A17, Lm9
.=
((nat_hom H) . g1) * ((nat_hom H) . g2)
by A21, A22, A23, A24, GROUP_6:24
.=
(nat_hom H) . (g1 * g2)
by GROUP_6:def 7
.=
(g1 * g2) * H
by GROUP_6:def 9
;
then
g3 * H = (g1 * g2) * H
by A13, A18, ZFMISC_1:33;
then
(g3 " ) * (g1 * g2) in H
by GROUP_2:137;
then
(g3 " ) * (g1 * g2) in the
carrier of
H
by STRUCT_0:def 5;
then
(g3 " ) * (g1 * g2) in N
by STRUCT_0:def 5;
then
(G ^ o) . ((g3 " ) * (g1 * g2)) in N
by Lm10;
then
((G ^ o) . (g3 " )) * ((G ^ o) . (g1 * g2)) in N
by GROUP_6:def 7;
then
((G ^ o) . (g3 " )) * (((G ^ o) . g1) * ((G ^ o) . g2)) in N
by GROUP_6:def 7;
then
(h3 " ) * (h1 * h2) in N
by A14, A15, A16, GROUP_6:41;
then
(h3 " ) * (h1 * h2) in the
carrier of
N
by STRUCT_0:def 5;
then A25:
(h3 " ) * (h1 * h2) in H
by STRUCT_0:def 5;
A26:
@ ((nat_hom H) . h1) = (nat_hom H) . h1
;
A27:
@ ((nat_hom H) . h2) = (nat_hom H) . h2
;
A28:
(nat_hom H) . h1 = h1 * H
by GROUP_6:def 9;
A29:
(nat_hom H) . h2 = h2 * H
by GROUP_6:def 9;
(f . A1) * (f . A2) =
the
multF of
G' . B1',
B2'
by A11, A17, A19, ZFMISC_1:33
.=
@ (B1' * B2')
by A6, Def15
.=
(@ B1') * (@ B2')
by GROUP_6:25
;
then (f . A1) * (f . A2) =
(h1 * H) * (h2 * H)
by A14, A17, Lm9
.=
((nat_hom H) . h1) * ((nat_hom H) . h2)
by A26, A27, A28, A29, GROUP_6:24
.=
(nat_hom H) . (h1 * h2)
by GROUP_6:def 7
.=
(h1 * h2) * H
by GROUP_6:def 9
;
hence
f . (A1 * A2) = (f . A1) * (f . A2)
by A20, A25, GROUP_2:137;
:: thesis: verum end; hence
a . o is
Homomorphism of
G',
G'
by A9, GROUP_6:def 7;
:: thesis: verum end; hence
a is
distributive
by Def4;
:: thesis: verum end;
hence
( G ./. N is distributive & G ./. N is Group-like & G ./. N is associative )
by A2, A3, Def5, GROUP_1:def 3, GROUP_1:def 4; :: thesis: verum