# Metamath Proof Explorer

## Theorem ip2di

Description: Distributive law for inner product. (Contributed by NM, 17-Apr-2008) (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
ip2di.1 ${⊢}{\phi }\to {W}\in \mathrm{PreHil}$
ip2di.2 ${⊢}{\phi }\to {A}\in {V}$
ip2di.3 ${⊢}{\phi }\to {B}\in {V}$
ip2di.4 ${⊢}{\phi }\to {C}\in {V}$
ip2di.5 ${⊢}{\phi }\to {D}\in {V}$
Assertion ip2di

### 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 ip2di.1 ${⊢}{\phi }\to {W}\in \mathrm{PreHil}$
7 ip2di.2 ${⊢}{\phi }\to {A}\in {V}$
8 ip2di.3 ${⊢}{\phi }\to {B}\in {V}$
9 ip2di.4 ${⊢}{\phi }\to {C}\in {V}$
10 ip2di.5 ${⊢}{\phi }\to {D}\in {V}$
11 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
12 6 11 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
13 3 4 lmodvacl
14 12 9 10 13 syl3anc
15 1 2 3 4 5 ipdir
16 6 7 8 14 15 syl13anc
17 1 2 3 4 5 ipdi
18 6 7 9 10 17 syl13anc
19 1 2 3 4 5 ipdi
20 6 8 9 10 19 syl13anc
21 1 phlsrng ${⊢}{W}\in \mathrm{PreHil}\to {F}\in \mathrm{*-Ring}$
22 srngring ${⊢}{F}\in \mathrm{*-Ring}\to {F}\in \mathrm{Ring}$
23 ringcmn ${⊢}{F}\in \mathrm{Ring}\to {F}\in \mathrm{CMnd}$
24 6 21 22 23 4syl ${⊢}{\phi }\to {F}\in \mathrm{CMnd}$
25 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
26 1 2 3 25 ipcl
27 6 8 9 26 syl3anc
28 1 2 3 25 ipcl
29 6 8 10 28 syl3anc
30 25 5 cmncom
31 24 27 29 30 syl3anc
32 20 31 eqtrd
33 18 32 oveq12d
34 1 2 3 25 ipcl
35 6 7 9 34 syl3anc
36 1 2 3 25 ipcl
37 6 7 10 36 syl3anc
38 25 5 cmn4
39 24 35 37 29 27 38 syl122anc
40 16 33 39 3eqtrd