# Metamath Proof Explorer

## Theorem ipass

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. (Contributed by NM, 25-Aug-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
phllmhm.h
phllmhm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
ipdir.f ${⊢}{K}={\mathrm{Base}}_{{F}}$
ipass.s
ipass.p
Assertion ipass

### Proof

Step Hyp Ref Expression
1 phlsrng.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 phllmhm.h
3 phllmhm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
4 ipdir.f ${⊢}{K}={\mathrm{Base}}_{{F}}$
5 ipass.s
6 ipass.p
7 eqid
8 1 2 3 7 phllmhm
10 simpr1 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {K}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {A}\in {K}$
11 simpr2 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {K}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {B}\in {V}$
12 rlmvsca ${⊢}{\cdot }_{{F}}={\cdot }_{\mathrm{ringLMod}\left({F}\right)}$
13 6 12 eqtri
14 1 4 3 5 13 lmhmlin
15 9 10 11 14 syl3anc
16 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
17 16 adantr ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {K}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {W}\in \mathrm{LMod}$
18 3 1 5 4 lmodvscl
19 17 10 11 18 syl3anc
20 oveq1
21 ovex
22 20 7 21 fvmpt3i
23 19 22 syl
24 oveq1
25 24 7 21 fvmpt3i
26 11 25 syl
27 26 oveq2d
28 15 23 27 3eqtr3d