Metamath Proof Explorer


Theorem slmdvsass

Description: Associative law for scalar product. ( ax-hvmulass analog.) (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 22-Sep-2015) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses slmdvsass.v V = Base W
slmdvsass.f F = Scalar W
slmdvsass.s · ˙ = W
slmdvsass.k K = Base F
slmdvsass.t × ˙ = F
Assertion slmdvsass W SLMod Q K R K X V Q × ˙ R · ˙ X = Q · ˙ R · ˙ X

Proof

Step Hyp Ref Expression
1 slmdvsass.v V = Base W
2 slmdvsass.f F = Scalar W
3 slmdvsass.s · ˙ = W
4 slmdvsass.k K = Base F
5 slmdvsass.t × ˙ = F
6 eqid + W = + W
7 eqid 0 W = 0 W
8 eqid + F = + F
9 eqid 1 F = 1 F
10 eqid 0 F = 0 F
11 1 6 3 7 2 4 8 5 9 10 slmdlema W SLMod Q K R K X V X V R · ˙ X V R · ˙ X + W X = R · ˙ X + W R · ˙ X Q + F R · ˙ X = Q · ˙ X + W R · ˙ X Q × ˙ R · ˙ X = Q · ˙ R · ˙ X 1 F · ˙ X = X 0 F · ˙ X = 0 W
12 11 simprd W SLMod Q K R K X V X V Q × ˙ R · ˙ X = Q · ˙ R · ˙ X 1 F · ˙ X = X 0 F · ˙ X = 0 W
13 12 simp1d W SLMod Q K R K X V X V Q × ˙ R · ˙ X = Q · ˙ R · ˙ X
14 13 3expa W SLMod Q K R K X V X V Q × ˙ R · ˙ X = Q · ˙ R · ˙ X
15 14 anabsan2 W SLMod Q K R K X V Q × ˙ R · ˙ X = Q · ˙ R · ˙ X
16 15 exp42 W SLMod Q K R K X V Q × ˙ R · ˙ X = Q · ˙ R · ˙ X
17 16 3imp2 W SLMod Q K R K X V Q × ˙ R · ˙ X = Q · ˙ R · ˙ X