Description: Scalar multiplication distributive law for subtraction. ( hvsubdistr2 analog.) (Contributed by NM, 2-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lmodsubdir.v | |
|
lmodsubdir.t | |
||
lmodsubdir.f | |
||
lmodsubdir.k | |
||
lmodsubdir.m | |
||
lmodsubdir.s | |
||
lmodsubdir.w | |
||
lmodsubdir.a | |
||
lmodsubdir.b | |
||
lmodsubdir.x | |
||
Assertion | lmodsubdir | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmodsubdir.v | |
|
2 | lmodsubdir.t | |
|
3 | lmodsubdir.f | |
|
4 | lmodsubdir.k | |
|
5 | lmodsubdir.m | |
|
6 | lmodsubdir.s | |
|
7 | lmodsubdir.w | |
|
8 | lmodsubdir.a | |
|
9 | lmodsubdir.b | |
|
10 | lmodsubdir.x | |
|
11 | 3 | lmodring | |
12 | 7 11 | syl | |
13 | ringgrp | |
|
14 | 12 13 | syl | |
15 | eqid | |
|
16 | 4 15 | grpinvcl | |
17 | 14 9 16 | syl2anc | |
18 | eqid | |
|
19 | eqid | |
|
20 | 1 18 3 2 4 19 | lmodvsdir | |
21 | 7 8 17 10 20 | syl13anc | |
22 | eqid | |
|
23 | eqid | |
|
24 | 4 22 23 15 12 9 | ringnegl | |
25 | 24 | oveq1d | |
26 | 4 23 | ringidcl | |
27 | 12 26 | syl | |
28 | 4 15 | grpinvcl | |
29 | 14 27 28 | syl2anc | |
30 | 1 3 2 4 22 | lmodvsass | |
31 | 7 29 9 10 30 | syl13anc | |
32 | 25 31 | eqtr3d | |
33 | 32 | oveq2d | |
34 | 21 33 | eqtrd | |
35 | 4 19 15 6 | grpsubval | |
36 | 8 9 35 | syl2anc | |
37 | 36 | oveq1d | |
38 | 1 3 2 4 | lmodvscl | |
39 | 7 8 10 38 | syl3anc | |
40 | 1 3 2 4 | lmodvscl | |
41 | 7 9 10 40 | syl3anc | |
42 | 1 18 5 3 2 15 23 | lmodvsubval2 | |
43 | 7 39 41 42 | syl3anc | |
44 | 34 37 43 | 3eqtr4d | |