Metamath Proof Explorer


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 ‘ 𝐺 ) )