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
ex B being finite set st
( B = Left_Cosets H & index H = card B ) by A1, GROUP_2:146;
then consider x, y being object such that
A3: x <> y and
A4: Left_Cosets H = {x,y} by A2, CARD_2:60;
carr H in Left_Cosets H by GROUP_2:135;
then ( {x,y} = {x,(carr H)} or {x,y} = {(carr H),y} ) by A4, TARSKI:def 2;
then consider z3 being object such that
A5: {x,y} = {(carr H),z3} ;
reconsider z3 = z3 as set by TARSKI:1;
A6: carr H misses z3

proof

z3 in Left_Cosets H by A4, A5, TARSKI:def 2;
then A7: ex a being Element of G st z3 = a * H by GROUP_2:def 15;
A8: carr H = (1_ G) * H by GROUP_2:109;
assume not carr H misses z3 ; :: thesis: contradiction
then carr H = z3 by A7, A8, GROUP_2:115;
then A9: {x,y} = {(carr H)} by A5, ENUMSET1:29;
then x = carr H by ZFMISC_1:4;
hence contradiction by A3, A9, ZFMISC_1:4; :: thesis: verum

end;

( union (Left_Cosets H) = the carrier of G & union (Left_Cosets H) = (carr H) \/ z3 ) by A4, A5, GROUP_2:137, ZFMISC_1:75;
then A10: ( union (Right_Cosets H) = the carrier of G & z3 = the carrier of G \ (carr H) ) by A6, GROUP_2:137, XBOOLE_1:88;
ex C being finite set st
( C = Right_Cosets H & index H = card C ) by A1, GROUP_2:146;
then consider z1, z2 being object such that
A11: z1 <> z2 and
A12: Right_Cosets H = {z1,z2} by A2, CARD_2:60;
carr H in Right_Cosets H by GROUP_2:135;
then ( {z1,z2} = {z1,(carr H)} or {z1,z2} = {(carr H),z2} ) by A12, TARSKI:def 2;
then consider z4 being object such that
A13: {z1,z2} = {(carr H),z4} ;
reconsider z4 = z4 as set by TARSKI:1;
A14: carr H misses z4

proof

z4 in Right_Cosets H by A12, A13, TARSKI:def 2;
then A15: ex a being Element of G st z4 = H * a by GROUP_2:def 16;
A16: carr H = H * (1_ G) by GROUP_2:109;
assume not carr H misses z4 ; :: thesis: contradiction
then carr H = z4 by A15, A16, GROUP_2:121;
then A17: {z1,z2} = {(carr H)} by A13, ENUMSET1:29;
then z1 = carr H by ZFMISC_1:4;
hence contradiction by A11, A17, ZFMISC_1:4; :: thesis: verum

end;

A18: union (Right_Cosets H) = (carr H) \/ z4 by A12, A13, ZFMISC_1:75;

now :: thesis: for c being Element of G holds c * H = H * c

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

now :: thesis: c * H = H * c

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

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

then c in H by GROUP_2:113;
hence c * H = H * c by A19, GROUP_2:119; :: thesis: verum

end;

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

then not c in H by GROUP_2:113;
then A21: H * c <> carr H by GROUP_2:119;
c * H in Left_Cosets H by GROUP_2:def 15;
then A22: c * H = z3 by A4, A5, A20, TARSKI:def 2;
H * c in Right_Cosets H by GROUP_2:def 16;
then H * c = z4 by A12, A13, A21, TARSKI:def 2;
hence c * H = H * c by A10, A18, A14, A22, XBOOLE_1:88; :: thesis: verum

end;

end;

end;

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

end;

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