let O be set ; 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; 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; ( A c= B implies the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B )
assume A1:
A c= B
; the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B
per cases
( A is empty or not A is empty )
;
suppose A3:
not
A is
empty
;
the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of Bnow for a being Element of G st a in the_stable_subgroup_of A holds
a in the_stable_subgroup_of Bset D =
the_stable_subset_generated_by (
B, the
action of
G);
let a be
Element of
G;
( a in the_stable_subgroup_of A implies a in the_stable_subgroup_of B )assume
a in the_stable_subgroup_of A
;
a in the_stable_subgroup_of Bthen 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 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 ;
( y in C implies y in the_stable_subset_generated_by (B, the action of G) )assume A8:
y in C
;
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;
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;
verum end; hence
the_stable_subgroup_of A is
StableSubgroup of
the_stable_subgroup_of B
by Th13;
verum end; end;