Description: Scalar multiplication in a free module at the coordinates. (Contributed by AV, 16-Jan-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frlmplusgvalb.f | |
|
frlmplusgvalb.b | |
||
frlmplusgvalb.i | |
||
frlmplusgvalb.x | |
||
frlmplusgvalb.z | |
||
frlmplusgvalb.r | |
||
frlmvscavalb.k | |
||
frlmvscavalb.a | |
||
frlmvscavalb.v | |
||
frlmvscavalb.t | |
||
Assertion | frlmvscavalb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frlmplusgvalb.f | |
|
2 | frlmplusgvalb.b | |
|
3 | frlmplusgvalb.i | |
|
4 | frlmplusgvalb.x | |
|
5 | frlmplusgvalb.z | |
|
6 | frlmplusgvalb.r | |
|
7 | frlmvscavalb.k | |
|
8 | frlmvscavalb.a | |
|
9 | frlmvscavalb.v | |
|
10 | frlmvscavalb.t | |
|
11 | 1 7 2 | frlmbasmap | |
12 | 3 5 11 | syl2anc | |
13 | 7 | fvexi | |
14 | 13 | a1i | |
15 | 14 3 | elmapd | |
16 | 12 15 | mpbid | |
17 | 16 | ffnd | |
18 | 1 | frlmlmod | |
19 | 6 3 18 | syl2anc | |
20 | 8 7 | eleqtrdi | |
21 | 1 | frlmsca | |
22 | 6 3 21 | syl2anc | |
23 | 22 | fveq2d | |
24 | 20 23 | eleqtrd | |
25 | eqid | |
|
26 | eqid | |
|
27 | 2 25 9 26 | lmodvscl | |
28 | 19 24 4 27 | syl3anc | |
29 | 1 7 2 | frlmbasmap | |
30 | 3 28 29 | syl2anc | |
31 | 14 3 | elmapd | |
32 | 30 31 | mpbid | |
33 | 32 | ffnd | |
34 | eqfnfv | |
|
35 | 17 33 34 | syl2anc | |
36 | 3 | adantr | |
37 | 8 | adantr | |
38 | 4 | adantr | |
39 | simpr | |
|
40 | 1 2 7 36 37 38 39 9 10 | frlmvscaval | |
41 | 40 | eqeq2d | |
42 | 41 | ralbidva | |
43 | 35 42 | bitrd | |