Theorem ipffval

Description: The inner product operation as a function. (Contributed by Mario Carneiro, 12-Oct-2015) (Proof shortened by AV, 2-Mar-2024)

	Ref	Expression
Hypotheses	ipffval.1	$$⊢V={\mathrm{Base}}_W$$
	ipffval.2	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	ipffval.3	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{if}}\left(W\right)$$
Assertion	ipffval	$$⊢\underset{\dot{}}{·}=\left(x\in V,y\in V⟼x\underset{\dot{}}{,}y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ipffval.1	$$⊢V={\mathrm{Base}}_W$$
2		ipffval.2	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		ipffval.3	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{if}}\left(W\right)$$
4		fveq2	$$⊢g=W\to {\mathrm{Base}}_g={\mathrm{Base}}_W$$
5	4 1	eqtr4di	$$⊢g=W\to {\mathrm{Base}}_g=V$$
6		fveq2	$$⊢g=W\to {\cdot }_{𝑖}\left(g\right)={\cdot }_{𝑖}\left(W\right)$$
7	6 2	eqtr4di	$$⊢g=W\to {\cdot }_{𝑖}\left(g\right)=\underset{\dot{}}{,}$$
8	7	oveqd	$$⊢g=W\to x{\cdot }_{𝑖}\left(g\right)y=x\underset{\dot{}}{,}y$$
9	5 5 8	mpoeq123dv	$$⊢g=W\to \left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{\cdot }_{𝑖}\left(g\right)y\right)=\left(x\in V,y\in V⟼x\underset{\dot{}}{,}y\right)$$
10		df-ipf	$$⊢{\cdot }_{\mathrm{if}}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{\cdot }_{𝑖}\left(g\right)y\right)\right)$$
11	1	fvexi	$$⊢V\in \mathrm{V}$$
12	2	fvexi	$$⊢\underset{\dot{}}{,}\in \mathrm{V}$$
13	12	rnex	$$⊢\mathrm{ran}\underset{\dot{}}{,}\in \mathrm{V}$$
14		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
15	13 14	unex	$$⊢\mathrm{ran}\underset{\dot{}}{,}\cup \left\{\varnothing \right\}\in \mathrm{V}$$
16		df-ov	$$⊢x\underset{\dot{}}{,}y=\underset{\dot{}}{,}\left(⟨x,y⟩\right)$$
17		fvrn0	$$⊢\underset{\dot{}}{,}\left(⟨x,y⟩\right)\in \left(\mathrm{ran}\underset{\dot{}}{,}\cup \left\{\varnothing \right\}\right)$$
18	16 17	eqeltri	$$⊢x\underset{\dot{}}{,}y\in \left(\mathrm{ran}\underset{\dot{}}{,}\cup \left\{\varnothing \right\}\right)$$
19	18	rgen2w	$$⊢\forall x\in V\forall y\in Vx\underset{\dot{}}{,}y\in \left(\mathrm{ran}\underset{\dot{}}{,}\cup \left\{\varnothing \right\}\right)$$
20	11 11 15 19	mpoexw	$$⊢\left(x\in V,y\in V⟼x\underset{\dot{}}{,}y\right)\in \mathrm{V}$$
21	9 10 20	fvmpt	$$⊢W\in \mathrm{V}\to {\cdot }_{\mathrm{if}}\left(W\right)=\left(x\in V,y\in V⟼x\underset{\dot{}}{,}y\right)$$
22		fvprc	$$⊢\neg W\in \mathrm{V}\to {\cdot }_{\mathrm{if}}\left(W\right)=\varnothing$$
23		fvprc	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_W=\varnothing$$
24	1 23	eqtrid	$$⊢\neg W\in \mathrm{V}\to V=\varnothing$$
25	24	olcd	$$⊢\neg W\in \mathrm{V}\to \left(V=\varnothing \vee V=\varnothing \right)$$
26		0mpo0	$$⊢\left(V=\varnothing \vee V=\varnothing \right)\to \left(x\in V,y\in V⟼x\underset{\dot{}}{,}y\right)=\varnothing$$
27	25 26	syl	$$⊢\neg W\in \mathrm{V}\to \left(x\in V,y\in V⟼x\underset{\dot{}}{,}y\right)=\varnothing$$
28	22 27	eqtr4d	$$⊢\neg W\in \mathrm{V}\to {\cdot }_{\mathrm{if}}\left(W\right)=\left(x\in V,y\in V⟼x\underset{\dot{}}{,}y\right)$$
29	21 28	pm2.61i	$$⊢{\cdot }_{\mathrm{if}}\left(W\right)=\left(x\in V,y\in V⟼x\underset{\dot{}}{,}y\right)$$
30	3 29	eqtri	$$⊢\underset{\dot{}}{·}=\left(x\in V,y\in V⟼x\underset{\dot{}}{,}y\right)$$