A1: now
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 ) }
deffunc H1( set ) -> 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 Lm7;
A3: Cosets N = Cosets H by Def14;
A4: now
let x be set ; :: thesis: ( x in O implies H1(x) in Funcs (Cosets N),(Cosets N) )
assume A5: x in O ; :: thesis: H1(x) in Funcs (Cosets N),(Cosets N)
set f = H1(x);
A6: now
let y be set ; :: thesis: ( y in H1(x) implies ex A, B being set st y = [A,B] )
assume y in H1(x) ; :: thesis: ex A, B being set st y = [A,B]
then consider A, B being Element of Cosets N such that
A7: ( y = [A,B] & ( 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 set ;
take A = A; :: thesis: ex B being set st y = [A,B]
take B = B; :: thesis: y = [A,B]
thus y = [A,B] by A7; :: thesis: verum
end;
now
let y, y1, y2 be set ; :: 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] & ( 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
A9: ( [y,y2] = [A2,B2] & ( 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 ) ) ) ;
A10: ( y = A1 & y1 = B1 & y = A2 & y2 = B2 ) by A8, A9, ZFMISC_1:33;
reconsider o = x as Element of O by A5;
consider g1, h1 being Element of G such that
A11: ( g1 in A1 & h1 in B1 & h1 = (G ^ o) . g1 ) by A8;
consider g2, h2 being Element of G such that
A12: ( g2 in A2 & h2 in B2 & h2 = (G ^ o) . g2 ) by A9;
reconsider A1 = A1, A2 = A2, B1 = B1, B2 = B2 as Element of Cosets H by Def14;
set f = G ^ o;
( A1 = g1 * H & A2 = g2 * H ) by A11, A12, Lm9;
then (g2 " ) * g1 in H by A10, GROUP_2:137;
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 Lm10;
then ((G ^ o) . (g2 " )) * ((G ^ o) . g1) in N by GROUP_6:def 7;
then (h2 " ) * h1 in N by A11, A12, GROUP_6:41;
then (h2 " ) * h1 in the carrier of N by STRUCT_0:def 5;
then A13: (h2 " ) * h1 in H by STRUCT_0:def 5;
( B1 = h1 * H & B2 = h2 * H ) by A11, A12, Lm9;
hence y1 = y2 by A10, A13, GROUP_2:137; :: thesis: verum
end;
then reconsider f = H1(x) as Function by A6, FUNCT_1:def 1, RELAT_1:def 1;
now
let y1 be set ; :: thesis: ( ( y1 in Cosets N implies ex y2 being set st [y1,y2] in f ) & ( ex y2 being set st [y1,y2] in f implies y1 in Cosets N ) )
hereby :: thesis: ( ex y2 being set st [y1,y2] in f implies y1 in Cosets N )
assume A14: y1 in Cosets N ; :: thesis: ex y2 being set st [y1,y2] in f
then y1 in Cosets H by Def14;
then consider g being Element of G such that
A15: ( y1 = g * H & y1 = H * g ) by GROUP_6:15;
reconsider o = x as Element of O by A5;
reconsider A = y1 as Element of Cosets N by A14;
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 set ;
take y2 = y2; :: thesis: [y1,y2] in f
now
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 A16: 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, A15, Lm9; :: thesis: ( h in B & h = (G ^ o) . g )
thus h in B by A3, Lm9; :: thesis: h = (G ^ o) . g
thus h = (G ^ o) . g by A16; :: thesis: verum
end;
hence [y1,y2] in f ; :: thesis: verum
end;
given y2 being set such that A17: [y1,y2] in f ; :: thesis: y1 in Cosets N
consider A, B being Element of Cosets N such that
A18: ( [y1,y2] = [A,B] & ( 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 A17;
A in Cosets N by A3;
hence y1 in Cosets N by A18, ZFMISC_1:33; :: thesis: verum
end;
then A19: dom f = Cosets N by RELAT_1:def 4;
now
let y2 be set ; :: thesis: ( y2 in rng f implies y2 in Cosets N )
assume y2 in rng f ; :: thesis: y2 in Cosets N
then consider y1 being set such that
A20: [y1,y2] in f by RELAT_1:def 5;
consider A, B being Element of Cosets N such that
A21: ( [y1,y2] = [A,B] & ( 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 A20;
B in Cosets N by A3;
hence y2 in Cosets N by A21, ZFMISC_1:33; :: thesis: verum
end;
then rng f c= Cosets N by TARSKI:def 3;
hence H1(x) in Funcs (Cosets N),(Cosets N) by A19, FUNCT_2:def 2; :: thesis: verum
end;
ex f being Function of O,(Funcs (Cosets N),(Cosets N)) st
for x being set 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
A22: for x being set 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 ) } ;
A23: now
let y be set ; :: 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
A24: ( y = [A,B] & ( 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 A24;
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 A24; :: 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
A25: ( y = [A,B] & 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 A25;
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 A25; :: 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, A22;
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 A23, TARSKI:2; :: thesis: verum
end;
now
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 Lm2;
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