reconsider H = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;
set G9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #);
A2:
now for G9 being Group
for a being Action of O, the carrier of G9 st a = the action of (G ./. N) & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) holds
a is distributive let G9 be
Group;
for a being Action of O, the carrier of G9 st a = the action of (G ./. N) & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) holds
a is distributive let a be
Action of
O, the
carrier of
G9;
( a = the action of (G ./. N) & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) implies a is distributive )assume A3:
a = the
action of
(G ./. N)
;
( multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) implies a is distributive )assume A4:
multMagma(# the
carrier of
G9, the
multF of
G9 #)
= multMagma(# the
carrier of
(G ./. N), the
multF of
(G ./. N) #)
;
a is distributive now for o being Element of O st o in O holds
a . o is Homomorphism of G9,G9let o be
Element of
O;
( o in O implies a . o is Homomorphism of G9,G9 )assume A5:
o in O
;
a . o is Homomorphism of G9,G9then A6:
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 A3, Def16;
a . o in Funcs (
(Cosets N),
(Cosets N))
by A3, A5, FUNCT_2:5;
then consider f being
Function such that A7:
a . o = f
and A8:
dom f = Cosets N
and A9:
rng f c= Cosets N
by FUNCT_2:def 2;
reconsider f =
f as
Function of the
carrier of
G9, the
carrier of
G9 by A4, A8, A9, FUNCT_2:2;
now for A1, A2 being Element of G9 holds f . (A1 * A2) = (f . A1) * (f . A2)let A1,
A2 be
Element of
G9;
f . (A1 * A2) = (f . A1) * (f . A2)set A3 =
A1 * A2;
set B1 =
f . A1;
set B2 =
f . A2;
set B3 =
f . (A1 * A2);
[A1,(f . A1)] in f
by A4, A8, FUNCT_1:1;
then consider A19,
B19 being
Element of
Cosets N such that A10:
[A1,(f . A1)] = [A19,B19]
and A11:
ex
g1,
h1 being
Element of
G st
(
g1 in A19 &
h1 in B19 &
h1 = (G ^ o) . g1 )
by A6, A7;
[A2,(f . A2)] in f
by A4, A8, FUNCT_1:1;
then consider A29,
B29 being
Element of
Cosets N such that A12:
[A2,(f . A2)] = [A29,B29]
and A13:
ex
g2,
h2 being
Element of
G st
(
g2 in A29 &
h2 in B29 &
h2 = (G ^ o) . g2 )
by A6, A7;
[(A1 * A2),(f . (A1 * A2))] in f
by A4, A8, FUNCT_1:1;
then consider A39,
B39 being
Element of
Cosets N such that A14:
[(A1 * A2),(f . (A1 * A2))] = [A39,B39]
and A15:
ex
g3,
h3 being
Element of
G st
(
g3 in A39 &
h3 in B39 &
h3 = (G ^ o) . g3 )
by A6, A7;
consider g3,
h3 being
Element of
G such that A16:
g3 in A39
and A17:
h3 in B39
and A18:
h3 = (G ^ o) . g3
by A15;
consider g2,
h2 being
Element of
G such that A19:
g2 in A29
and A20:
h2 in B29
and A21:
h2 = (G ^ o) . g2
by A13;
consider g1,
h1 being
Element of
G such that A22:
g1 in A19
and A23:
h1 in B19
and A24:
h1 = (G ^ o) . g1
by A11;
A25:
(
@ ((nat_hom H) . g1) = (nat_hom H) . g1 &
@ ((nat_hom H) . g2) = (nat_hom H) . g2 )
;
A26:
(
(nat_hom H) . g1 = g1 * H &
(nat_hom H) . g2 = g2 * H )
by GROUP_6:def 8;
reconsider A19 =
A19,
A29 =
A29,
A39 =
A39,
B19 =
B19,
B29 =
B29,
B39 =
B39 as
Element of
Cosets H by Def14;
A27:
A29 = g2 * H
by A19, Lm8;
A28:
A39 = g3 * H
by A16, Lm8;
A29:
B29 = h2 * H
by A20, Lm8;
reconsider A19 =
A19,
A29 =
A29,
B19 =
B19,
B29 =
B29 as
Element of
(G ./. H) ;
A2 = g2 * H
by A12, A27, XTUPLE_0:1;
then A1 * A2 =
the
multF of
G9 . (
A19,
A29)
by A10, A27, XTUPLE_0:1
.=
@ (A19 * A29)
by A4, Def15
.=
(@ A19) * (@ A29)
by GROUP_6:20
;
then A1 * A2 =
(g1 * H) * (g2 * H)
by A22, A27, Lm8
.=
((nat_hom H) . g1) * ((nat_hom H) . g2)
by A25, A26, GROUP_6:19
.=
(nat_hom H) . (g1 * g2)
by GROUP_6:def 6
.=
(g1 * g2) * H
by GROUP_6:def 8
;
then
g3 * H = (g1 * g2) * H
by A14, A28, XTUPLE_0:1;
then
(g3 ") * (g1 * g2) in H
by GROUP_2:114;
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 Lm9;
then
((G ^ o) . (g3 ")) * ((G ^ o) . (g1 * g2)) in N
by GROUP_6:def 6;
then
((G ^ o) . (g3 ")) * (((G ^ o) . g1) * ((G ^ o) . g2)) in N
by GROUP_6:def 6;
then
(h3 ") * (h1 * h2) in N
by A24, A21, A18, GROUP_6:32;
then
(h3 ") * (h1 * h2) in the
carrier of
N
by STRUCT_0:def 5;
then A30:
(h3 ") * (h1 * h2) in H
by STRUCT_0:def 5;
A31:
(
(nat_hom H) . h1 = h1 * H &
(nat_hom H) . h2 = h2 * H )
by GROUP_6:def 8;
B39 = h3 * H
by A17, Lm8;
then A32:
f . (A1 * A2) = h3 * H
by A14, XTUPLE_0:1;
A33:
(
@ ((nat_hom H) . h1) = (nat_hom H) . h1 &
@ ((nat_hom H) . h2) = (nat_hom H) . h2 )
;
f . A2 = h2 * H
by A12, A29, XTUPLE_0:1;
then (f . A1) * (f . A2) =
the
multF of
G9 . (
B19,
B29)
by A10, A29, XTUPLE_0:1
.=
@ (B19 * B29)
by A4, Def15
.=
(@ B19) * (@ B29)
by GROUP_6:20
;
then (f . A1) * (f . A2) =
(h1 * H) * (h2 * H)
by A23, A29, Lm8
.=
((nat_hom H) . h1) * ((nat_hom H) . h2)
by A33, A31, GROUP_6:19
.=
(nat_hom H) . (h1 * h2)
by GROUP_6:def 6
.=
(h1 * h2) * H
by GROUP_6:def 8
;
hence
f . (A1 * A2) = (f . A1) * (f . A2)
by A32, A30, GROUP_2:114;
verum end; hence
a . o is
Homomorphism of
G9,
G9
by A7, GROUP_6:def 6;
verum end; hence
a is
distributive
;
verum end;
the carrier of (G ./. N) = the carrier of (G ./. H)
by Def14;
then A34:
( 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;
hence
( G ./. N is distributive & G ./. N is Group-like & G ./. N is associative )
by A1, A2, GROUP_1:def 2, GROUP_1:def 3; verum