let O be set ; :: thesis: for G being GroupWithOperators of O
for A, B being Subset of G st A c= B holds
the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B
let G be GroupWithOperators of O; :: thesis: for A, B being Subset of G st A c= B holds
the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B
let A, B be Subset of G; :: thesis: ( A c= B implies the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B )
assume A1: A c= B ; :: thesis: the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B
per cases ( A is empty or not A is empty ) ;
suppose A2: A is empty ; :: thesis: the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B
reconsider H1 = (1). G, H2 = (1). (the_stable_subgroup_of B) as strict StableSubgroup of G by Th11;
the carrier of H1 = {(1_ G)} by Def8
.= {(1_ (the_stable_subgroup_of B))} by Th4
.= the carrier of H2 by Def8 ;
then (1). G = (1). (the_stable_subgroup_of B) by Lm4;
hence the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B by A2, Lm24; :: thesis: verum
end;
suppose A3: not A is empty ; :: thesis: the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B
now :: thesis: for a being Element of G st a in the_stable_subgroup_of A holds
a in the_stable_subgroup_of B
set D = the_stable_subset_generated_by (B, the action of G);
let a be Element of G; :: thesis: ( a in the_stable_subgroup_of A implies a in the_stable_subgroup_of B )
assume a in the_stable_subgroup_of A ; :: thesis: a in the_stable_subgroup_of B
then consider F being FinSequence of the carrier of G, I being FinSequence of INT , C being Subset of G such that
A4: C = the_stable_subset_generated_by (A, the action of G) and
A5: len F = len I and
A6: rng F c= C and
A7: Product (F |^ I) = a by Th24;
now :: thesis: for y being object st y in C holds
y in the_stable_subset_generated_by (B, the action of G)
let y be object ; :: thesis: ( y in C implies y in the_stable_subset_generated_by (B, the action of G) )
assume A8: y in C ; :: thesis: y in the_stable_subset_generated_by (B, the action of G)
then reconsider b = y as Element of G ;
consider F1 being FinSequence of O, x being Element of A such that
A9: (Product (F1, the action of G)) . x = b by A3, A4, A8, Lm30;
x in A by A3;
hence y in the_stable_subset_generated_by (B, the action of G) by A1, A9, Lm30; :: thesis: verum
end;
then C c= the_stable_subset_generated_by (B, the action of G) ;
then rng F c= the_stable_subset_generated_by (B, the action of G) by A6;
hence a in the_stable_subgroup_of B by A5, A7, Th24; :: thesis: verum
end;
hence the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B by Th13; :: thesis: verum
end;
end;