# Metamath Proof Explorer

## Theorem lvecvscan

Description: Cancellation law for scalar multiplication. ( hvmulcan analog.) (Contributed by NM, 2-Jul-2014)

Ref Expression
Hypotheses lvecmulcan.v $⊢ V = Base W$
lvecmulcan.s
lvecmulcan.f $⊢ F = Scalar ⁡ W$
lvecmulcan.k $⊢ K = Base F$
lvecmulcan.o
lvecmulcan.w $⊢ φ → W ∈ LVec$
lvecmulcan.a $⊢ φ → A ∈ K$
lvecmulcan.x $⊢ φ → X ∈ V$
lvecmulcan.y $⊢ φ → Y ∈ V$
lvecmulcan.n
Assertion lvecvscan

### Proof

Step Hyp Ref Expression
1 lvecmulcan.v $⊢ V = Base W$
2 lvecmulcan.s
3 lvecmulcan.f $⊢ F = Scalar ⁡ W$
4 lvecmulcan.k $⊢ K = Base F$
5 lvecmulcan.o
6 lvecmulcan.w $⊢ φ → W ∈ LVec$
7 lvecmulcan.a $⊢ φ → A ∈ K$
8 lvecmulcan.x $⊢ φ → X ∈ V$
9 lvecmulcan.y $⊢ φ → Y ∈ V$
10 lvecmulcan.n
11 df-ne
12 biorf
13 11 12 sylbi
14 10 13 syl
15 lveclmod $⊢ W ∈ LVec → W ∈ LMod$
16 6 15 syl $⊢ φ → W ∈ LMod$
17 eqid $⊢ 0 W = 0 W$
18 eqid $⊢ - W = - W$
19 1 17 18 lmodsubeq0 $⊢ W ∈ LMod ∧ X ∈ V ∧ Y ∈ V → X - W Y = 0 W ↔ X = Y$
20 16 8 9 19 syl3anc $⊢ φ → X - W Y = 0 W ↔ X = Y$
21 1 2 3 4 18 16 7 8 9 lmodsubdi
22 21 eqeq1d
23 1 18 lmodvsubcl $⊢ W ∈ LMod ∧ X ∈ V ∧ Y ∈ V → X - W Y ∈ V$
24 16 8 9 23 syl3anc $⊢ φ → X - W Y ∈ V$
25 1 2 3 4 5 17 6 7 24 lvecvs0or
26 1 3 2 4 lmodvscl
27 16 7 8 26 syl3anc
28 1 3 2 4 lmodvscl
29 16 7 9 28 syl3anc
30 1 17 18 lmodsubeq0
31 16 27 29 30 syl3anc
32 22 25 31 3bitr3d
33 14 20 32 3bitr3rd