Theorem ipfval

Description: The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015)

	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	ipfval	$$⊢\left(X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{,}Y$$

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		oveq12	$$⊢\left(x=X\wedge y=Y\right)\to x\underset{\dot{}}{,}y=X\underset{\dot{}}{,}Y$$
5	1 2 3	ipffval	$$⊢\underset{\dot{}}{·}=\left(x\in V,y\in V⟼x\underset{\dot{}}{,}y\right)$$
6		ovex	$$⊢X\underset{\dot{}}{,}Y\in \mathrm{V}$$
7	4 5 6	ovmpoa	$$⊢\left(X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{,}Y$$