Metamath Proof Explorer


Theorem 2nsgsimpgd

Description: If any normal subgroup of a nontrivial group is either the trivial subgroup or the whole group, the group is simple. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses 2nsgsimpgd.1 B=BaseG
2nsgsimpgd.2 0˙=0G
2nsgsimpgd.3 φGGrp
2nsgsimpgd.4 φ¬0˙=B
2nsgsimpgd.5 φxNrmSGrpGx=0˙x=B
Assertion 2nsgsimpgd φGSimpGrp

Proof

Step Hyp Ref Expression
1 2nsgsimpgd.1 B=BaseG
2 2nsgsimpgd.2 0˙=0G
3 2nsgsimpgd.3 φGGrp
4 2nsgsimpgd.4 φ¬0˙=B
5 2nsgsimpgd.5 φxNrmSGrpGx=0˙x=B
6 elprg xNrmSGrpGx0˙Bx=0˙x=B
7 6 adantl φxNrmSGrpGx0˙Bx=0˙x=B
8 5 7 mpbird φxNrmSGrpGx0˙B
9 simpr φx=0˙x=0˙
10 2 0nsg GGrp0˙NrmSGrpG
11 3 10 syl φ0˙NrmSGrpG
12 11 adantr φx=0˙0˙NrmSGrpG
13 9 12 eqeltrd φx=0˙xNrmSGrpG
14 13 adantlr φx0˙Bx=0˙xNrmSGrpG
15 simpr φx=Bx=B
16 1 nsgid GGrpBNrmSGrpG
17 3 16 syl φBNrmSGrpG
18 17 adantr φx=BBNrmSGrpG
19 15 18 eqeltrd φx=BxNrmSGrpG
20 19 adantlr φx0˙Bx=BxNrmSGrpG
21 elpri x0˙Bx=0˙x=B
22 21 adantl φx0˙Bx=0˙x=B
23 14 20 22 mpjaodan φx0˙BxNrmSGrpG
24 8 23 impbida φxNrmSGrpGx0˙B
25 24 eqrdv φNrmSGrpG=0˙B
26 snex 0˙V
27 26 a1i φ0˙V
28 1 fvexi BV
29 28 a1i φBV
30 27 29 4 enpr2d φ0˙B2𝑜
31 25 30 eqbrtrd φNrmSGrpG2𝑜
32 3 31 issimpgd φGSimpGrp