# Metamath Proof Explorer

## 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
ipffval.3
Assertion ipffval

### Proof

Step Hyp Ref Expression
1 ipffval.1 ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 ipffval.2
3 ipffval.3
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
8 7 oveqd
9 5 5 8 mpoeq123dv
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
13 12 rnex
14 p0ex ${⊢}\left\{\varnothing \right\}\in \mathrm{V}$
15 13 14 unex
16 df-ov
17 fvrn0
18 16 17 eqeltri
19 18 rgen2w
20 11 11 15 19 mpoexw
21 9 10 20 fvmpt
22 fvprc ${⊢}¬{W}\in \mathrm{V}\to {\cdot }_{\mathrm{if}}\left({W}\right)=\varnothing$
23 fvprc ${⊢}¬{W}\in \mathrm{V}\to {\mathrm{Base}}_{{W}}=\varnothing$
24 1 23 syl5eq ${⊢}¬{W}\in \mathrm{V}\to {V}=\varnothing$
25 24 olcd ${⊢}¬{W}\in \mathrm{V}\to \left({V}=\varnothing \vee {V}=\varnothing \right)$
26 0mpo0
27 25 26 syl
28 22 27 eqtr4d
29 21 28 pm2.61i
30 3 29 eqtri