Theorem 0subgALT

Description: A shorter proof of 0subg using df-od . (Contributed by SN, 31-Jan-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		0subgALT.z	$$⊢\underset{\dot{}}{0}=0_G$$
2		eqid	$$⊢\mathrm{od}\left(G\right)=\mathrm{od}\left(G\right)$$
3		id	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Grp}$$
4		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
5	1	0subm	$$⊢G\in \mathrm{Mnd}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubMnd}\left(G\right)$$
6	4 5	syl	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubMnd}\left(G\right)$$
7	2 1	od1	$$⊢G\in \mathrm{Grp}\to \mathrm{od}\left(G\right)\left(\underset{\dot{}}{0}\right)=1$$
8		1nn	$$⊢1\in \mathbb{N}$$
9	7 8	eqeltrdi	$$⊢G\in \mathrm{Grp}\to \mathrm{od}\left(G\right)\left(\underset{\dot{}}{0}\right)\in \mathbb{N}$$
10	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
11		fveq2	$$⊢a=\underset{\dot{}}{0}\to \mathrm{od}\left(G\right)\left(a\right)=\mathrm{od}\left(G\right)\left(\underset{\dot{}}{0}\right)$$
12	11	eleq1d	$$⊢a=\underset{\dot{}}{0}\to \left(\mathrm{od}\left(G\right)\left(a\right)\in \mathbb{N}\leftrightarrow \mathrm{od}\left(G\right)\left(\underset{\dot{}}{0}\right)\in \mathbb{N}\right)$$
13	10 12	ralsn	$$⊢\forall a\in \left\{\underset{\dot{}}{0}\right\}\mathrm{od}\left(G\right)\left(a\right)\in \mathbb{N}\leftrightarrow \mathrm{od}\left(G\right)\left(\underset{\dot{}}{0}\right)\in \mathbb{N}$$
14	9 13	sylibr	$$⊢G\in \mathrm{Grp}\to \forall a\in \left\{\underset{\dot{}}{0}\right\}\mathrm{od}\left(G\right)\left(a\right)\in \mathbb{N}$$
15	2 3 6 14	finodsubmsubg	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubGrp}\left(G\right)$$