Description: Continuity of scalar multiplication; analogue of cnmpt12f which cannot be used directly because .s is not a function. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tlmtrg.f | |
|
cnmpt1vsca.t | |
||
cnmpt1vsca.j | |
||
cnmpt1vsca.k | |
||
cnmpt1vsca.w | |
||
cnmpt1vsca.l | |
||
cnmpt1vsca.a | |
||
cnmpt1vsca.b | |
||
Assertion | cnmpt1vsca | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tlmtrg.f | |
|
2 | cnmpt1vsca.t | |
|
3 | cnmpt1vsca.j | |
|
4 | cnmpt1vsca.k | |
|
5 | cnmpt1vsca.w | |
|
6 | cnmpt1vsca.l | |
|
7 | cnmpt1vsca.a | |
|
8 | cnmpt1vsca.b | |
|
9 | 1 | tlmscatps | |
10 | 5 9 | syl | |
11 | eqid | |
|
12 | 11 4 | istps | |
13 | 10 12 | sylib | |
14 | cnf2 | |
|
15 | 6 13 7 14 | syl3anc | |
16 | 15 | fvmptelrn | |
17 | tlmtps | |
|
18 | 5 17 | syl | |
19 | eqid | |
|
20 | 19 3 | istps | |
21 | 18 20 | sylib | |
22 | cnf2 | |
|
23 | 6 21 8 22 | syl3anc | |
24 | 23 | fvmptelrn | |
25 | eqid | |
|
26 | 19 1 11 25 2 | scafval | |
27 | 16 24 26 | syl2anc | |
28 | 27 | mpteq2dva | |
29 | 25 3 1 4 | vscacn | |
30 | 5 29 | syl | |
31 | 6 7 8 30 | cnmpt12f | |
32 | 28 31 | eqeltrrd | |