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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	trivnsgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
	trivnsgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	trivnsgd.4	⊢ ( 𝜑 → 𝐵 = { 0 } )
Assertion	trivnsgd	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		trivnsgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		trivnsgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		trivnsgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4		trivnsgd.4	⊢ ( 𝜑 → 𝐵 = { 0 } )
5		nsgsubg	⊢ ( 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) )
6	5	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) )
7	6	ssrdv	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) ⊆ ( SubGrp ‘ 𝐺 ) )
8	1 2 3 4	trivsubgsnd	⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) = { 𝐵 } )
9	7 8	sseqtrd	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) ⊆ { 𝐵 } )
10	1	nsgid	⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )
11	3 10	syl	⊢ ( 𝜑 → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )
12	11	snssd	⊢ ( 𝜑 → { 𝐵 } ⊆ ( NrmSGrp ‘ 𝐺 ) )
13	9 12	eqssd	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) = { 𝐵 } )