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=BaseW
lvecmulcan2.s ·˙=W
lvecmulcan2.f F=ScalarW
lvecmulcan2.k K=BaseF
lvecmulcan2.o 0˙=0W
lvecmulcan2.w φWLVec
lvecmulcan2.a φAK
lvecmulcan2.b φBK
lvecmulcan2.x φXV
lvecmulcan2.n φX0˙
Assertion lvecvscan2 φA·˙X=B·˙XA=B

Proof

Step Hyp Ref Expression
1 lvecmulcan2.v V=BaseW
2 lvecmulcan2.s ·˙=W
3 lvecmulcan2.f F=ScalarW
4 lvecmulcan2.k K=BaseF
5 lvecmulcan2.o 0˙=0W
6 lvecmulcan2.w φWLVec
7 lvecmulcan2.a φAK
8 lvecmulcan2.b φBK
9 lvecmulcan2.x φXV
10 lvecmulcan2.n φX0˙
11 10 neneqd φ¬X=0˙
12 biorf ¬X=0˙A-FB=0FX=0˙A-FB=0F
13 orcom X=0˙A-FB=0FA-FB=0FX=0˙
14 12 13 bitrdi ¬X=0˙A-FB=0FA-FB=0FX=0˙
15 11 14 syl φA-FB=0FA-FB=0FX=0˙
16 eqid 0F=0F
17 lveclmod WLVecWLMod
18 6 17 syl φWLMod
19 3 lmodfgrp WLModFGrp
20 18 19 syl φFGrp
21 eqid -F=-F
22 4 21 grpsubcl FGrpAKBKA-FBK
23 20 7 8 22 syl3anc φA-FBK
24 1 2 3 4 16 5 6 23 9 lvecvs0or φA-FB·˙X=0˙A-FB=0FX=0˙
25 eqid -W=-W
26 1 2 3 4 25 21 18 7 8 9 lmodsubdir φA-FB·˙X=A·˙X-WB·˙X
27 26 eqeq1d φA-FB·˙X=0˙A·˙X-WB·˙X=0˙
28 15 24 27 3bitr2rd φA·˙X-WB·˙X=0˙A-FB=0F
29 1 3 2 4 lmodvscl WLModAKXVA·˙XV
30 18 7 9 29 syl3anc φA·˙XV
31 1 3 2 4 lmodvscl WLModBKXVB·˙XV
32 18 8 9 31 syl3anc φB·˙XV
33 1 5 25 lmodsubeq0 WLModA·˙XVB·˙XVA·˙X-WB·˙X=0˙A·˙X=B·˙X
34 18 30 32 33 syl3anc φA·˙X-WB·˙X=0˙A·˙X=B·˙X
35 4 16 21 grpsubeq0 FGrpAKBKA-FB=0FA=B
36 20 7 8 35 syl3anc φA-FB=0FA=B
37 28 34 36 3bitr3d φA·˙X=B·˙XA=B