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:128;

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:128;

now :: thesis: for a being Element of G st a in G ` holds

a in H

hence
G ` is Subgroup of H
by GROUP_2:58; :: thesis: veruma 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

hence a in H by GROUP_4:31; :: thesis: verum

end;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

then
a in gr (carr H)
by A4, A6, GROUP_4:28;
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 ; :: 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 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;

end;( 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 ; :: 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 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 :: thesis: X in carr Hend;

hence
X in carr H
; :: thesis: verumper 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;

end;

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 A11, Th38;

hence X in carr H by STRUCT_0:def 5; :: thesis: verum

end;then X in H by A11, Th38;

hence X in carr H by STRUCT_0:def 5; :: thesis: verum

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:51;

then (a ") * (a |^ b) in H by GROUP_2:50;

then X in H by A11, Th16;

hence X in carr H by STRUCT_0:def 5; :: thesis: verum

end;then ( a |^ b in H & a " in H ) by A3, Th3, GROUP_2:51;

then (a ") * (a |^ b) in H by GROUP_2:50;

then X in H by A11, Th16;

hence X in carr H by STRUCT_0:def 5; :: thesis: verum

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

then A14:
b in H
by STRUCT_0:def 5;

then b " in H by GROUP_2:51;

then (b ") |^ a in H by A3, Th3;

then ((b ") |^ a) * b in H by A14, GROUP_2:50;

hence X in carr H by A11, STRUCT_0:def 5; :: thesis: verum

end;then b " in H by GROUP_2:51;

then (b ") |^ a in H by A3, Th3;

then ((b ") |^ a) * b in H by A14, GROUP_2:50;

hence X in carr H by A11, STRUCT_0:def 5; :: thesis: verum

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 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; :: thesis: verum

end;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; :: thesis: verum

hence a in H by GROUP_4:31; :: thesis: verum