let O be set ; :: thesis: for G being GroupWithOperators of O
for A being Subset of G
for g1 being Element of G holds
( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )
let G be GroupWithOperators of O; :: thesis: for A being Subset of G
for g1 being Element of G holds
( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )
let A be Subset of G; :: thesis: for g1 being Element of G holds
( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )
let g1 be Element of G; :: thesis: ( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )
set H9 = the_stable_subgroup_of A;
set Y = the carrier of (the_stable_subgroup_of A);
A1: A c= the carrier of (the_stable_subgroup_of A) by Def26;
thus ( g1 in the_stable_subgroup_of A implies ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) ) :: thesis: ( ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) implies g1 in the_stable_subgroup_of A )
proof
defpred S1[ set ] means ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & $1 = Product (F |^ I) & len F = len I & rng F c= C );
assume A2: g1 in the_stable_subgroup_of A ; :: thesis: ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 )
reconsider B = { b where b is Element of G : S1[b] } as Subset of G from DOMAIN_1:sch 7();
A3: now :: thesis: for c, d being Element of G st c in B & d in B holds
c * d in B
let c, d be Element of G; :: thesis: ( c in B & d in B implies c * d in B )
assume that
A4: c in B and
A5: d in B ; :: thesis: c * d in B
ex d1 being Element of G st
( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & d1 = Product (F |^ I) & len F = len I & rng F c= C ) ) by A4;
then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT , C being Subset of G such that
A6: C = the_stable_subset_generated_by (A, the action of G) and
A7: c = Product (F1 |^ I1) and
A8: len F1 = len I1 and
A9: rng F1 c= C ;
ex d2 being Element of G st
( d = d2 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & d2 = Product (F |^ I) & len F = len I & rng F c= C ) ) by A5;
then consider F2 being FinSequence of the carrier of G, I2 being FinSequence of INT , C being Subset of G such that
A10: C = the_stable_subset_generated_by (A, the action of G) and
A11: d = Product (F2 |^ I2) and
A12: len F2 = len I2 and
A13: rng F2 c= C ;
A14: len (F1 ^ F2) = (len I1) + (len I2) by A8, A12, FINSEQ_1:22
.= len (I1 ^ I2) by FINSEQ_1:22 ;
rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:31;
then A15: rng (F1 ^ F2) c= C by A6, A9, A10, A13, XBOOLE_1:8;
c * d = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A7, A11, GROUP_4:5
.= Product ((F1 ^ F2) |^ (I1 ^ I2)) by A8, A12, GROUP_4:19 ;
hence c * d in B by A10, A15, A14; :: thesis: verum
end;
A16: now :: thesis: for o being Element of O
for c being Element of G st c in B holds
(G ^ o) . c in B
let o be Element of O; :: thesis: for c being Element of G st c in B holds
(G ^ o) . c in B
let c be Element of G; :: thesis: ( c in B implies (G ^ o) . c in B )
assume c in B ; :: thesis: (G ^ o) . c in B
then ex d1 being Element of G st
( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & d1 = Product (F |^ I) & len F = len I & rng F c= C ) ) ;
then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT , C being Subset of G such that
A17: C = the_stable_subset_generated_by (A, the action of G) and
A18: c = Product (F1 |^ I1) and
A19: len F1 = len I1 and
A20: rng F1 c= C ;
deffunc H1( Nat) -> set = (G ^ o) . (F1 . $1);
consider F2 being FinSequence such that
A21: len F2 = len F1 and
A22: for k being Nat st k in dom F2 holds
F2 . k = H1(k) from FINSEQ_1:sch 2();
A23: dom F2 = dom F1 by A21, FINSEQ_3:29;
A24: Seg (len F1) = dom F1 by FINSEQ_1:def 3;
now :: thesis: for y being object st y in rng F2 holds
y in C
A25: C is_stable_under_the_action_of the action of G by A17, Def2;
let y be object ; :: thesis: ( y in rng F2 implies b1 in C )
assume y in rng F2 ; :: thesis: b1 in C
then consider x being object such that
A26: x in dom F2 and
A27: y = F2 . x by FUNCT_1:def 3;
A28: x in Seg (len F1) by A21, A26, FINSEQ_1:def 3;
reconsider x = x as Element of NAT by A26;
A29: F2 . x = (G ^ o) . (F1 . x) by A22, A26;
A30: F1 . x in rng F1 by A24, A28, FUNCT_1:3;
per cases ( O <> {} or O = {} ) ;
suppose A31: O <> {} ; :: thesis: b1 in C
set f = the action of G . o;
A32: G ^ o = the action of G . o by A31, Def6;
then reconsider f = the action of G . o as Function of G,G ;
dom f = the carrier of G by FUNCT_2:def 1;
then A33: y in f .: C by A20, A27, A29, A30, A32, FUNCT_1:def 6;
f .: C c= C by A25, A31;
hence y in C by A33; :: thesis: verum
end;
suppose O = {} ; :: thesis: b1 in C
then G ^ o = id the carrier of G by Def6;
then (G ^ o) . (F1 . x) = F1 . x by A30, FUNCT_1:18;
hence y in C by A20, A27, A29, A30; :: thesis: verum
end;
end;
end;
then A34: rng F2 c= C ;
then rng F2 c= the carrier of G by XBOOLE_1:1;
then reconsider F2 = F2 as FinSequence of the carrier of G by FINSEQ_1:def 4;
(G ^ o) . c = Product (F2 |^ I1) by A18, A19, A21, A22, A23, Lm23;
hence (G ^ o) . c in B by A17, A19, A21, A34; :: thesis: verum
end;
A35: now :: thesis: for c being Element of G st c in B holds
c " in B
let c be Element of G; :: thesis: ( c in B implies c " in B )
assume c in B ; :: thesis: c " in B
then ex d1 being Element of G st
( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & d1 = Product (F |^ I) & len F = len I & rng F c= C ) ) ;
then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT , C being Subset of G such that
A36: ( C = the_stable_subset_generated_by (A, the action of G) & c = Product (F1 |^ I1) ) and
A37: len F1 = len I1 and
A38: rng F1 c= C ;
deffunc H1( Nat) -> set = F1 . (((len F1) - $1) + 1);
consider F2 being FinSequence such that
A39: len F2 = len F1 and
A40: for k being Nat st k in dom F2 holds
F2 . k = H1(k) from FINSEQ_1:sch 2();
A41: Seg (len I1) = dom I1 by FINSEQ_1:def 3;
A42: rng F2 c= rng F1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F2 or x in rng F1 )
assume x in rng F2 ; :: thesis: x in rng F1
then consider y being object such that
A43: y in dom F2 and
A44: F2 . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A43;
reconsider n = ((len F1) - y) + 1 as Element of NAT by A39, A43, Lm22;
( 1 <= n & n <= len F1 ) by A39, A43, Lm22;
then A45: n in dom F1 by FINSEQ_3:25;
x = F1 . (((len F1) - y) + 1) by A40, A43, A44;
hence x in rng F1 by A45, FUNCT_1:def 3; :: thesis: verum
end;
then A46: rng F2 c= C by A38;
set p = F1 |^ I1;
A47: Seg (len F1) = dom F1 by FINSEQ_1:def 3;
A48: len (F1 |^ I1) = len F1 by GROUP_4:def 3;
defpred S2[ Nat, object ] means ex i being Integer st
( i = I1 . (((len I1) - $1) + 1) & $2 = - i );
A49: for k being Nat st k in Seg (len I1) holds
ex x being object st S2[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len I1) implies ex x being object st S2[k,x] )
assume k in Seg (len I1) ; :: thesis: ex x being object st S2[k,x]
then A50: k in dom I1 by FINSEQ_1:def 3;
then reconsider n = ((len I1) - k) + 1 as Element of NAT by Lm22;
( 1 <= n & n <= len I1 ) by A50, Lm22;
then n in dom I1 by FINSEQ_3:25;
then I1 . n in rng I1 by FUNCT_1:def 3;
then reconsider i = I1 . n as Element of INT ;
take - i ; :: thesis: S2[k, - i]
take i ; :: thesis: ( i = I1 . (((len I1) - k) + 1) & - i = - i )
thus ( i = I1 . (((len I1) - k) + 1) & - i = - i ) ; :: thesis: verum
end;
consider I2 being FinSequence such that
A51: dom I2 = Seg (len I1) and
A52: for k being Nat st k in Seg (len I1) holds
S2[k,I2 . k] from FINSEQ_1:sch 1(A49);
A53: len F2 = len I2 by A37, A39, A51, FINSEQ_1:def 3;
A54: rng I2 c= INT
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng I2 or x in INT )
assume x in rng I2 ; :: thesis: x in INT
then consider y being object such that
A55: y in dom I2 and
A56: x = I2 . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A55;
ex i being Integer st
( i = I1 . (((len I1) - y) + 1) & x = - i ) by A51, A52, A55, A56;
hence x in INT by INT_1:def 2; :: thesis: verum
end;
A57: rng F2 c= the carrier of G by A42, XBOOLE_1:1;
A58: dom F2 = dom I2 by A37, A39, A51, FINSEQ_1:def 3;
reconsider I2 = I2 as FinSequence of INT by A54, FINSEQ_1:def 4;
reconsider F2 = F2 as FinSequence of the carrier of G by A57, FINSEQ_1:def 4;
set q = F2 |^ I2;
A59: len (F2 |^ I2) = len F2 by GROUP_4:def 3;
then A60: dom (F2 |^ I2) = dom F2 by FINSEQ_3:29;
A61: dom F1 = dom I1 by A37, FINSEQ_3:29;
now :: thesis: for k being Nat st k in dom (F2 |^ I2) holds
((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1)
let k be Nat; :: thesis: ( k in dom (F2 |^ I2) implies ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1) )
A62: I2 /. k = @ (I2 /. k) ;
assume A63: k in dom (F2 |^ I2) ; :: thesis: ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1)
then reconsider n = ((len (F1 |^ I1)) - k) + 1 as Element of NAT by A39, A48, A59, Lm22;
A64: ( I1 /. n = @ (I1 /. n) & (F2 |^ I2) /. k = (F2 |^ I2) . k ) by A63, PARTFUN1:def 6;
A65: ( F2 /. k = F2 . k & F2 . k = F1 . n ) by A40, A48, A60, A63, PARTFUN1:def 6;
( 1 <= n & len (F1 |^ I1) >= n ) by A39, A48, A59, A63, Lm22;
then A66: n in dom I2 by A37, A51, A48;
then A67: I1 . n = I1 /. n by A51, A41, PARTFUN1:def 6;
dom (F2 |^ I2) = dom I1 by A37, A39, A59, FINSEQ_3:29;
then consider i being Integer such that
A68: i = I1 . n and
A69: I2 . k = - i by A37, A52, A41, A48, A63;
I2 . k = I2 /. k by A58, A60, A63, PARTFUN1:def 6;
then A70: (F2 |^ I2) . k = (F2 /. k) |^ (- i) by A60, A63, A69, A62, GROUP_4:def 3;
F1 /. n = F1 . n by A37, A47, A51, A66, PARTFUN1:def 6;
then (F2 |^ I2) . k = ((F1 /. n) |^ i) " by A70, A65, GROUP_1:36;
hence ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1) by A61, A51, A41, A66, A68, A67, A64, GROUP_4:def 3; :: thesis: verum
end;
then (Product (F1 |^ I1)) " = Product (F2 |^ I2) by A39, A48, A59, GROUP_4:14;
hence c " in B by A36, A53, A46; :: thesis: verum
end;
A71: ( rng (<*> the carrier of G) = {} & {} c= the_stable_subset_generated_by (A, the action of G) ) ;
( 1_ G = Product (<*> the carrier of G) & (<*> the carrier of G) |^ (<*> INT) = {} ) by GROUP_4:8, GROUP_4:21;
then 1_ G in B by A71;
then consider H being strict StableSubgroup of G such that
A72: the carrier of H = B by A3, A35, A16, Lm14;
A c= B
proof
set C = the_stable_subset_generated_by (A, the action of G);
reconsider p = 1 as Integer ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume A73: x in A ; :: thesis: x in B
then reconsider a = x as Element of G ;
A c= the_stable_subset_generated_by (A, the action of G) by Def2;
then A74: ( rng <*a*> = {a} & {a} c= the_stable_subset_generated_by (A, the action of G) ) by A73, FINSEQ_1:39, ZFMISC_1:31;
A75: Product (<*a*> |^ <*(@ p)*>) = Product <*(a |^ 1)*> by GROUP_4:22
.= a |^ 1 by GROUP_4:9
.= a by GROUP_1:26 ;
( len <*a*> = 1 & len <*(@ p)*> = 1 ) by FINSEQ_1:39;
hence x in B by A75, A74; :: thesis: verum
end;
then the_stable_subgroup_of A is StableSubgroup of H by A72, Def26;
then the_stable_subgroup_of A is Subgroup of H by Def7;
then g1 in H by A2, GROUP_2:40;
then g1 in B by A72, STRUCT_0:def 5;
then ex b being Element of G st
( b = g1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & b = Product (F |^ I) & len F = len I & rng F c= C ) ) ;
hence ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) ; :: thesis: verum
end;
given F being FinSequence of the carrier of G, I being FinSequence of INT , C being Subset of G such that A76: C = the_stable_subset_generated_by (A, the action of G) and
len F = len I and
A77: rng F c= C and
A78: Product (F |^ I) = g1 ; :: thesis: g1 in the_stable_subgroup_of A
the_stable_subgroup_of A is Subgroup of G by Def7;
then reconsider Y = the carrier of (the_stable_subgroup_of A) as Subset of G by GROUP_2:def 5;
now :: thesis: for o being Element of O
for f being Function of G,G st o in O & f = the action of G . o holds
f .: Y c= Y
let o be Element of O; :: thesis: for f being Function of G,G st o in O & f = the action of G . o holds
f .: Y c= Y
let f be Function of G,G; :: thesis: ( o in O & f = the action of G . o implies f .: Y c= Y )
assume A79: o in O ; :: thesis: ( f = the action of G . o implies f .: Y c= Y )
assume A80: f = the action of G . o ; :: thesis: f .: Y c= Y
now :: thesis: for y being object st y in f .: Y holds
y in Y
let y be object ; :: thesis: ( y in f .: Y implies y in Y )
assume y in f .: Y ; :: thesis: y in Y
then consider x being object such that
A81: x in dom f and
A82: x in Y and
A83: y = f . x by FUNCT_1:def 6;
reconsider x = x as Element of G by A81;
x in the_stable_subgroup_of A by A82, STRUCT_0:def 5;
then (G ^ o) . x in the_stable_subgroup_of A by Lm9;
then f . x in the_stable_subgroup_of A by A79, A80, Def6;
hence y in Y by A83, STRUCT_0:def 5; :: thesis: verum
end;
hence f .: Y c= Y ; :: thesis: verum
end;
then A84: Y is_stable_under_the_action_of the action of G ;
reconsider H9 = the_stable_subgroup_of A as Subgroup of G by Def7;
C c= the carrier of H9 by A76, A1, A84, Def2;
then rng F c= carr H9 by A77;
hence g1 in the_stable_subgroup_of A by A78, GROUP_4:20; :: thesis: verum