let G be Group; :: thesis: for H being strict Subgroup of G st Left_Cosets H is finite & index H = 2 holds
G ` is Subgroup of H
let H be strict Subgroup of G; :: thesis: ( Left_Cosets H is finite & index H = 2 implies G ` is Subgroup of H )
assume that
A1: Left_Cosets H is finite and
A2: index H = 2 ; :: thesis: G ` is Subgroup of H
A3: H is normal Subgroup of G by A1, A2, GROUP_3:151;

now

let a be Element of G; :: thesis: ( a in G ` implies a in H )
assume a in G ` ; :: thesis: a in H
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A4: len F = len I and
A5: rng F c= commutators G and
A6: a = Product (F |^ I) by Th83;
rng F c= carr H

proof

let X be set ; :: according to TARSKI:def 3 :: thesis: ( not X in rng F or X in carr H )
assume X in rng F ; :: thesis: X in carr H
then consider a, b being Element of G such that
A7: X = [.a,b.] by A5, Th65;
ex B being finite set st
( B = Left_Cosets H & index H = card B ) by A1, GROUP_2:176;
then consider x, y being set such that
x <> y and
A8: Left_Cosets H = {x,y} by A2, CARD_2:79;
x in Left_Cosets H by A8, TARSKI:def 2;
then consider d being Element of G such that
A9: x = d * H by GROUP_2:def 15;
y in Left_Cosets H by A8, TARSKI:def 2;
then consider e being Element of G such that
A10: y = e * H by GROUP_2:def 15;
carr H in Left_Cosets H by GROUP_2:165;
then ( Left_Cosets H = {(carr H),(e * H)} or Left_Cosets H = {(d * H),(carr H)} ) by A8, A9, A10, TARSKI:def 2;
then consider c being Element of G such that
A11: Left_Cosets H = {(carr H),(c * H)} ;
( a in the carrier of G & b in the carrier of G ) ;
then ( a in union (Left_Cosets H) & b in union (Left_Cosets H) ) by GROUP_2:167;
then A12: ( a in (carr H) \/ (c * H) & b in (carr H) \/ (c * H) ) by A11, ZFMISC_1:93;

now

per cases ( ( a in carr H & b in carr H ) or ( a in carr H & b in c * H ) or ( a in c * H & b in carr H ) or ( a in c * H & b in c * H ) ) by A12, XBOOLE_0:def 3;

suppose ( a in carr H & b in carr H ) ; :: thesis: X in carr H

then ( a in H & b in H ) by STRUCT_0:def 5;
then X in H by A7, Th41;
hence X in carr H by STRUCT_0:def 5; :: thesis: verum

end;

suppose ( a in carr H & b in c * H ) ; :: thesis: X in carr H

then a in H by STRUCT_0:def 5;
then ( a |^ b in H & a " in H ) by A3, Th3, GROUP_2:60;
then (a " ) * (a |^ b) in H by GROUP_2:59;
then X in H by A7, Th19;
hence X in carr H by STRUCT_0:def 5; :: thesis: verum

end;

suppose ( a in c * H & b in carr H ) ; :: thesis: X in carr H

then A13: b in H by STRUCT_0:def 5;
then b " in H by GROUP_2:60;
then (b " ) |^ a in H by A3, Th3;
then ((b " ) |^ a) * b in H by A13, GROUP_2:59;
hence X in carr H by A7, STRUCT_0:def 5; :: thesis: verum

end;

suppose A14: ( a in c * H & b in c * H ) ; :: thesis: X in carr H

then consider d being Element of G such that
A15: ( a = c * d & d in H ) by GROUP_2:125;
consider e being Element of G such that
A16: ( b = c * e & e in H ) by A14, GROUP_2:125;
A17: [.a,b.] = ((a " ) * (b " )) * (a * b) by Th19
.= (((d " ) * (c " )) * (b " )) * ((c * d) * (c * e)) by A15, A16, GROUP_1:25
.= (((d " ) * (c " )) * ((e " ) * (c " ))) * ((c * d) * (c * e)) by A16, GROUP_1:25
.= ((((d " ) * (c " )) * (e " )) * (c " )) * ((c * d) * (c * e)) by GROUP_1:def 4
.= ((((d " ) * (c " )) * (e " )) * (c " )) * (c * (d * (c * e))) by GROUP_1:def 4
.= (((((d " ) * (c " )) * (e " )) * (c " )) * c) * (d * (c * e)) by GROUP_1:def 4
.= ((((d " ) * (c " )) * (e " )) * ((c " ) * c)) * (d * (c * e)) by GROUP_1:def 4
.= ((((d " ) * (c " )) * (e " )) * (1_ G)) * (d * (c * e)) by GROUP_1:def 6
.= ((((d " ) * (c " )) * (e " )) * (c * (c " ))) * (d * (c * e)) by GROUP_1:def 6
.= (((((d " ) * (c " )) * (e " )) * c) * (c " )) * (d * (c * e)) by GROUP_1:def 4
.= ((((d " ) * ((c " ) * (e " ))) * c) * (c " )) * (d * (c * e)) by GROUP_1:def 4
.= (((d " ) * ((e " ) |^ c)) * (c " )) * (d * (c * e)) by GROUP_1:def 4
.= (((d " ) * ((e " ) |^ c)) * (c " )) * ((d * c) * e) by GROUP_1:def 4
.= ((d " ) * ((e " ) |^ c)) * ((c " ) * ((d * c) * e)) by GROUP_1:def 4
.= ((d " ) * ((e " ) |^ c)) * ((c " ) * (d * (c * e))) by GROUP_1:def 4
.= ((d " ) * ((e " ) |^ c)) * (((c " ) * d) * (c * e)) by GROUP_1:def 4
.= ((d " ) * ((e " ) |^ c)) * ((d |^ c) * e) by GROUP_1:def 4 ;
e " in H by A16, GROUP_2:60;
then ( d " in H & (e " ) |^ c in H & d |^ c in H ) by A3, A15, Th3, GROUP_2:60;
then ( (d " ) * ((e " ) |^ c) in H & (d |^ c) * e in H ) by A16, GROUP_2:59;
then X in H by A7, A17, GROUP_2:59;
hence X in carr H by STRUCT_0:def 5; :: thesis: verum

end;

end;

end;

hence X in carr H ; :: thesis: verum

end;

then a in gr (carr H) by A4, A6, GROUP_4:37;
hence a in H by GROUP_4:40; :: thesis: verum

end;

hence G ` is Subgroup of H by GROUP_2:67; :: thesis: verum