Description: Continuity of scalar multiplication; analogue of cnmpt22f 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 | |
||
cnmpt2vsca.m | |
||
cnmpt2vsca.a | |
||
cnmpt2vsca.b | |
||
Assertion | cnmpt2vsca | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tlmtrg.f | |
|
2 | cnmpt1vsca.t | |
|
3 | cnmpt1vsca.j | |
|
4 | cnmpt1vsca.k | |
|
5 | cnmpt1vsca.w | |
|
6 | cnmpt1vsca.l | |
|
7 | cnmpt2vsca.m | |
|
8 | cnmpt2vsca.a | |
|
9 | cnmpt2vsca.b | |
|
10 | txtopon | |
|
11 | 6 7 10 | syl2anc | |
12 | 1 | tlmscatps | |
13 | 5 12 | syl | |
14 | eqid | |
|
15 | 14 4 | istps | |
16 | 13 15 | sylib | |
17 | cnf2 | |
|
18 | 11 16 8 17 | syl3anc | |
19 | eqid | |
|
20 | 19 | fmpo | |
21 | 18 20 | sylibr | |
22 | 21 | r19.21bi | |
23 | 22 | r19.21bi | |
24 | tlmtps | |
|
25 | 5 24 | syl | |
26 | eqid | |
|
27 | 26 3 | istps | |
28 | 25 27 | sylib | |
29 | cnf2 | |
|
30 | 11 28 9 29 | syl3anc | |
31 | eqid | |
|
32 | 31 | fmpo | |
33 | 30 32 | sylibr | |
34 | 33 | r19.21bi | |
35 | 34 | r19.21bi | |
36 | eqid | |
|
37 | 26 1 14 36 2 | scafval | |
38 | 23 35 37 | syl2anc | |
39 | 38 | 3impa | |
40 | 39 | mpoeq3dva | |
41 | 36 3 1 4 | vscacn | |
42 | 5 41 | syl | |
43 | 6 7 8 9 42 | cnmpt22f | |
44 | 40 43 | eqeltrrd | |