let O be set ; for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of H1
for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 "\/" N29 = N1 "\/" N2
let G be GroupWithOperators of O; for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of H1
for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 "\/" N29 = N1 "\/" N2
let H1 be StableSubgroup of G; for N1, N2 being strict StableSubgroup of H1
for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 "\/" N29 = N1 "\/" N2
let N1, N2 be strict StableSubgroup of H1; for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 "\/" N29 = N1 "\/" N2
reconsider S2 = the_stable_subgroup_of (N1 * N2) as StableSubgroup of G by Th11;
let N19, N29 be strict StableSubgroup of G; ( N1 = N19 & N2 = N29 implies N19 "\/" N29 = N1 "\/" N2 )
set S1 = the_stable_subgroup_of (N19 * N29);
set X1 = { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & N19 * N29 c= carr H ) } ;
set X2 = { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st
( B = the carrier of H & N1 * N2 c= carr H ) } ;
A1:
( N19 "\/" N29 = the_stable_subgroup_of (N19 * N29) & N1 "\/" N2 = the_stable_subgroup_of (N1 * N2) )
by Th29;
A2:
( the carrier of (the_stable_subgroup_of (N19 * N29)) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & N19 * N29 c= carr H ) } & the carrier of (the_stable_subgroup_of (N1 * N2)) = meet { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st
( B = the carrier of H & N1 * N2 c= carr H ) } )
by Th27;
assume A3:
( N1 = N19 & N2 = N29 )
; N19 "\/" N29 = N1 "\/" N2
then A7:
{ B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st
( B = the carrier of H & N1 * N2 c= carr H ) } c= { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & N19 * N29 c= carr H ) }
;
then A8:
meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & N19 * N29 c= carr H ) } c= meet { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st
( B = the carrier of H & N1 * N2 c= carr H ) }
by A7, SETFAM_1:6;
now for x being object st x in the carrier of (the_stable_subgroup_of (N1 * N2)) holds
x in the carrier of (the_stable_subgroup_of (N19 * N29))let x be
object ;
( x in the carrier of (the_stable_subgroup_of (N1 * N2)) implies x in the carrier of (the_stable_subgroup_of (N19 * N29)) )assume A9:
x in the
carrier of
(the_stable_subgroup_of (N1 * N2))
;
x in the carrier of (the_stable_subgroup_of (N19 * N29))
the_stable_subgroup_of (N1 * N2) is
Subgroup of
H1
by Def7;
then
the
carrier of
(the_stable_subgroup_of (N1 * N2)) c= the
carrier of
H1
by GROUP_2:def 5;
then reconsider g =
x as
Element of
H1 by A9;
g in the_stable_subgroup_of (N1 * N2)
by A9, STRUCT_0:def 5;
then consider F being
FinSequence of the
carrier of
H1,
I being
FinSequence of
INT ,
C being
Subset of
H1 such that A10:
C = the_stable_subset_generated_by (
(N1 * N2), the
action of
H1)
and A11:
len F = len I
and A12:
rng F c= C
and A13:
Product (F |^ I) = g
by Th24;
now for x being object st x in the_stable_subset_generated_by ((N1 * N2), the action of H1) holds
x in the_stable_subset_generated_by ((N19 * N29), the action of G)
N2 is
Subgroup of
H1
by Def7;
then
1_ H1 in N2
by GROUP_2:46;
then A14:
1_ H1 in carr N2
by STRUCT_0:def 5;
let x be
object ;
( x in the_stable_subset_generated_by ((N1 * N2), the action of H1) implies x in the_stable_subset_generated_by ((N19 * N29), the action of G) )assume A15:
x in the_stable_subset_generated_by (
(N1 * N2), the
action of
H1)
;
x in the_stable_subset_generated_by ((N19 * N29), the action of G)then reconsider a =
x as
Element of
H1 ;
N1 is
Subgroup of
H1
by Def7;
then
1_ H1 in N1
by GROUP_2:46;
then A16:
1_ H1 in carr N1
by STRUCT_0:def 5;
1_ H1 = (1_ H1) * (1_ H1)
by GROUP_1:def 4;
then A17:
1_ H1 in (carr N1) * (carr N2)
by A16, A14;
then consider F being
FinSequence of
O,
h being
Element of
N1 * N2 such that A18:
(Product (F, the action of H1)) . h = a
by A15, Lm30;
H1 is
Subgroup of
G
by Def7;
then A19:
the
carrier of
H1 c= the
carrier of
G
by GROUP_2:def 5;
then reconsider a =
a as
Element of
G ;
A20:
h in N1 * N2
by A17;
reconsider h =
h as
Element of
N19 * N29 by A3, Th85;
then
Product (
F, the
action of
H1)
= (Product (F, the action of G)) | the
carrier of
H1
by A19, Th84;
then A23:
(Product (F, the action of G)) . h = a
by A18, A20, FUNCT_1:49;
not
N19 * N29 is
empty
by A3, A20, Th85;
hence
x in the_stable_subset_generated_by (
(N19 * N29), the
action of
G)
by A23, Lm30;
verum end; then
the_stable_subset_generated_by (
(N1 * N2), the
action of
H1)
c= the_stable_subset_generated_by (
(N19 * N29), the
action of
G)
;
then A24:
rng F c= the_stable_subset_generated_by (
(N19 * N29), the
action of
G)
by A10, A12;
reconsider g =
g as
Element of
G by Th2;
H1 is
Subgroup of
G
by Def7;
then
the
carrier of
H1 c= the
carrier of
G
by GROUP_2:def 5;
then
rng F c= the
carrier of
G
;
then reconsider F =
F as
FinSequence of the
carrier of
G by FINSEQ_1:def 4;
Product (F |^ I) = g
by A11, A13, Th83;
then A25:
g in the_stable_subgroup_of (N19 * N29)
by A11, A24, Th24;
assume
not
x in the
carrier of
(the_stable_subgroup_of (N19 * N29))
;
contradictionhence
contradiction
by A25, STRUCT_0:def 5;
verum end;
then
meet { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st
( B = the carrier of H & N1 * N2 c= carr H ) } c= meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & N19 * N29 c= carr H ) }
by A2;
then
the carrier of (the_stable_subgroup_of (N19 * N29)) = the carrier of S2
by A2, A8, XBOOLE_0:def 10;
hence
N19 "\/" N29 = N1 "\/" N2
by A1, Lm4; verum