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