Metamath Proof Explorer

Theorem simpgnsgbid

Description: A nontrivial group is simple if and only if its normal subgroups are exactly the group itself and the trivial subgroup. (Contributed by Rohan Ridenour, 4-Aug-2023)

Ref Expression
Hypotheses simpgnsgbid.1 ⊢ B = Base G
simpgnsgbid.2 ⊢ 0 ˙ = 0 G
simpgnsgbid.3 ⊢ φ → G ∈ Grp
simpgnsgbid.4 ⊢ φ → ¬ 0 ˙ = B
Assertion simpgnsgbid ⊢ φ → G ∈ SimpGrp ↔ NrmSGrp ⁡ G = 0 ˙ B

Proof

Step Hyp Ref Expression
1 simpgnsgbid.1 ⊢ B = Base G
2 simpgnsgbid.2 ⊢ 0 ˙ = 0 G
3 simpgnsgbid.3 ⊢ φ → G ∈ Grp
4 simpgnsgbid.4 ⊢ φ → ¬ 0 ˙ = B
5 simpr ⊢ φ ∧ G ∈ SimpGrp → G ∈ SimpGrp
6 1 2 5 simpgnsgd ⊢ φ ∧ G ∈ SimpGrp → NrmSGrp ⁡ G = 0 ˙ B
7 3 adantr ⊢ φ ∧ NrmSGrp ⁡ G = 0 ˙ B → G ∈ Grp
8 4 adantr ⊢ φ ∧ NrmSGrp ⁡ G = 0 ˙ B → ¬ 0 ˙ = B
9 simpr ⊢ φ ∧ NrmSGrp ⁡ G = 0 ˙ B ∧ x ∈ NrmSGrp ⁡ G → x ∈ NrmSGrp ⁡ G
10 simplr ⊢ φ ∧ NrmSGrp ⁡ G = 0 ˙ B ∧ x ∈ NrmSGrp ⁡ G → NrmSGrp ⁡ G = 0 ˙ B
11 9 10 eleqtrd ⊢ φ ∧ NrmSGrp ⁡ G = 0 ˙ B ∧ x ∈ NrmSGrp ⁡ G → x ∈ 0 ˙ B
12 elpri ⊢ x ∈ 0 ˙ B → x = 0 ˙ ∨ x = B
13 11 12 syl ⊢ φ ∧ NrmSGrp ⁡ G = 0 ˙ B ∧ x ∈ NrmSGrp ⁡ G → x = 0 ˙ ∨ x = B
14 1 2 7 8 13 2nsgsimpgd ⊢ φ ∧ NrmSGrp ⁡ G = 0 ˙ B → G ∈ SimpGrp
15 6 14 impbida ⊢ φ → G ∈ SimpGrp ↔ NrmSGrp ⁡ G = 0 ˙ B