Theorem 0idnsgd

Description: The whole group and the zero subgroup are normal subgroups of a group. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	0idnsgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	0idnsgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
	0idnsgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
Assertion	0idnsgd	⊢ ( 𝜑 → { { 0 } , 𝐵 } ⊆ ( NrmSGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		0idnsgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		0idnsgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		0idnsgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4	2	0nsg	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) )
5	3 4	syl	⊢ ( 𝜑 → { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) )
6	1	nsgid	⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )
7	3 6	syl	⊢ ( 𝜑 → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )
8	5 7	prssd	⊢ ( 𝜑 → { { 0 } , 𝐵 } ⊆ ( NrmSGrp ‘ 𝐺 ) )