Theorem 0subg

Description: The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014) (Proof shortened by SN, 31-Jan-2025)

	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		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
3	1	0subm	$$⊢G\in \mathrm{Mnd}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubMnd}\left(G\right)$$
4	2 3	syl	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubMnd}\left(G\right)$$
5		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
6	1 5	grpinvid	$$⊢G\in \mathrm{Grp}\to {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
7		fvex	$$⊢{inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)\in \mathrm{V}$$
8	7	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}$$
9	6 8	sylibr	$$⊢G\in \mathrm{Grp}\to {inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)\in \left\{\underset{\dot{}}{0}\right\}$$
10	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
11		fveq2	$$⊢a=\underset{\dot{}}{0}\to {inv}_g\left(G\right)\left(a\right)={inv}_g\left(G\right)\left(\underset{\dot{}}{0}\right)$$
12	11	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)$$
13	10 12	ralsn	$$⊢\forall a\in \left\{\underset{\dot{}}{0}\right\}{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\}$$
14	9 13	sylibr	$$⊢G\in \mathrm{Grp}\to \forall a\in \left\{\underset{\dot{}}{0}\right\}{inv}_g\left(G\right)\left(a\right)\in \left\{\underset{\dot{}}{0}\right\}$$
15	5	issubg3	$$⊢G\in \mathrm{Grp}\to \left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubGrp}\left(G\right)\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubMnd}\left(G\right)\wedge \forall a\in \left\{\underset{\dot{}}{0}\right\}{inv}_g\left(G\right)\left(a\right)\in \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
16	4 14 15	mpbir2and	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubGrp}\left(G\right)$$