This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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. = ( 0g ` G )
1nsgtrivd.3 
|- ( ph -> G e. Grp )
1nsgtrivd.4 
|- ( ph -> ( NrmSGrp ` G ) ~~ 1o )
Assertion 1nsgtrivd 
|- ( ph -> B = { .0. } )

Proof

Step Hyp Ref Expression
1 1nsgtrivd.1 
 |-  B = ( Base ` G )
2 1nsgtrivd.2 
 |-  .0. = ( 0g ` G )
3 1nsgtrivd.3 
 |-  ( ph -> G e. Grp )
4 1nsgtrivd.4 
 |-  ( ph -> ( NrmSGrp ` G ) ~~ 1o )
5 1 nsgid 
 |-  ( G e. Grp -> B e. ( NrmSGrp ` G ) )
6 3 5 syl 
 |-  ( ph -> B e. ( NrmSGrp ` G ) )
7 2 0nsg 
 |-  ( G e. Grp -> { .0. } e. ( NrmSGrp ` G ) )
8 3 7 syl 
 |-  ( ph -> { .0. } e. ( NrmSGrp ` G ) )
9 en1eqsn 
 |-  ( ( { .0. } e. ( NrmSGrp ` G ) /\ ( NrmSGrp ` G ) ~~ 1o ) -> ( NrmSGrp ` G ) = { { .0. } } )
10 8 4 9 syl2anc 
 |-  ( ph -> ( NrmSGrp ` G ) = { { .0. } } )
11 6 10 eleqtrd 
 |-  ( ph -> B e. { { .0. } } )
12 snex 
 |-  { .0. } e. _V
13 elsn2g 
 |-  ( { .0. } e. _V -> ( B e. { { .0. } } <-> B = { .0. } ) )
14 12 13 mp1i 
 |-  ( ph -> ( B e. { { .0. } } <-> B = { .0. } ) )
15 11 14 mpbid 
 |-  ( ph -> B = { .0. } )