This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ B = {Base}_{G}$
	0idnsgd.2	$⊢ \underset{˙}{0} = 0_{G}$
	0idnsgd.3	$⊢ φ \to G \in Grp$
Assertion	0idnsgd	$⊢ φ \to \{\{\underset{˙}{0}\}, B\} \subseteq NrmSGrp (G)$

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