A1:
now ( not O is empty implies ex IT being Action of O,(Cosets N) st
for o being Element of O holds IT . 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 ) } )deffunc H1(
object )
-> set =
{ [A,B] where A, B is Element of Cosets N : for o being Element of O st $1 = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } ;
reconsider H =
multMagma(# the
carrier of
N, the
multF of
N #) as
strict normal Subgroup of
G by Lm6;
assume A2:
not
O is
empty
;
ex IT being Action of O,(Cosets N) st
for o being Element of O holds IT . 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 ) } A3:
Cosets N = Cosets H
by Def14;
A4:
now for x being object st x in O holds
H1(x) in Funcs ((Cosets N),(Cosets N))let x be
object ;
( x in O implies H1(x) in Funcs ((Cosets N),(Cosets N)) )set f =
H1(
x);
A5:
now for y being object st y in H1(x) holds
ex A, B being object st y = [A,B]let y be
object ;
( y in H1(x) implies ex A, B being object st y = [A,B] )assume
y in H1(
x)
;
ex A, B being object st y = [A,B]then consider A,
B being
Element of
Cosets N such that A6:
y = [A,B]
and
for
o being
Element of
O st
x = o holds
ex
g,
h being
Element of
G st
(
g in A &
h in B &
h = (G ^ o) . g )
;
reconsider A =
A,
B =
B as
object ;
take A =
A;
ex B being object st y = [A,B]take B =
B;
y = [A,B]thus
y = [A,B]
by A6;
verum end; assume A7:
x in O
;
H1(x) in Funcs ((Cosets N),(Cosets N))now for y, y1, y2 being object st [y,y1] in H1(x) & [y,y2] in H1(x) holds
y1 = y2reconsider o =
x as
Element of
O by A7;
let y,
y1,
y2 be
object ;
( [y,y1] in H1(x) & [y,y2] in H1(x) implies y1 = y2 )assume
[y,y1] in H1(
x)
;
( [y,y2] in H1(x) implies y1 = y2 )then consider A1,
B1 being
Element of
Cosets N such that A8:
[y,y1] = [A1,B1]
and A9:
for
o being
Element of
O st
x = o holds
ex
g,
h being
Element of
G st
(
g in A1 &
h in B1 &
h = (G ^ o) . g )
;
assume
[y,y2] in H1(
x)
;
y1 = y2then consider A2,
B2 being
Element of
Cosets N such that A10:
[y,y2] = [A2,B2]
and A11:
for
o being
Element of
O st
x = o holds
ex
g,
h being
Element of
G st
(
g in A2 &
h in B2 &
h = (G ^ o) . g )
;
A12:
y1 = B1
by A8, XTUPLE_0:1;
A13:
y2 = B2
by A10, XTUPLE_0:1;
A14:
y = A2
by A10, XTUPLE_0:1;
set f =
G ^ o;
A15:
y = A1
by A8, XTUPLE_0:1;
consider g1,
h1 being
Element of
G such that A16:
g1 in A1
and A17:
h1 in B1
and A18:
h1 = (G ^ o) . g1
by A9;
consider g2,
h2 being
Element of
G such that A19:
g2 in A2
and A20:
h2 in B2
and A21:
h2 = (G ^ o) . g2
by A11;
reconsider A1 =
A1,
A2 =
A2,
B1 =
B1,
B2 =
B2 as
Element of
Cosets H by Def14;
A22:
A2 = g2 * H
by A19, Lm8;
A1 = g1 * H
by A16, Lm8;
then
(g2 ") * g1 in H
by A15, A14, A22, GROUP_2:114;
then
(g2 ") * g1 in the
carrier of
H
by STRUCT_0:def 5;
then
(g2 ") * g1 in N
by STRUCT_0:def 5;
then
(G ^ o) . ((g2 ") * g1) in N
by Lm9;
then
((G ^ o) . (g2 ")) * ((G ^ o) . g1) in N
by GROUP_6:def 6;
then
(h2 ") * h1 in N
by A18, A21, GROUP_6:32;
then
(h2 ") * h1 in the
carrier of
N
by STRUCT_0:def 5;
then A23:
(h2 ") * h1 in H
by STRUCT_0:def 5;
A24:
B2 = h2 * H
by A20, Lm8;
B1 = h1 * H
by A17, Lm8;
hence
y1 = y2
by A12, A13, A23, A24, GROUP_2:114;
verum end; then reconsider f =
H1(
x) as
Function by A5, FUNCT_1:def 1, RELAT_1:def 1;
then A30:
dom f = Cosets N
by XTUPLE_0:def 12;
then
rng f c= Cosets N
;
hence
H1(
x)
in Funcs (
(Cosets N),
(Cosets N))
by A30, FUNCT_2:def 2;
verum end;
ex
f being
Function of
O,
(Funcs ((Cosets N),(Cosets N))) st
for
x being
object st
x in O holds
f . x = H1(
x)
from FUNCT_2:sch 2(A4);
then consider IT being
Function of
O,
(Funcs ((Cosets N),(Cosets N))) such that A33:
for
x being
object st
x in O holds
IT . x = H1(
x)
;
reconsider IT =
IT as
Action of
O,
(Cosets N) ;
take IT =
IT;
for o being Element of O holds IT . 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 ) } let o be
Element of
O;
IT . 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 ) } reconsider x =
o as
set ;
set X =
{ [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } ;
set Y =
{ [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 ) } ;
A34:
now for y being object holds
( ( y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } implies y in { [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 ) } ) & ( y in { [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 ) } implies y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } ) )let y be
object ;
( ( y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } implies y in { [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 ) } ) & ( y in { [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 ) } implies y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } ) )hereby ( y in { [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 ) } implies y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } )
assume
y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) }
;
y in { [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 ) } then consider A,
B being
Element of
Cosets N such that A35:
y = [A,B]
and A36:
for
o being
Element of
O st
x = o holds
ex
g,
h being
Element of
G st
(
g in A &
h in B &
h = (G ^ o) . g )
;
ex
g,
h being
Element of
G st
(
g in A &
h in B &
h = (G ^ o) . g )
by A36;
hence
y in { [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 A35;
verum
end; assume
y in { [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 ) }
;
y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } then consider A,
B being
Element of
Cosets N such that A37:
y = [A,B]
and A38:
ex
g,
h being
Element of
G st
(
g in A &
h in B &
h = (G ^ o) . g )
;
for
o being
Element of
O st
x = o holds
ex
g,
h being
Element of
G st
(
g in A &
h in B &
h = (G ^ o) . g )
by A38;
hence
y in { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) }
by A37;
verum end;
IT . o = { [A,B] where A, B is Element of Cosets N : for o being Element of O st x = o holds
ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) }
by A2, A33;
hence
IT . 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 A34, TARSKI:2;
verum end;
hence
( ( not O is empty implies ex b1 being Action of O,(Cosets N) st
for o being Element of O holds b1 . 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 ) } ) & ( O is empty implies ex b1 being Action of O,(Cosets N) st b1 = [:{},{(id (Cosets N))}:] ) )
by A1; verum