Metamath Proof Explorer


Theorem 1nsgtrivd

Description: A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses 1nsgtrivd.1 B = Base G
1nsgtrivd.2 0 ˙ = 0 G
1nsgtrivd.3 φ G Grp
1nsgtrivd.4 φ NrmSGrp G 1 𝑜
Assertion 1nsgtrivd φ B = 0 ˙

Proof

Step Hyp Ref Expression
1 1nsgtrivd.1 B = Base G
2 1nsgtrivd.2 0 ˙ = 0 G
3 1nsgtrivd.3 φ G Grp
4 1nsgtrivd.4 φ NrmSGrp G 1 𝑜
5 1 nsgid G Grp B NrmSGrp G
6 3 5 syl φ B NrmSGrp G
7 2 0nsg G Grp 0 ˙ NrmSGrp G
8 3 7 syl φ 0 ˙ NrmSGrp G
9 en1eqsn 0 ˙ NrmSGrp G NrmSGrp G 1 𝑜 NrmSGrp G = 0 ˙
10 8 4 9 syl2anc φ NrmSGrp G = 0 ˙
11 6 10 eleqtrd φ B 0 ˙
12 snex 0 ˙ V
13 elsn2g 0 ˙ V B 0 ˙ B = 0 ˙
14 12 13 mp1i φ B 0 ˙ B = 0 ˙
15 11 14 mpbid φ B = 0 ˙