Theorem odfvalALT

Description: Shorter proof of odfval using ax-rep . (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by AV, 5-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	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)$$
Assertion	odfvalALT	$$⊢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)$$

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		fveq2	$$⊢g=G\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
6	5 1	eqtr4di	$$⊢g=G\to {\mathrm{Base}}_g=X$$
7		fveq2	$$⊢g=G\to {\cdot }_g={\cdot }_G$$
8	7 2	eqtr4di	$$⊢g=G\to {\cdot }_g=\underset{\dot{}}{·}$$
9	8	oveqd	$$⊢g=G\to y{\cdot }_{g}x=y\underset{\dot{}}{·}x$$
10		fveq2	$$⊢g=G\to 0_g=0_G$$
11	10 3	eqtr4di	$$⊢g=G\to 0_g=\underset{\dot{}}{0}$$
12	9 11	eqeq12d	$$⊢g=G\to \left(y{\cdot }_{g}x=0_g\leftrightarrow y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)$$
13	12	rabbidv	$$⊢g=G\to \left\{y\in \mathbb{N}|y{\cdot }_{g}x=0_g\right\}=\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
14	13	csbeq1d	$$⊢g=G\to ⦋\left\{y\in \mathbb{N}|y{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)=⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)$$
15	6 14	mpteq12dv	$$⊢g=G\to \left(x\in {\mathrm{Base}}_g⟼⦋\left\{y\in \mathbb{N}|y{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)=\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)$$
16		df-od	$$⊢\mathrm{od}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g⟼⦋\left\{y\in \mathbb{N}|y{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)\right)$$
17	15 16 1	mptfvmpt	$$⊢G\in \mathrm{V}\to \mathrm{od}\left(G\right)=\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)$$
18		fvprc	$$⊢\neg G\in \mathrm{V}\to \mathrm{od}\left(G\right)=\varnothing$$
19		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
20	1 19	eqtrid	$$⊢\neg G\in \mathrm{V}\to X=\varnothing$$
21	20	mpteq1d	$$⊢\neg G\in \mathrm{V}\to \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)=\left(x\in \varnothing ⟼⦋\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)$$
22		mpt0	$$⊢\left(x\in \varnothing ⟼⦋\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)=\varnothing$$
23	21 22	eqtrdi	$$⊢\neg G\in \mathrm{V}\to \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)=\varnothing$$
24	18 23	eqtr4d	$$⊢\neg G\in \mathrm{V}\to \mathrm{od}\left(G\right)=\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)$$
25	17 24	pm2.61i	$$⊢\mathrm{od}\left(G\right)=\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)$$
26	4 25	eqtri	$$⊢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)$$