let O be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( (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) ; :: thesis: ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2)
A2: now :: thesis: for o being Element of O
for g being Element of G st g in (carr H1) * (carr H2) holds
(G ^ o) . g in (carr H1) * (carr H2)
let o be Element of O; :: thesis: for g being Element of G st g in (carr H1) * (carr H2) holds
(G ^ o) . g in (carr H1) * (carr H2)
let g be Element of G; :: thesis: ( g in (carr H1) * (carr H2) implies (G ^ o) . g in (carr H1) * (carr H2) )
assume g in (carr H1) * (carr H2) ; :: thesis: (G ^ o) . g in (carr H1) * (carr H2)
then consider a, b being Element of G such that
A3: g = a * b and
A4: a in carr H1 and
A5: b in carr H2 ;
a in H1 by A4, STRUCT_0:def 5;
then (G ^ o) . a in H1 by Lm9;
then A6: (G ^ o) . a in carr H1 by STRUCT_0:def 5;
b in H2 by A5, STRUCT_0:def 5;
then (G ^ o) . b in H2 by Lm9;
then (G ^ o) . b in carr H2 by STRUCT_0:def 5;
then ((G ^ o) . a) * ((G ^ o) . b) in (carr H1) * (carr H2) by A6;
hence (G ^ o) . g in (carr H1) * (carr H2) by A3, GROUP_6:def 6; :: thesis: verum
end;
A7: H2 is Subgroup of G by Def7;
A8: H1 is Subgroup of G by Def7;
A9: now :: thesis: 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; :: thesis: ( g in (carr H1) * (carr H2) implies g " in (carr H1) * (carr H2) )
assume A10: g in (carr H1) * (carr H2) ; :: thesis: 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; :: thesis: verum
end;
A17: now :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: thesis: 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; :: thesis: verum