A1: now :: thesis: ( 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 ; :: thesis: 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 :: thesis: for x being object st x in O holds
H1(x) in Funcs ((Cosets N),(Cosets N))
let x be object ; :: thesis: ( x in O implies H1(x) in Funcs ((Cosets N),(Cosets N)) )
set f = H1(x);
A5: now :: thesis: for y being object st y in H1(x) holds
ex A, B being object st y = [A,B]
let y be object ; :: thesis: ( y in H1(x) implies ex A, B being object st y = [A,B] )
assume y in H1(x) ; :: thesis: 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; :: thesis: ex B being object st y = [A,B]
take B = B; :: thesis: y = [A,B]
thus y = [A,B] by A6; :: thesis: verum
end;
assume A7: x in O ; :: thesis: H1(x) in Funcs ((Cosets N),(Cosets N))
now :: thesis: for y, y1, y2 being object st [y,y1] in H1(x) & [y,y2] in H1(x) holds
y1 = y2
reconsider o = x as Element of O by A7;
let y, y1, y2 be object ; :: thesis: ( [y,y1] in H1(x) & [y,y2] in H1(x) implies y1 = y2 )
assume [y,y1] in H1(x) ; :: thesis: ( [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) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
then reconsider f = H1(x) as Function by A5, FUNCT_1:def 1, RELAT_1:def 1;
now :: thesis: for y1 being object holds
( ( y1 in Cosets N implies ex y2 being object st [y1,y2] in f ) & ( ex y2 being object st [y1,y2] in f implies y1 in Cosets N ) )
let y1 be object ; :: thesis: ( ( y1 in Cosets N implies ex y2 being object st [y1,y2] in f ) & ( ex y2 being object st [y1,y2] in f implies y1 in Cosets N ) )
hereby :: thesis: ( ex y2 being object st [y1,y2] in f implies y1 in Cosets N )
reconsider o = x as Element of O by A7;
assume A25: y1 in Cosets N ; :: thesis: ex y2 being object st [y1,y2] in f
then reconsider A = y1 as Element of Cosets N ;
y1 in Cosets H by A25, Def14;
then consider g being Element of G such that
A26: y1 = g * H and
y1 = H * g by GROUP_6:13;
set h = (G ^ o) . g;
reconsider B = ((G ^ o) . g) * H as Element of Cosets N by A3, GROUP_2:def 15;
reconsider y2 = B as object ;
take y2 = y2; :: thesis: [y1,y2] in f
now :: thesis: for o being Element of O st x = o holds
ex g being Element of G ex h being Element of the carrier of G st
( g in A & h in B & h = (G ^ o) . g )
let o be Element of O; :: thesis: ( x = o implies ex g being Element of G ex h being Element of the carrier of G st
( g in A & h in B & h = (G ^ o) . g ) )
assume A27: x = o ; :: thesis: ex g being Element of G ex h being Element of the carrier of G st
( g in A & h in B & h = (G ^ o) . g )
take g = g; :: thesis: ex h being Element of the carrier of G st
( g in A & h in B & h = (G ^ o) . g )
take h = (G ^ o) . g; :: thesis: ( g in A & h in B & h = (G ^ o) . g )
thus g in A by A3, A26, Lm8; :: thesis: ( h in B & h = (G ^ o) . g )
thus h in B by A3, Lm8; :: thesis: h = (G ^ o) . g
thus h = (G ^ o) . g by A27; :: thesis: verum
end;
hence [y1,y2] in f ; :: thesis: verum
end;
given y2 being object such that A28: [y1,y2] in f ; :: thesis: y1 in Cosets N
consider A, B being Element of Cosets N such that
A29: [y1,y2] = [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 ) by A28;
A in Cosets N by A3;
hence y1 in Cosets N by A29, XTUPLE_0:1; :: thesis: verum
end;
then A30: dom f = Cosets N by XTUPLE_0:def 12;
now :: thesis: for y2 being object st y2 in rng f holds
y2 in Cosets N
let y2 be object ; :: thesis: ( y2 in rng f implies y2 in Cosets N )
assume y2 in rng f ; :: thesis: y2 in Cosets N
then consider y1 being object such that
A31: [y1,y2] in f by XTUPLE_0:def 13;
consider A, B being Element of Cosets N such that
A32: [y1,y2] = [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 ) by A31;
B in Cosets N by A3;
hence y2 in Cosets N by A32, XTUPLE_0:1; :: thesis: verum
end;
then rng f c= Cosets N ;
hence H1(x) in Funcs ((Cosets N),(Cosets N)) by A30, FUNCT_2:def 2; :: thesis: 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; :: thesis: 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; :: thesis: 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 :: thesis: 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 ; :: thesis: ( ( 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 :: thesis: ( 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 ) } ; :: thesis: 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; :: thesis: 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 ) } ; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
now :: thesis: ( O is empty implies ex IT being Action of O,(Cosets N) st IT = [:{},{(id (Cosets N))}:] )
assume O is empty ; :: thesis: ex IT being Action of O,(Cosets N) st IT = [:{},{(id (Cosets N))}:]
then reconsider IT = [:{},{(id (Cosets N))}:] as Action of O,(Cosets N) by Lm1;
take IT = IT; :: thesis: IT = [:{},{(id (Cosets N))}:]
thus IT = [:{},{(id (Cosets N))}:] ; :: thesis: 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; :: thesis: verum