Metamath Proof Explorer


Theorem cph2ass

Description: Move scalar multiplication to outside of inner product. See his35 . (Contributed by Mario Carneiro, 17-Oct-2015)

Ref Expression
Hypotheses cphipcj.h , ˙ = 𝑖 W
cphipcj.v V = Base W
cphass.f F = Scalar W
cphass.k K = Base F
cphass.s · ˙ = W
Assertion cph2ass W CPreHil A K B K C V D V A · ˙ C , ˙ B · ˙ D = A B C , ˙ D

Proof

Step Hyp Ref Expression
1 cphipcj.h , ˙ = 𝑖 W
2 cphipcj.v V = Base W
3 cphass.f F = Scalar W
4 cphass.k K = Base F
5 cphass.s · ˙ = W
6 simp1 W CPreHil A K B K C V D V W CPreHil
7 simp2r W CPreHil A K B K C V D V B K
8 simp3l W CPreHil A K B K C V D V C V
9 simp3r W CPreHil A K B K C V D V D V
10 1 2 3 4 5 cphassr W CPreHil B K C V D V C , ˙ B · ˙ D = B C , ˙ D
11 6 7 8 9 10 syl13anc W CPreHil A K B K C V D V C , ˙ B · ˙ D = B C , ˙ D
12 11 oveq2d W CPreHil A K B K C V D V A C , ˙ B · ˙ D = A B C , ˙ D
13 simp2l W CPreHil A K B K C V D V A K
14 cphlmod W CPreHil W LMod
15 14 3ad2ant1 W CPreHil A K B K C V D V W LMod
16 2 3 5 4 lmodvscl W LMod B K D V B · ˙ D V
17 15 7 9 16 syl3anc W CPreHil A K B K C V D V B · ˙ D V
18 1 2 3 4 5 cphass W CPreHil A K C V B · ˙ D V A · ˙ C , ˙ B · ˙ D = A C , ˙ B · ˙ D
19 6 13 8 17 18 syl13anc W CPreHil A K B K C V D V A · ˙ C , ˙ B · ˙ D = A C , ˙ B · ˙ D
20 cphclm W CPreHil W CMod
21 20 3ad2ant1 W CPreHil A K B K C V D V W CMod
22 3 4 clmsscn W CMod K
23 21 22 syl W CPreHil A K B K C V D V K
24 23 13 sseldd W CPreHil A K B K C V D V A
25 23 7 sseldd W CPreHil A K B K C V D V B
26 25 cjcld W CPreHil A K B K C V D V B
27 2 1 cphipcl W CPreHil C V D V C , ˙ D
28 27 3expb W CPreHil C V D V C , ˙ D
29 28 3adant2 W CPreHil A K B K C V D V C , ˙ D
30 24 26 29 mulassd W CPreHil A K B K C V D V A B C , ˙ D = A B C , ˙ D
31 12 19 30 3eqtr4d W CPreHil A K B K C V D V A · ˙ C , ˙ B · ˙ D = A B C , ˙ D