Theorem 0nsg

Description: The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Hypothesis	0nsg.z	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	0nsg	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{NrmSGrp}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		0nsg.z	$$⊢\underset{\dot{}}{0}=0_G$$
2	1	0subg	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubGrp}\left(G\right)$$
3		elsni	$$⊢y\in \left\{\underset{\dot{}}{0}\right\}\to y=\underset{\dot{}}{0}$$
4	3	ad2antll	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to y=\underset{\dot{}}{0}$$
5	4	oveq2d	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x{+}_{G}y=x{+}_G\underset{\dot{}}{0}$$
6		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
7		eqid	$$⊢{+}_G={+}_G$$
8	6 7 1	grprid	$$⊢\left(G\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_G\right)\to x{+}_G\underset{\dot{}}{0}=x$$
9	8	adantrr	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x{+}_G\underset{\dot{}}{0}=x$$
10	5 9	eqtrd	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x{+}_{G}y=x$$
11	10	oveq1d	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(x{+}_{G}y\right){-}_{G}x=x{-}_{G}x$$
12		eqid	$$⊢{-}_G={-}_G$$
13	6 1 12	grpsubid	$$⊢\left(G\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_G\right)\to x{-}_{G}x=\underset{\dot{}}{0}$$
14	13	adantrr	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x{-}_{G}x=\underset{\dot{}}{0}$$
15	11 14	eqtrd	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(x{+}_{G}y\right){-}_{G}x=\underset{\dot{}}{0}$$
16		ovex	$$⊢\left(x{+}_{G}y\right){-}_{G}x\in \mathrm{V}$$
17	16	elsn	$$⊢\left(x{+}_{G}y\right){-}_{G}x\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \left(x{+}_{G}y\right){-}_{G}x=\underset{\dot{}}{0}$$
18	15 17	sylibr	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(x{+}_{G}y\right){-}_{G}x\in \left\{\underset{\dot{}}{0}\right\}$$
19	18	ralrimivva	$$⊢G\in \mathrm{Grp}\to \forall x\in {\mathrm{Base}}_G\forall y\in \left\{\underset{\dot{}}{0}\right\}\left(x{+}_{G}y\right){-}_{G}x\in \left\{\underset{\dot{}}{0}\right\}$$
20	6 7 12	isnsg3	$$⊢\left\{\underset{\dot{}}{0}\right\}\in \mathrm{NrmSGrp}\left(G\right)\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubGrp}\left(G\right)\wedge \forall x\in {\mathrm{Base}}_G\forall y\in \left\{\underset{\dot{}}{0}\right\}\left(x{+}_{G}y\right){-}_{G}x\in \left\{\underset{\dot{}}{0}\right\}\right)$$
21	2 19 20	sylanbrc	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{NrmSGrp}\left(G\right)$$