Metamath Proof Explorer


Theorem trivnsgd

Description: The only normal subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses trivnsgd.1
|- B = ( Base ` G )
trivnsgd.2
|- .0. = ( 0g ` G )
trivnsgd.3
|- ( ph -> G e. Grp )
trivnsgd.4
|- ( ph -> B = { .0. } )
Assertion trivnsgd
|- ( ph -> ( NrmSGrp ` G ) = { B } )

Proof

Step Hyp Ref Expression
1 trivnsgd.1
 |-  B = ( Base ` G )
2 trivnsgd.2
 |-  .0. = ( 0g ` G )
3 trivnsgd.3
 |-  ( ph -> G e. Grp )
4 trivnsgd.4
 |-  ( ph -> B = { .0. } )
5 nsgsubg
 |-  ( x e. ( NrmSGrp ` G ) -> x e. ( SubGrp ` G ) )
6 5 a1i
 |-  ( ph -> ( x e. ( NrmSGrp ` G ) -> x e. ( SubGrp ` G ) ) )
7 6 ssrdv
 |-  ( ph -> ( NrmSGrp ` G ) C_ ( SubGrp ` G ) )
8 1 2 3 4 trivsubgsnd
 |-  ( ph -> ( SubGrp ` G ) = { B } )
9 7 8 sseqtrd
 |-  ( ph -> ( NrmSGrp ` G ) C_ { B } )
10 1 nsgid
 |-  ( G e. Grp -> B e. ( NrmSGrp ` G ) )
11 3 10 syl
 |-  ( ph -> B e. ( NrmSGrp ` G ) )
12 11 snssd
 |-  ( ph -> { B } C_ ( NrmSGrp ` G ) )
13 9 12 eqssd
 |-  ( ph -> ( NrmSGrp ` G ) = { B } )