let O be set ; for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st (carr H1) * (carr H2) = (carr H2) * (carr H1) holds
ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2)
let G be GroupWithOperators of O; for H1, H2 being StableSubgroup of G st (carr H1) * (carr H2) = (carr H2) * (carr H1) holds
ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2)
let H1, H2 be StableSubgroup of G; ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2) )
assume A1:
(carr H1) * (carr H2) = (carr H2) * (carr H1)
; ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2)
A7:
H2 is Subgroup of G
by Def7;
A8:
H1 is Subgroup of G
by Def7;
A9:
now for g being Element of G st g in (carr H1) * (carr H2) holds
g " in (carr H1) * (carr H2)let g be
Element of
G;
( g in (carr H1) * (carr H2) implies g " in (carr H1) * (carr H2) )assume A10:
g in (carr H1) * (carr H2)
;
g " in (carr H1) * (carr H2)then consider a,
b being
Element of
G such that A11:
g = a * b
and
a in carr H1
and
b in carr H2
;
consider b1,
a1 being
Element of
G such that A12:
a * b = b1 * a1
and A13:
b1 in carr H2
and A14:
a1 in carr H1
by A1, A10, A11;
b1 in H2
by A13, STRUCT_0:def 5;
then
b1 " in H2
by A7, GROUP_2:51;
then A15:
b1 " in carr H2
by STRUCT_0:def 5;
a1 in H1
by A14, STRUCT_0:def 5;
then
a1 " in H1
by A8, GROUP_2:51;
then A16:
a1 " in carr H1
by STRUCT_0:def 5;
g " = (a1 ") * (b1 ")
by A11, A12, GROUP_1:17;
hence
g " in (carr H1) * (carr H2)
by A16, A15;
verum end;
A17:
now for g1, g2 being Element of G st g1 in (carr H1) * (carr H2) & g2 in (carr H1) * (carr H2) holds
g1 * g2 in (carr H1) * (carr H2)let g1,
g2 be
Element of
G;
( g1 in (carr H1) * (carr H2) & g2 in (carr H1) * (carr H2) implies g1 * g2 in (carr H1) * (carr H2) )assume that A18:
g1 in (carr H1) * (carr H2)
and A19:
g2 in (carr H1) * (carr H2)
;
g1 * g2 in (carr H1) * (carr H2)consider a1,
b1 being
Element of
G such that A20:
g1 = a1 * b1
and A21:
a1 in carr H1
and A22:
b1 in carr H2
by A18;
consider a2,
b2 being
Element of
G such that A23:
g2 = a2 * b2
and A24:
a2 in carr H1
and A25:
b2 in carr H2
by A19;
b1 * a2 in (carr H1) * (carr H2)
by A1, A22, A24;
then consider a,
b being
Element of
G such that A26:
b1 * a2 = a * b
and A27:
a in carr H1
and A28:
b in carr H2
;
A29:
a in H1
by A27, STRUCT_0:def 5;
A30:
b in H2
by A28, STRUCT_0:def 5;
b2 in H2
by A25, STRUCT_0:def 5;
then
b * b2 in H2
by A7, A30, GROUP_2:50;
then A31:
b * b2 in carr H2
by STRUCT_0:def 5;
a1 in H1
by A21, STRUCT_0:def 5;
then
a1 * a in H1
by A8, A29, GROUP_2:50;
then A32:
a1 * a in carr H1
by STRUCT_0:def 5;
g1 * g2 =
((a1 * b1) * a2) * b2
by A20, A23, GROUP_1:def 3
.=
(a1 * (b1 * a2)) * b2
by GROUP_1:def 3
;
then g1 * g2 =
((a1 * a) * b) * b2
by A26, GROUP_1:def 3
.=
(a1 * a) * (b * b2)
by GROUP_1:def 3
;
hence
g1 * g2 in (carr H1) * (carr H2)
by A32, A31;
verum end;
(carr H1) * (carr H2) <> {}
by GROUP_2:9;
hence
ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2)
by A17, A9, A2, Lm14; verum