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:128;
now for a being Element of G st a in G ` holds
a in Hlet 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 Th73;
rng F c= carr H
proof
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
x <> y
and A7:
Left_Cosets H = {x,y}
by A2, CARD_2:60;
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:135;
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
object ;
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, Th58;
b in the
carrier of
G
;
then
b in union (Left_Cosets H)
by GROUP_2:137;
then A12:
b in (carr H) \/ (c * H)
by A10, ZFMISC_1:75;
a in the
carrier of
G
;
then
a in union (Left_Cosets H)
by GROUP_2:137;
then A13:
a in (carr H) \/ (c * H)
by A10, ZFMISC_1:75;
now X in carr Hper 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:103;
consider e being
Element of
G such that A18:
b = c * e
and A19:
e in H
by A15, GROUP_2:103;
e " in H
by A19, GROUP_2:51;
then A20:
(e ") |^ c in H
by A3, Th3;
d " in H
by A17, GROUP_2:51;
then A21:
(d ") * ((e ") |^ c) in H
by A20, GROUP_2:50;
d |^ c in H
by A3, A17, Th3;
then A22:
(d |^ c) * e in H
by A19, GROUP_2:50;
[.a,b.] =
((a ") * (b ")) * (a * b)
by Th16
.=
(((d ") * (c ")) * (b ")) * ((c * d) * (c * e))
by A16, A18, GROUP_1:17
.=
(((d ") * (c ")) * ((e ") * (c "))) * ((c * d) * (c * e))
by A18, GROUP_1:17
.=
((((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 A11, A21, A22, GROUP_2:50;
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:28;
hence
a in H
by GROUP_4:31;
verum end;
hence
G ` is Subgroup of H
by GROUP_2:58; verum