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 ;
now :: thesis: for a being Element of G st a in G ` holds
a in H
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 Th73;
rng F c= carr H
proof
ex B being finite set st
( B = Left_Cosets H & index H = card B ) by ;
then consider x, y being object such that
x <> y and
A7: Left_Cosets H = {x,y} by ;
x in Left_Cosets H by ;
then consider d being Element of G such that
A8: x = d * H by GROUP_2:def 15;
y in Left_Cosets H by ;
then consider e being Element of G such that
A9: y = e * H by GROUP_2:def 15;
carr H in Left_Cosets H by GROUP_2:135;
then ( Left_Cosets H = {(carr H),(e * H)} or Left_Cosets H = {(d * H),(carr H)} ) by ;
then consider c being Element of G such that
A10: Left_Cosets H = {(carr H),(c * H)} ;
let X be object ; :: 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
A11: X = [.a,b.] by ;
b in the carrier of G ;
then b in union () by GROUP_2:137;
then A12: b in (carr H) \/ (c * H) by ;
a in the carrier of G ;
then a in union () by GROUP_2:137;
then A13: a in (carr H) \/ (c * H) by ;
now :: thesis: X in carr H
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 ;
suppose A15: ( a in c * H & b in c * H ) ; :: thesis: X in carr H
then consider d being Element of G such that
A16: a = c * d and
A17: d in H by GROUP_2:103;
consider e being Element of G such that
A18: b = c * e and
A19: e in H by ;
e " in H by ;
then A20: (e ") |^ c in H by ;
d " in H by ;
then A21: (d ") * ((e ") |^ c) in H by ;
d |^ c in H by A3, A17, Th3;
then A22: (d |^ c) * e in H by ;
[.a,b.] = ((a ") * (b ")) * (a * b) by Th16
.= (((d ") * (c ")) * (b ")) * ((c * d) * (c * e)) by
.= (((d ") * (c ")) * ((e ") * (c "))) * ((c * d) * (c * e)) by
.= ((((d ") * (c ")) * (e ")) * (c ")) * ((c * d) * (c * e)) by GROUP_1:def 3
.= ((((d ") * (c ")) * (e ")) * (c ")) * (c * (d * (c * e))) by GROUP_1:def 3
.= (((((d ") * (c ")) * (e ")) * (c ")) * c) * (d * (c * e)) by GROUP_1:def 3
.= ((((d ") * (c ")) * (e ")) * ((c ") * c)) * (d * (c * e)) by GROUP_1:def 3
.= ((((d ") * (c ")) * (e ")) * (1_ G)) * (d * (c * e)) by GROUP_1:def 5
.= ((((d ") * (c ")) * (e ")) * (c * (c "))) * (d * (c * e)) by GROUP_1:def 5
.= (((((d ") * (c ")) * (e ")) * c) * (c ")) * (d * (c * e)) by GROUP_1:def 3
.= ((((d ") * ((c ") * (e "))) * c) * (c ")) * (d * (c * e)) by GROUP_1:def 3
.= (((d ") * ((e ") |^ c)) * (c ")) * (d * (c * e)) by GROUP_1:def 3
.= (((d ") * ((e ") |^ c)) * (c ")) * ((d * c) * e) by GROUP_1:def 3
.= ((d ") * ((e ") |^ c)) * ((c ") * ((d * c) * e)) by GROUP_1:def 3
.= ((d ") * ((e ") |^ c)) * ((c ") * (d * (c * e))) by GROUP_1:def 3
.= ((d ") * ((e ") |^ c)) * (((c ") * d) * (c * e)) by GROUP_1:def 3
.= ((d ") * ((e ") |^ c)) * ((d |^ c) * e) by GROUP_1:def 3 ;
then X in H by ;
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 ;
hence a in H by GROUP_4:31; :: thesis: verum
end;
hence G ` is Subgroup of H by GROUP_2:58; :: thesis: verum