Metamath Proof Explorer


Theorem cphass

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. See ipass , his5 . (Contributed by Mario Carneiro, 16-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 cphass W CPreHil A K B V C V A · ˙ B , ˙ C = A B , ˙ C

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 cphphl W CPreHil W PreHil
7 eqid F = F
8 3 1 2 4 5 7 ipass W PreHil A K B V C V A · ˙ B , ˙ C = A F B , ˙ C
9 6 8 sylan W CPreHil A K B V C V A · ˙ B , ˙ C = A F B , ˙ C
10 cphclm W CPreHil W CMod
11 3 clmmul W CMod × = F
12 10 11 syl W CPreHil × = F
13 12 adantr W CPreHil A K B V C V × = F
14 13 oveqd W CPreHil A K B V C V A B , ˙ C = A F B , ˙ C
15 9 14 eqtr4d W CPreHil A K B V C V A · ˙ B , ˙ C = A B , ˙ C