# Metamath Proof Explorer

## Theorem ipdir

Description: Distributive law for inner product (right-distributivity). Equation I3 of Ponnusamy p. 362. (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.g
ipdir.p
Assertion ipdir

### 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.g
5 ipdir.p
6 eqid
7 1 2 3 6 phllmhm
9 lmghm
10 8 9 syl
11 simpr1 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {A}\in {V}$
12 simpr2 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {B}\in {V}$
13 rlmplusg ${⊢}{+}_{{F}}={+}_{\mathrm{ringLMod}\left({F}\right)}$
14 5 13 eqtri
15 3 4 14 ghmlin
16 10 11 12 15 syl3anc
17 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
18 3 4 lmodvacl
19 17 18 syl3an1