Description: Cancellation law for scalar multiplication. ( hvmulcan2 analog.) (Contributed by NM, 2-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lvecmulcan2.v | |
|
lvecmulcan2.s | |
||
lvecmulcan2.f | |
||
lvecmulcan2.k | |
||
lvecmulcan2.o | |
||
lvecmulcan2.w | |
||
lvecmulcan2.a | |
||
lvecmulcan2.b | |
||
lvecmulcan2.x | |
||
lvecmulcan2.n | |
||
Assertion | lvecvscan2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lvecmulcan2.v | |
|
2 | lvecmulcan2.s | |
|
3 | lvecmulcan2.f | |
|
4 | lvecmulcan2.k | |
|
5 | lvecmulcan2.o | |
|
6 | lvecmulcan2.w | |
|
7 | lvecmulcan2.a | |
|
8 | lvecmulcan2.b | |
|
9 | lvecmulcan2.x | |
|
10 | lvecmulcan2.n | |
|
11 | 10 | neneqd | |
12 | biorf | |
|
13 | orcom | |
|
14 | 12 13 | bitrdi | |
15 | 11 14 | syl | |
16 | eqid | |
|
17 | lveclmod | |
|
18 | 6 17 | syl | |
19 | 3 | lmodfgrp | |
20 | 18 19 | syl | |
21 | eqid | |
|
22 | 4 21 | grpsubcl | |
23 | 20 7 8 22 | syl3anc | |
24 | 1 2 3 4 16 5 6 23 9 | lvecvs0or | |
25 | eqid | |
|
26 | 1 2 3 4 25 21 18 7 8 9 | lmodsubdir | |
27 | 26 | eqeq1d | |
28 | 15 24 27 | 3bitr2rd | |
29 | 1 3 2 4 | lmodvscl | |
30 | 18 7 9 29 | syl3anc | |
31 | 1 3 2 4 | lmodvscl | |
32 | 18 8 9 31 | syl3anc | |
33 | 1 5 25 | lmodsubeq0 | |
34 | 18 30 32 33 | syl3anc | |
35 | 4 16 21 | grpsubeq0 | |
36 | 20 7 8 35 | syl3anc | |
37 | 28 34 36 | 3bitr3d | |