let G be Group; :: thesis: for H being strict Subgroup of G st Left_Cosets H = { {a} where a is Element of G : verum } holds

H = (1). G

let H be strict Subgroup of G; :: thesis: ( Left_Cosets H = { {a} where a is Element of G : verum } implies H = (1). G )

assume A1: Left_Cosets H = { {a} where a is Element of G : verum } ; :: thesis: H = (1). G

A2: the carrier of H c= {(1_ G)}

then 1_ G in the carrier of H ;

then {(1_ G)} c= the carrier of H by ZFMISC_1:31;

then {(1_ G)} = the carrier of H by A2;

hence H = (1). G by Def7; :: thesis: verum

H = (1). G

let H be strict Subgroup of G; :: thesis: ( Left_Cosets H = { {a} where a is Element of G : verum } implies H = (1). G )

assume A1: Left_Cosets H = { {a} where a is Element of G : verum } ; :: thesis: H = (1). G

A2: the carrier of H c= {(1_ G)}

proof

1_ G in H
by Th46;
set a = the Element of G;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of H or x in {(1_ G)} )

assume x in the carrier of H ; :: thesis: x in {(1_ G)}

then reconsider h = x as Element of H ;

A3: h in H ;

reconsider h = h as Element of G by Th42;

the Element of G * H in Left_Cosets H by Def15;

then consider b being Element of G such that

A4: the Element of G * H = {b} by A1;

the Element of G * h in the Element of G * H by A3, Th103;

then A5: the Element of G * h = b by A4, TARSKI:def 1;

1_ G in H by Th46;

then the Element of G * (1_ G) in the Element of G * H by Th103;

then the Element of G * (1_ G) = b by A4, TARSKI:def 1;

then h = 1_ G by A5, GROUP_1:6;

hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of H or x in {(1_ G)} )

assume x in the carrier of H ; :: thesis: x in {(1_ G)}

then reconsider h = x as Element of H ;

A3: h in H ;

reconsider h = h as Element of G by Th42;

the Element of G * H in Left_Cosets H by Def15;

then consider b being Element of G such that

A4: the Element of G * H = {b} by A1;

the Element of G * h in the Element of G * H by A3, Th103;

then A5: the Element of G * h = b by A4, TARSKI:def 1;

1_ G in H by Th46;

then the Element of G * (1_ G) in the Element of G * H by Th103;

then the Element of G * (1_ G) = b by A4, TARSKI:def 1;

then h = 1_ G by A5, GROUP_1:6;

hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

then 1_ G in the carrier of H ;

then {(1_ G)} c= the carrier of H by ZFMISC_1:31;

then {(1_ G)} = the carrier of H by A2;

hence H = (1). G by Def7; :: thesis: verum