Metamath Proof Explorer


Theorem lvecvscan2

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

Ref Expression
Hypotheses lvecmulcan2.v V = Base W
lvecmulcan2.s · ˙ = W
lvecmulcan2.f F = Scalar W
lvecmulcan2.k K = Base F
lvecmulcan2.o 0 ˙ = 0 W
lvecmulcan2.w φ W LVec
lvecmulcan2.a φ A K
lvecmulcan2.b φ B K
lvecmulcan2.x φ X V
lvecmulcan2.n φ X 0 ˙
Assertion lvecvscan2 φ A · ˙ X = B · ˙ X A = B

Proof

Step Hyp Ref Expression
1 lvecmulcan2.v V = Base W
2 lvecmulcan2.s · ˙ = W
3 lvecmulcan2.f F = Scalar W
4 lvecmulcan2.k K = Base F
5 lvecmulcan2.o 0 ˙ = 0 W
6 lvecmulcan2.w φ W LVec
7 lvecmulcan2.a φ A K
8 lvecmulcan2.b φ B K
9 lvecmulcan2.x φ X V
10 lvecmulcan2.n φ X 0 ˙
11 10 neneqd φ ¬ X = 0 ˙
12 biorf ¬ X = 0 ˙ A - F B = 0 F X = 0 ˙ A - F B = 0 F
13 orcom X = 0 ˙ A - F B = 0 F A - F B = 0 F X = 0 ˙
14 12 13 bitrdi ¬ X = 0 ˙ A - F B = 0 F A - F B = 0 F X = 0 ˙
15 11 14 syl φ A - F B = 0 F A - F B = 0 F X = 0 ˙
16 eqid 0 F = 0 F
17 lveclmod W LVec W LMod
18 6 17 syl φ W LMod
19 3 lmodfgrp W LMod F Grp
20 18 19 syl φ F Grp
21 eqid - F = - F
22 4 21 grpsubcl F Grp A K B K A - F B K
23 20 7 8 22 syl3anc φ A - F B K
24 1 2 3 4 16 5 6 23 9 lvecvs0or φ A - F B · ˙ X = 0 ˙ A - F B = 0 F X = 0 ˙
25 eqid - W = - W
26 1 2 3 4 25 21 18 7 8 9 lmodsubdir φ A - F B · ˙ X = A · ˙ X - W B · ˙ X
27 26 eqeq1d φ A - F B · ˙ X = 0 ˙ A · ˙ X - W B · ˙ X = 0 ˙
28 15 24 27 3bitr2rd φ A · ˙ X - W B · ˙ X = 0 ˙ A - F B = 0 F
29 1 3 2 4 lmodvscl W LMod A K X V A · ˙ X V
30 18 7 9 29 syl3anc φ A · ˙ X V
31 1 3 2 4 lmodvscl W LMod B K X V B · ˙ X V
32 18 8 9 31 syl3anc φ B · ˙ X V
33 1 5 25 lmodsubeq0 W LMod A · ˙ X V B · ˙ X V A · ˙ X - W B · ˙ X = 0 ˙ A · ˙ X = B · ˙ X
34 18 30 32 33 syl3anc φ A · ˙ X - W B · ˙ X = 0 ˙ A · ˙ X = B · ˙ X
35 4 16 21 grpsubeq0 F Grp A K B K A - F B = 0 F A = B
36 20 7 8 35 syl3anc φ A - F B = 0 F A = B
37 28 34 36 3bitr3d φ A · ˙ X = B · ˙ X A = B