Theorem 0subg

Description: The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		0subg.z	$$⊢\underset{\dot{}}{0}=0_G$$
2		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
3	2 1	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
4	3	snssd	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\subseteq {\mathrm{Base}}_G$$
5	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
6	5	snnz	$$⊢\left\{\underset{\dot{}}{0}\right\}\ne \varnothing$$
7	6	a1i	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\ne \varnothing$$
8		eqid	$$⊢{+}_G={+}_G$$
9	2 8 1	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_G\right)\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
10	3 9	mpdan	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
11		ovex	$$⊢\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \mathrm{V}$$
12	11	elsn	$$⊢\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
13	10 12	sylibr	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}$$
14		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
15	1 14	grpinvid	$$⊢G\in \mathrm{Grp}\to {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
16		fvex	$$⊢{inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)\in \mathrm{V}$$
17	16	elsn	$$⊢{inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
18	15 17	sylibr	$$⊢G\in \mathrm{Grp}\to {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)\in \left\{\underset{\dot{}}{0}\right\}$$
19		oveq1	$$⊢a=\underset{\dot{}}{0}\to a{+}_{G}b=\underset{\dot{}}{0}{+}_{G}b$$
20	19	eleq1d	$$⊢a=\underset{\dot{}}{0}\to \left(a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{0}{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\right)$$
21	20	ralbidv	$$⊢a=\underset{\dot{}}{0}\to \left(\forall b\in \left\{\underset{\dot{}}{0}\right\}a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \forall b\in \left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{0}{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\right)$$
22		oveq2	$$⊢b=\underset{\dot{}}{0}\to \underset{\dot{}}{0}{+}_{G}b=\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}$$
23	22	eleq1d	$$⊢b=\underset{\dot{}}{0}\to \left(\underset{\dot{}}{0}{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}\right)$$
24	5 23	ralsn	$$⊢\forall b\in \left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{0}{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}$$
25	21 24	bitrdi	$$⊢a=\underset{\dot{}}{0}\to \left(\forall b\in \left\{\underset{\dot{}}{0}\right\}a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}\right)$$
26		fveq2	$$⊢a=\underset{\dot{}}{0}\to {inv}_g\left(G\right)\left(a\right)={inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)$$
27	26	eleq1d	$$⊢a=\underset{\dot{}}{0}\to \left({inv}_g\left(G\right)\left(a\right)\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)\in \left\{\underset{\dot{}}{0}\right\}\right)$$
28	25 27	anbi12d	$$⊢a=\underset{\dot{}}{0}\to \left(\left(\forall b\in \left\{\underset{\dot{}}{0}\right\}a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\wedge {inv}_g\left(G\right)\left(a\right)\in \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}\wedge {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)\in \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
29	5 28	ralsn	$$⊢\forall a\in \left\{\underset{\dot{}}{0}\right\}\left(\forall b\in \left\{\underset{\dot{}}{0}\right\}a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\wedge {inv}_g\left(G\right)\left(a\right)\in \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}\wedge {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)\in \left\{\underset{\dot{}}{0}\right\}\right)$$
30	13 18 29	sylanbrc	$$⊢G\in \mathrm{Grp}\to \forall a\in \left\{\underset{\dot{}}{0}\right\}\left(\forall b\in \left\{\underset{\dot{}}{0}\right\}a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\wedge {inv}_g\left(G\right)\left(a\right)\in \left\{\underset{\dot{}}{0}\right\}\right)$$
31	2 8 14	issubg2	$$⊢G\in \mathrm{Grp}\to \left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubGrp}\left(G\right)\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}\subseteq {\mathrm{Base}}_G\wedge \left\{\underset{\dot{}}{0}\right\}\ne \varnothing \wedge \forall a\in \left\{\underset{\dot{}}{0}\right\}\left(\forall b\in \left\{\underset{\dot{}}{0}\right\}a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\wedge {inv}_g\left(G\right)\left(a\right)\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)$$
32	4 7 30 31	mpbir3and	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubGrp}\left(G\right)$$