Theorem odval

Description: Second substitution for the group order definition. (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by Stefan O'Rear, 5-Sep-2015) (Revised by AV, 5-Oct-2020)

	Ref	Expression
Hypotheses	odval.1	$$⊢X={\mathrm{Base}}_G$$
	odval.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	odval.3	$$⊢\underset{\dot{}}{0}=0_G$$
	odval.4	$$⊢O=\mathrm{od}\left(G\right)$$
	odval.i	$$⊢I=\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}$$
Assertion	odval	$$⊢A\in X\to O\left(A\right)=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		odval.1	$$⊢X={\mathrm{Base}}_G$$
2		odval.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		odval.3	$$⊢\underset{\dot{}}{0}=0_G$$
4		odval.4	$$⊢O=\mathrm{od}\left(G\right)$$
5		odval.i	$$⊢I=\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}$$
6		oveq2	$$⊢x=A\to y\underset{\dot{}}{·}x=y\underset{\dot{}}{·}A$$
7	6	eqeq1d	$$⊢x=A\to \left(y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
8	7	rabbidv	$$⊢x=A\to \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}$$
9	8 5	eqtr4di	$$⊢x=A\to \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=I$$
10	9	csbeq1d	$$⊢x=A\to ⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)=⦋I/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)$$
11		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
12	5 11	rabex2	$$⊢I\in \mathrm{V}$$
13		eqeq1	$$⊢i=I\to \left(i=\varnothing \leftrightarrow I=\varnothing \right)$$
14		infeq1	$$⊢i=I\to inf\left(i,ℝ,<\right)=inf\left(I,ℝ,<\right)$$
15	13 14	ifbieq2d	$$⊢i=I\to if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)$$
16	12 15	csbie	$$⊢⦋I/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)$$
17	10 16	eqtrdi	$$⊢x=A\to ⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)$$
18	1 2 3 4	odfval	$$⊢O=\left(x\in X⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)$$
19		c0ex	$$⊢0\in \mathrm{V}$$
20		ltso	$$⊢<\mathrm{Or}ℝ$$
21	20	infex	$$⊢inf\left(I,ℝ,<\right)\in \mathrm{V}$$
22	19 21	ifex	$$⊢if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)\in \mathrm{V}$$
23	17 18 22	fvmpt	$$⊢A\in X\to O\left(A\right)=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)$$