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 = ( Base ` G )
2nsgsimpgd.2 
|- .0. = ( 0g ` G )
2nsgsimpgd.3 
|- ( ph -> G e. Grp )
2nsgsimpgd.4 
|- ( ph -> -. { .0. } = B )
2nsgsimpgd.5 
|- ( ( ph /\ x e. ( NrmSGrp ` G ) ) -> ( x = { .0. } \/ x = B ) )
Assertion 2nsgsimpgd 
|- ( ph -> G e. SimpGrp )

Proof

Step Hyp Ref Expression
1 2nsgsimpgd.1 
 |-  B = ( Base ` G )
2 2nsgsimpgd.2 
 |-  .0. = ( 0g ` G )
3 2nsgsimpgd.3 
 |-  ( ph -> G e. Grp )
4 2nsgsimpgd.4 
 |-  ( ph -> -. { .0. } = B )
5 2nsgsimpgd.5 
 |-  ( ( ph /\ x e. ( NrmSGrp ` G ) ) -> ( x = { .0. } \/ x = B ) )
6 elprg 
 |-  ( x e. ( NrmSGrp ` G ) -> ( x e. { { .0. } , B } <-> ( x = { .0. } \/ x = B ) ) )
7 6 adantl 
 |-  ( ( ph /\ x e. ( NrmSGrp ` G ) ) -> ( x e. { { .0. } , B } <-> ( x = { .0. } \/ x = B ) ) )
8 5 7 mpbird 
 |-  ( ( ph /\ x e. ( NrmSGrp ` G ) ) -> x e. { { .0. } , B } )
9 simpr 
 |-  ( ( ph /\ x = { .0. } ) -> x = { .0. } )
10 2 0nsg 
 |-  ( G e. Grp -> { .0. } e. ( NrmSGrp ` G ) )
11 3 10 syl 
 |-  ( ph -> { .0. } e. ( NrmSGrp ` G ) )
12 11 adantr 
 |-  ( ( ph /\ x = { .0. } ) -> { .0. } e. ( NrmSGrp ` G ) )
13 9 12 eqeltrd 
 |-  ( ( ph /\ x = { .0. } ) -> x e. ( NrmSGrp ` G ) )
14 13 adantlr 
 |-  ( ( ( ph /\ x e. { { .0. } , B } ) /\ x = { .0. } ) -> x e. ( NrmSGrp ` G ) )
15 simpr 
 |-  ( ( ph /\ x = B ) -> x = B )
16 1 nsgid 
 |-  ( G e. Grp -> B e. ( NrmSGrp ` G ) )
17 3 16 syl 
 |-  ( ph -> B e. ( NrmSGrp ` G ) )
18 17 adantr 
 |-  ( ( ph /\ x = B ) -> B e. ( NrmSGrp ` G ) )
19 15 18 eqeltrd 
 |-  ( ( ph /\ x = B ) -> x e. ( NrmSGrp ` G ) )
20 19 adantlr 
 |-  ( ( ( ph /\ x e. { { .0. } , B } ) /\ x = B ) -> x e. ( NrmSGrp ` G ) )
21 elpri 
 |-  ( x e. { { .0. } , B } -> ( x = { .0. } \/ x = B ) )
22 21 adantl 
 |-  ( ( ph /\ x e. { { .0. } , B } ) -> ( x = { .0. } \/ x = B ) )
23 14 20 22 mpjaodan 
 |-  ( ( ph /\ x e. { { .0. } , B } ) -> x e. ( NrmSGrp ` G ) )
24 8 23 impbida 
 |-  ( ph -> ( x e. ( NrmSGrp ` G ) <-> x e. { { .0. } , B } ) )
25 24 eqrdv 
 |-  ( ph -> ( NrmSGrp ` G ) = { { .0. } , B } )
26 snex 
 |-  { .0. } e. _V
27 26 a1i 
 |-  ( ph -> { .0. } e. _V )
28 1 fvexi 
 |-  B e. _V
29 28 a1i 
 |-  ( ph -> B e. _V )
30 27 29 4 enpr2d 
 |-  ( ph -> { { .0. } , B } ~~ 2o )
31 25 30 eqbrtrd 
 |-  ( ph -> ( NrmSGrp ` G ) ~~ 2o )
32 3 31 issimpgd 
 |-  ( ph -> G e. SimpGrp )