Metamath Proof Explorer


Theorem clmvsass

Description: Associative law for scalar product. Analogue of lmodvsass . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clmvscl.v V=BaseW
clmvscl.f F=ScalarW
clmvscl.s ·˙=W
clmvscl.k K=BaseF
Assertion clmvsass WCModQKRKXVQR·˙X=Q·˙R·˙X

Proof

Step Hyp Ref Expression
1 clmvscl.v V=BaseW
2 clmvscl.f F=ScalarW
3 clmvscl.s ·˙=W
4 clmvscl.k K=BaseF
5 2 clmmul WCMod×=F
6 5 adantr WCModQKRKXV×=F
7 6 oveqd WCModQKRKXVQR=QFR
8 7 oveq1d WCModQKRKXVQR·˙X=QFR·˙X
9 clmlmod WCModWLMod
10 eqid F=F
11 1 2 3 4 10 lmodvsass WLModQKRKXVQFR·˙X=Q·˙R·˙X
12 9 11 sylan WCModQKRKXVQFR·˙X=Q·˙R·˙X
13 8 12 eqtrd WCModQKRKXVQR·˙X=Q·˙R·˙X