Theorem trivnsgd

Description: The only normal subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	trivnsgd.1	$$⊢B={\mathrm{Base}}_G$$
	trivnsgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
	trivnsgd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
	trivnsgd.4	$$⊢\phi \to B=\left\{\underset{\dot{}}{0}\right\}$$
Assertion	trivnsgd	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		trivnsgd.1	$$⊢B={\mathrm{Base}}_G$$
2		trivnsgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		trivnsgd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
4		trivnsgd.4	$$⊢\phi \to B=\left\{\underset{\dot{}}{0}\right\}$$
5		nsgsubg	$$⊢x\in \mathrm{NrmSGrp}\left(G\right)\to x\in \mathrm{SubGrp}\left(G\right)$$
6	5	a1i	$$⊢\phi \to \left(x\in \mathrm{NrmSGrp}\left(G\right)\to x\in \mathrm{SubGrp}\left(G\right)\right)$$
7	6	ssrdv	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)\subseteq \mathrm{SubGrp}\left(G\right)$$
8	1 2 3 4	trivsubgsnd	$$⊢\phi \to \mathrm{SubGrp}\left(G\right)=\left\{B\right\}$$
9	7 8	sseqtrd	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)\subseteq \left\{B\right\}$$
10	1	nsgid	$$⊢G\in \mathrm{Grp}\to B\in \mathrm{NrmSGrp}\left(G\right)$$
11	3 10	syl	$$⊢\phi \to B\in \mathrm{NrmSGrp}\left(G\right)$$
12	11	snssd	$$⊢\phi \to \left\{B\right\}\subseteq \mathrm{NrmSGrp}\left(G\right)$$
13	9 12	eqssd	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)=\left\{B\right\}$$