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	$$⊢B={\mathrm{Base}}_G$$
	0idnsgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
	0idnsgd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
Assertion	0idnsgd	$$⊢\phi \to \left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\subseteq \mathrm{NrmSGrp}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		0idnsgd.1	$$⊢B={\mathrm{Base}}_G$$
2		0idnsgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		0idnsgd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
4	2	0nsg	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{NrmSGrp}\left(G\right)$$
5	3 4	syl	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{NrmSGrp}\left(G\right)$$
6	1	nsgid	$$⊢G\in \mathrm{Grp}\to B\in \mathrm{NrmSGrp}\left(G\right)$$
7	3 6	syl	$$⊢\phi \to B\in \mathrm{NrmSGrp}\left(G\right)$$
8	5 7	prssd	$$⊢\phi \to \left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\subseteq \mathrm{NrmSGrp}\left(G\right)$$