let G be Group; :: thesis: for H being Subgroup of G st Left_Cosets H is finite & index H = 2 holds
H is normal Subgroup of G
let H be Subgroup of G; :: thesis: ( Left_Cosets H is finite & index H = 2 implies H is normal Subgroup of G )
assume that
A1: Left_Cosets H is finite and
A2: index H = 2 ; :: thesis: H is normal Subgroup of G
consider B being finite set such that
A3: ( B = Left_Cosets H & index H = card B ) by A1, GROUP_2:176;
consider C being finite set such that
A4: ( C = Right_Cosets H & index H = card C ) by A1, GROUP_2:176;
consider x, y being set such that
A5: x <> y and
A6: Left_Cosets H = {x,y} by A2, A3, CARD_2:79;
consider z1, z2 being set such that
A7: z1 <> z2 and
A8: Right_Cosets H = {z1,z2} by A2, A4, CARD_2:79;
A9: ( carr H in Left_Cosets H & carr H in Right_Cosets H ) by GROUP_2:165;
then ( {x,y} = {x,(carr H)} or {x,y} = {(carr H),y} ) by A6, TARSKI:def 2;
then consider z3 being set such that
A10: {x,y} = {(carr H),z3} ;
( {z1,z2} = {z1,(carr H)} or {z1,z2} = {(carr H),z2} ) by A8, A9, TARSKI:def 2;
then consider z4 being set such that
A11: {z1,z2} = {(carr H),z4} ;
A12: ( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G ) by GROUP_2:167;
A13: union (Left_Cosets H) = (carr H) \/ z3 by A6, A10, ZFMISC_1:93;
carr H misses z3

proof

assume A14: not carr H misses z3 ; :: thesis: contradiction
z3 in Left_Cosets H by A6, A10, TARSKI:def 2;
then A15: ex a being Element of G st z3 = a * H by GROUP_2:def 15;
carr H = (1_ G) * H by GROUP_2:132;
then carr H = z3 by A14, A15, GROUP_2:138;
then {x,y} = {(carr H)} by A10, ENUMSET1:69;
then ( x = carr H & y = carr H ) by ZFMISC_1:8;
hence contradiction by A5; :: thesis: verum

end;

then A16: z3 = the carrier of G \ (carr H) by A12, A13, XBOOLE_1:88;
A17: union (Right_Cosets H) = (carr H) \/ z4 by A8, A11, ZFMISC_1:93;
A18: carr H misses z4

proof

assume A19: not carr H misses z4 ; :: thesis: contradiction
z4 in Right_Cosets H by A8, A11, TARSKI:def 2;
then A20: ex a being Element of G st z4 = H * a by GROUP_2:def 16;
carr H = H * (1_ G) by GROUP_2:132;
then carr H = z4 by A19, A20, GROUP_2:144;
then {z1,z2} = {(carr H)} by A11, ENUMSET1:69;
then ( z1 = carr H & z2 = carr H ) by ZFMISC_1:8;
hence contradiction by A7; :: thesis: verum

end;

now

let c be Element of G; :: thesis: c * H = H * c

now

per cases ( c * H = carr H or c * H <> carr H ) ;

suppose A21: c * H = carr H ; :: thesis: c * H = H * c

then c in H by GROUP_2:136;
hence c * H = H * c by A21, GROUP_2:142; :: thesis: verum

end;

suppose A22: c * H <> carr H ; :: thesis: c * H = H * c

then not c in H by GROUP_2:136;
then A23: H * c <> carr H by GROUP_2:142;
( c * H in Left_Cosets H & H * c in Right_Cosets H ) by GROUP_2:def 15, GROUP_2:def 16;
then ( c * H = z3 & H * c = z4 ) by A6, A8, A10, A11, A22, A23, TARSKI:def 2;
hence c * H = H * c by A12, A16, A17, A18, XBOOLE_1:88; :: thesis: verum

end;

end;

end;

hence c * H = H * c ; :: thesis: verum

end;

hence H is normal Subgroup of G by Th140; :: thesis: verum