Theorem odval2

Description: A non-conditional definition of the group order. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	odcl.1	$$⊢X={\mathrm{Base}}_G$$
	odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
	odid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	odid.4	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	odval2	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to O\left(A\right)=\left(\iota x\in {\mathbb{N}}_0|\forall y\in {\mathbb{N}}_0\left(x\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$$⊢X={\mathrm{Base}}_G$$
2		odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
3		odid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		odid.4	$$⊢\underset{\dot{}}{0}=0_G$$
5	1 2	odcl	$$⊢A\in X\to O\left(A\right)\in {\mathbb{N}}_0$$
6	5	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to O\left(A\right)\in {\mathbb{N}}_0$$
7	1 2 3 4	odeq	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge x\in {\mathbb{N}}_0\right)\to \left(x=O\left(A\right)\leftrightarrow \forall y\in {\mathbb{N}}_0\left(x\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$
8	7	3expa	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\right)\wedge x\in {\mathbb{N}}_0\right)\to \left(x=O\left(A\right)\leftrightarrow \forall y\in {\mathbb{N}}_0\left(x\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$
9	8	bicomd	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\right)\wedge x\in {\mathbb{N}}_0\right)\to \left(\forall y\in {\mathbb{N}}_0\left(x\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\leftrightarrow x=O\left(A\right)\right)$$
10	6 9	riota5	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \left(\iota x\in {\mathbb{N}}_0|\forall y\in {\mathbb{N}}_0\left(x\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)=O\left(A\right)$$
11	10	eqcomd	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to O\left(A\right)=\left(\iota x\in {\mathbb{N}}_0|\forall y\in {\mathbb{N}}_0\left(x\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$