# Metamath Proof Explorer

## Definition df-ipf

Description: Define the inner product function. Usually we will use .i directly instead of .if , and they have the same behavior in most cases. The main advantage of .if is that it is a guaranteed function ( ipffn ), while .i only has closure ( ipcl ). (Contributed by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion 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)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cipf ${class}{\cdot }_{\mathrm{if}}$
1 vg ${setvar}{g}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{g}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{g}}$
7 vy ${setvar}{y}$
8 3 cv ${setvar}{x}$
9 cip ${class}{\cdot }_{𝑖}$
10 5 9 cfv ${class}{\cdot }_{𝑖}\left({g}\right)$
11 7 cv ${setvar}{y}$
12 8 11 10 co ${class}\left({x}{\cdot }_{𝑖}\left({g}\right){y}\right)$
13 3 7 6 6 12 cmpo ${class}\left({x}\in {\mathrm{Base}}_{{g}},{y}\in {\mathrm{Base}}_{{g}}⟼{x}{\cdot }_{𝑖}\left({g}\right){y}\right)$
14 1 2 13 cmpt ${class}\left({g}\in \mathrm{V}⟼\left({x}\in {\mathrm{Base}}_{{g}},{y}\in {\mathrm{Base}}_{{g}}⟼{x}{\cdot }_{𝑖}\left({g}\right){y}\right)\right)$
15 0 14 wceq ${wff}{\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)$