Metamath Proof Explorer

Theorem ipdi

Description: Distributive law for inner product (left-distributivity). (Contributed by NM, 20-Nov-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 ipdi

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 simpl ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {W}\in \mathrm{PreHil}$
7 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}$
8 simpr3 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {C}\in {V}$
9 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}$
10 1 2 3 4 5 ipdir
11 6 7 8 9 10 syl13anc
12 11 fveq2d
13 1 phlsrng ${⊢}{W}\in \mathrm{PreHil}\to {F}\in \mathrm{*-Ring}$
14 13 adantr ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {F}\in \mathrm{*-Ring}$
15 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
16 1 2 3 15 ipcl
17 6 7 9 16 syl3anc
18 1 2 3 15 ipcl
19 6 8 9 18 syl3anc
20 eqid ${⊢}{*}_{{F}}={*}_{{F}}$
22 14 17 19 21 syl3anc
23 12 22 eqtrd
24 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
25 24 adantr ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {W}\in \mathrm{LMod}$
26 3 4 lmodvacl
27 25 7 8 26 syl3anc
28 1 2 3 20 ipcj
29 6 27 9 28 syl3anc
30 1 2 3 20 ipcj
31 6 7 9 30 syl3anc
32 1 2 3 20 ipcj
33 6 8 9 32 syl3anc
34 31 33 oveq12d
35 23 29 34 3eqtr3d