Metamath Proof Explorer


Theorem clmvscom

Description: Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008) (Revised by AV, 7-Oct-2021)

Ref Expression
Hypotheses clmvscl.v V = Base W
clmvscl.f F = Scalar W
clmvscl.s · ˙ = W
clmvscl.k K = Base F
Assertion clmvscom W CMod Q K R K X V Q · ˙ R · ˙ X = R · ˙ Q · ˙ X

Proof

Step Hyp Ref Expression
1 clmvscl.v V = Base W
2 clmvscl.f F = Scalar W
3 clmvscl.s · ˙ = W
4 clmvscl.k K = Base F
5 ssel K Q K Q
6 ssel K R K R
7 5 6 anim12d K Q K R K Q R
8 2 4 clmsscn W CMod K
9 7 8 syl11 Q K R K W CMod Q R
10 9 3adant3 Q K R K X V W CMod Q R
11 10 impcom W CMod Q K R K X V Q R
12 mulcom Q R Q R = R Q
13 11 12 syl W CMod Q K R K X V Q R = R Q
14 13 oveq1d W CMod Q K R K X V Q R · ˙ X = R Q · ˙ X
15 1 2 3 4 clmvsass W CMod Q K R K X V Q R · ˙ X = Q · ˙ R · ˙ X
16 3ancoma Q K R K X V R K Q K X V
17 1 2 3 4 clmvsass W CMod R K Q K X V R Q · ˙ X = R · ˙ Q · ˙ X
18 16 17 sylan2b W CMod Q K R K X V R Q · ˙ X = R · ˙ Q · ˙ X
19 14 15 18 3eqtr3d W CMod Q K R K X V Q · ˙ R · ˙ X = R · ˙ Q · ˙ X