# Metamath Proof Explorer

## Theorem phlipf

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

Ref Expression
Hypotheses ipffn.1 ${⊢}{V}={\mathrm{Base}}_{{W}}$
ipffn.2
phlipf.s ${⊢}{S}=\mathrm{Scalar}\left({W}\right)$
phlipf.k ${⊢}{K}={\mathrm{Base}}_{{S}}$
Assertion phlipf

### Proof

Step Hyp Ref Expression
1 ipffn.1 ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 ipffn.2
3 phlipf.s ${⊢}{S}=\mathrm{Scalar}\left({W}\right)$
4 phlipf.k ${⊢}{K}={\mathrm{Base}}_{{S}}$
5 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
6 3 5 1 4 ipcl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\in {V}\wedge {y}\in {V}\right)\to {x}{\cdot }_{𝑖}\left({W}\right){y}\in {K}$
7 6 3expb ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({x}\in {V}\wedge {y}\in {V}\right)\right)\to {x}{\cdot }_{𝑖}\left({W}\right){y}\in {K}$
8 7 ralrimivva ${⊢}{W}\in \mathrm{PreHil}\to \forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in {V}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}\in {K}$
9 1 5 2 ipffval
10 9 fmpo
11 8 10 sylib