let G be Group; 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; ( 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
; 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;
( a in G ` implies a in H )assume
a in G `
;
a in Hthen 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
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 A7:
Left_Cosets H = {x,y}
by A2, CARD_2:79;
x in Left_Cosets H
by A7, TARSKI:def 2;
then consider d being
Element of
G such that A8:
x = d * H
by GROUP_2:def 15;
y in Left_Cosets H
by A7, TARSKI:def 2;
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:165;
then
(
Left_Cosets H = {(carr H),(e * H)} or
Left_Cosets H = {(d * H),(carr H)} )
by A7, A8, A9, TARSKI:def 2;
then consider c being
Element of
G such that A10:
Left_Cosets H = {(carr H),(c * H)}
;
let X be
set ;
TARSKI:def 3 ( not X in rng F or X in carr H )
assume
X in rng F
;
X in carr H
then consider a,
b being
Element of
G such that A11:
X = [.a,b.]
by A5, Th65;
b in the
carrier of
G
;
then
b in union (Left_Cosets H)
by GROUP_2:167;
then A12:
b in (carr H) \/ (c * H)
by A10, ZFMISC_1:93;
a in the
carrier of
G
;
then
a in union (Left_Cosets H)
by GROUP_2:167;
then A13:
a in (carr H) \/ (c * H)
by A10, 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 A13, A12, XBOOLE_0:def 3;
suppose A15:
(
a in c * H &
b in c * H )
;
X in carr Hthen consider d being
Element of
G such that A16:
a = c * d
and A17:
d in H
by GROUP_2:125;
consider e being
Element of
G such that A18:
b = c * e
and A19:
e in H
by A15, GROUP_2:125;
e " in H
by A19, GROUP_2:60;
then A20:
(e " ) |^ c in H
by A3, Th3;
d " in H
by A17, GROUP_2:60;
then A21:
(d " ) * ((e " ) |^ c) in H
by A20, GROUP_2:59;
d |^ c in H
by A3, A17, Th3;
then A22:
(d |^ c) * e in H
by A19, GROUP_2:59;
[.a,b.] =
((a " ) * (b " )) * (a * b)
by Th19
.=
(((d " ) * (c " )) * (b " )) * ((c * d) * (c * e))
by A16, A18, GROUP_1:25
.=
(((d " ) * (c " )) * ((e " ) * (c " ))) * ((c * d) * (c * e))
by A18, 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
;
then
X in H
by A11, A21, A22, GROUP_2:59;
hence
X in carr H
by STRUCT_0:def 5;
verum end;
hence
X in carr H
;
verum
end; then
a in gr (carr H)
by A4, A6, GROUP_4:37;
hence
a in H
by GROUP_4:40;
verum end;
hence
G ` is Subgroup of H
by GROUP_2:67; verum