let G be Group; :: thesis: for H1, H2 being Subgroup of G holds

( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )

let H1, H2 be Subgroup of G; :: thesis: ( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )

thus ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) :: thesis: ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) )

thus (carr H1) * (carr H2) c= (carr H2) * (carr H1) :: according to XBOOLE_0:def 10 :: thesis: (carr H2) * (carr H1) c= (carr H1) * (carr H2)

assume A27: x in (carr H2) * (carr H1) ; :: thesis: x in (carr H1) * (carr H2)

then reconsider y = x as Element of G ;

consider a, b being Element of G such that

A28: ( x = a * b & a in carr H2 ) and

A29: b in carr H1 by A27;

hence x in (carr H1) * (carr H2) by A22; :: thesis: verum

( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )

let H1, H2 be Subgroup of G; :: thesis: ( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )

thus ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) :: thesis: ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) )

proof

given H being Subgroup of G such that A22:
the carrier of H = (carr H1) * (carr H2)
; :: thesis: (carr H1) * (carr H2) = (carr H2) * (carr H1)
assume A1:
(carr H1) * (carr H2) = (carr H2) * (carr H1)
; :: thesis: ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)

hence ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) by A8, A2, Th52; :: thesis: verum

end;A2: now :: thesis: for g being Element of G st g in (carr H1) * (carr H2) holds

g " in (carr H1) * (carr H2)

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 A3: g in (carr H1) * (carr H2) ; :: thesis: g " in (carr H1) * (carr H2)

then consider a, b being Element of G such that

A4: g = a * b and

a in carr H1 and

b in carr H2 ;

consider b1, a1 being Element of G such that

A5: a * b = b1 * a1 and

A6: ( b1 in carr H2 & a1 in carr H1 ) by A1, A3, A4;

A7: ( a1 " in carr H1 & b1 " in carr H2 ) by A6, Th75;

g " = (a1 ") * (b1 ") by A4, A5, GROUP_1:17;

hence g " in (carr H1) * (carr H2) by A7; :: thesis: verum

end;assume A3: g in (carr H1) * (carr H2) ; :: thesis: g " in (carr H1) * (carr H2)

then consider a, b being Element of G such that

A4: g = a * b and

a in carr H1 and

b in carr H2 ;

consider b1, a1 being Element of G such that

A5: a * b = b1 * a1 and

A6: ( b1 in carr H2 & a1 in carr H1 ) by A1, A3, A4;

A7: ( a1 " in carr H1 & b1 " in carr H2 ) by A6, Th75;

g " = (a1 ") * (b1 ") by A4, A5, GROUP_1:17;

hence g " in (carr H1) * (carr H2) by A7; :: thesis: verum

A8: 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)

(carr H1) * (carr H2) <> {}
by Th9;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

A9: g1 in (carr H1) * (carr H2) and

A10: g2 in (carr H1) * (carr H2) ; :: thesis: g1 * g2 in (carr H1) * (carr H2)

consider a1, b1 being Element of G such that

A11: g1 = a1 * b1 and

A12: a1 in carr H1 and

A13: b1 in carr H2 by A9;

consider a2, b2 being Element of G such that

A14: g2 = a2 * b2 and

A15: a2 in carr H1 and

A16: b2 in carr H2 by A10;

b1 * a2 in (carr H1) * (carr H2) by A1, A13, A15;

then consider a, b being Element of G such that

A17: b1 * a2 = a * b and

A18: a in carr H1 and

A19: b in carr H2 ;

A20: b * b2 in carr H2 by A16, A19, Th74;

g1 * g2 = ((a1 * b1) * a2) * b2 by A11, A14, GROUP_1:def 3

.= (a1 * (b1 * a2)) * b2 by GROUP_1:def 3 ;

then A21: g1 * g2 = ((a1 * a) * b) * b2 by A17, GROUP_1:def 3

.= (a1 * a) * (b * b2) by GROUP_1:def 3 ;

a1 * a in carr H1 by A12, A18, Th74;

hence g1 * g2 in (carr H1) * (carr H2) by A21, A20; :: thesis: verum

end;assume that

A9: g1 in (carr H1) * (carr H2) and

A10: g2 in (carr H1) * (carr H2) ; :: thesis: g1 * g2 in (carr H1) * (carr H2)

consider a1, b1 being Element of G such that

A11: g1 = a1 * b1 and

A12: a1 in carr H1 and

A13: b1 in carr H2 by A9;

consider a2, b2 being Element of G such that

A14: g2 = a2 * b2 and

A15: a2 in carr H1 and

A16: b2 in carr H2 by A10;

b1 * a2 in (carr H1) * (carr H2) by A1, A13, A15;

then consider a, b being Element of G such that

A17: b1 * a2 = a * b and

A18: a in carr H1 and

A19: b in carr H2 ;

A20: b * b2 in carr H2 by A16, A19, Th74;

g1 * g2 = ((a1 * b1) * a2) * b2 by A11, A14, GROUP_1:def 3

.= (a1 * (b1 * a2)) * b2 by GROUP_1:def 3 ;

then A21: g1 * g2 = ((a1 * a) * b) * b2 by A17, GROUP_1:def 3

.= (a1 * a) * (b * b2) by GROUP_1:def 3 ;

a1 * a in carr H1 by A12, A18, Th74;

hence g1 * g2 in (carr H1) * (carr H2) by A21, A20; :: thesis: verum

hence ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) by A8, A2, Th52; :: thesis: verum

thus (carr H1) * (carr H2) c= (carr H2) * (carr H1) :: according to XBOOLE_0:def 10 :: thesis: (carr H2) * (carr H1) c= (carr H1) * (carr H2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (carr H2) * (carr H1) or x in (carr H1) * (carr H2) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (carr H1) * (carr H2) or x in (carr H2) * (carr H1) )

assume A23: x in (carr H1) * (carr H2) ; :: thesis: x in (carr H2) * (carr H1)

then reconsider y = x as Element of G ;

y " in carr H by A22, A23, Th75;

then consider a, b being Element of G such that

A24: y " = a * b and

A25: ( a in carr H1 & b in carr H2 ) by A22;

A26: y = (y ") "

.= (b ") * (a ") by A24, GROUP_1:17 ;

( a " in carr H1 & b " in carr H2 ) by A25, Th75;

hence x in (carr H2) * (carr H1) by A26; :: thesis: verum

end;assume A23: x in (carr H1) * (carr H2) ; :: thesis: x in (carr H2) * (carr H1)

then reconsider y = x as Element of G ;

y " in carr H by A22, A23, Th75;

then consider a, b being Element of G such that

A24: y " = a * b and

A25: ( a in carr H1 & b in carr H2 ) by A22;

A26: y = (y ") "

.= (b ") * (a ") by A24, GROUP_1:17 ;

( a " in carr H1 & b " in carr H2 ) by A25, Th75;

hence x in (carr H2) * (carr H1) by A26; :: thesis: verum

assume A27: x in (carr H2) * (carr H1) ; :: thesis: x in (carr H1) * (carr H2)

then reconsider y = x as Element of G ;

consider a, b being Element of G such that

A28: ( x = a * b & a in carr H2 ) and

A29: b in carr H1 by A27;

now :: thesis: y " in carr H

then
(y ") " in carr H
by Th75;A30:
b " in carr H1
by A29, Th75;

assume A31: not y " in carr H ; :: thesis: contradiction

( y " = (b ") * (a ") & a " in carr H2 ) by A28, Th75, GROUP_1:17;

hence contradiction by A22, A31, A30; :: thesis: verum

end;assume A31: not y " in carr H ; :: thesis: contradiction

( y " = (b ") * (a ") & a " in carr H2 ) by A28, Th75, GROUP_1:17;

hence contradiction by A22, A31, A30; :: thesis: verum

hence x in (carr H1) * (carr H2) by A22; :: thesis: verum