let G be addGroup; 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; ( 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
; H is normal Subgroup of G
ex B being finite set st
( B = Left_Cosets H & index H = card B )
by A1, Th146;
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 Th135;
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
( union (Left_Cosets H) = the carrier of G & union (Left_Cosets H) = (carr H) \/ z3 )
by A4, A5, Th137, ZFMISC_1:75;
then A10:
( union (Right_Cosets H) = the carrier of G & z3 = the carrier of G \ (carr H) )
by A6, Th137, XBOOLE_1:88;
ex C being finite set st
( C = Right_Cosets H & index H = card C )
by A1, Th146;
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 Th135;
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
A18:
union (Right_Cosets H) = (carr H) \/ z4
by A12, A13, ZFMISC_1:75;
now for c being Element of G holds c + H = H + clet c be
Element of
G;
c + H = H + cnow c + H = H + cper cases
( c + H = carr H or c + H <> carr H )
;
suppose A20:
c + H <> carr H
;
c + H = H + cthen A21:
H + c <> carr H
by Th113, Th119;
c + H in Left_Cosets H
by Def15;
then A22:
c + H = z3
by A4, A5, A20, TARSKI:def 2;
H + c in Right_Cosets H
by Def16;
then
H + c = z4
by A12, A13, A21, TARSKI:def 2;
hence
c + H = H + c
by A10, A18, A14, A22, XBOOLE_1:88;
verum end; hence
c + H = H + c
;
verum end;
hence
H is normal Subgroup of G
by Th117; verum