Metamath Proof Explorer


Theorem clmsubdir

Description: Scalar multiplication distributive law for subtraction. ( lmodsubdir analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clmsubdir.v V = Base W
clmsubdir.t · ˙ = W
clmsubdir.f F = Scalar W
clmsubdir.k K = Base F
clmsubdir.m - ˙ = - W
clmsubdir.w φ W CMod
clmsubdir.a φ A K
clmsubdir.b φ B K
clmsubdir.x φ X V
Assertion clmsubdir φ A B · ˙ X = A · ˙ X - ˙ B · ˙ X

Proof

Step Hyp Ref Expression
1 clmsubdir.v V = Base W
2 clmsubdir.t · ˙ = W
3 clmsubdir.f F = Scalar W
4 clmsubdir.k K = Base F
5 clmsubdir.m - ˙ = - W
6 clmsubdir.w φ W CMod
7 clmsubdir.a φ A K
8 clmsubdir.b φ B K
9 clmsubdir.x φ X V
10 3 4 clmsub W CMod A K B K A B = A - F B
11 6 7 8 10 syl3anc φ A B = A - F B
12 11 oveq1d φ A B · ˙ X = A - F B · ˙ X
13 eqid - F = - F
14 clmlmod W CMod W LMod
15 6 14 syl φ W LMod
16 1 2 3 4 5 13 15 7 8 9 lmodsubdir φ A - F B · ˙ X = A · ˙ X - ˙ B · ˙ X
17 12 16 eqtrd φ A B · ˙ X = A · ˙ X - ˙ B · ˙ X