Metamath Proof Explorer


Theorem cnmpt1vsca

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 F=ScalarW
cnmpt1vsca.t ·˙=W
cnmpt1vsca.j J=TopOpenW
cnmpt1vsca.k K=TopOpenF
cnmpt1vsca.w φWTopMod
cnmpt1vsca.l φLTopOnX
cnmpt1vsca.a φxXALCnK
cnmpt1vsca.b φxXBLCnJ
Assertion cnmpt1vsca φxXA·˙BLCnJ

Proof

Step Hyp Ref Expression
1 tlmtrg.f F=ScalarW
2 cnmpt1vsca.t ·˙=W
3 cnmpt1vsca.j J=TopOpenW
4 cnmpt1vsca.k K=TopOpenF
5 cnmpt1vsca.w φWTopMod
6 cnmpt1vsca.l φLTopOnX
7 cnmpt1vsca.a φxXALCnK
8 cnmpt1vsca.b φxXBLCnJ
9 1 tlmscatps WTopModFTopSp
10 5 9 syl φFTopSp
11 eqid BaseF=BaseF
12 11 4 istps FTopSpKTopOnBaseF
13 10 12 sylib φKTopOnBaseF
14 cnf2 LTopOnXKTopOnBaseFxXALCnKxXA:XBaseF
15 6 13 7 14 syl3anc φxXA:XBaseF
16 15 fvmptelrn φxXABaseF
17 tlmtps WTopModWTopSp
18 5 17 syl φWTopSp
19 eqid BaseW=BaseW
20 19 3 istps WTopSpJTopOnBaseW
21 18 20 sylib φJTopOnBaseW
22 cnf2 LTopOnXJTopOnBaseWxXBLCnJxXB:XBaseW
23 6 21 8 22 syl3anc φxXB:XBaseW
24 23 fvmptelrn φxXBBaseW
25 eqid 𝑠𝑓W=𝑠𝑓W
26 19 1 11 25 2 scafval ABaseFBBaseWA𝑠𝑓WB=A·˙B
27 16 24 26 syl2anc φxXA𝑠𝑓WB=A·˙B
28 27 mpteq2dva φxXA𝑠𝑓WB=xXA·˙B
29 25 3 1 4 vscacn WTopMod𝑠𝑓WK×tJCnJ
30 5 29 syl φ𝑠𝑓WK×tJCnJ
31 6 7 8 30 cnmpt12f φxXA𝑠𝑓WBLCnJ
32 28 31 eqeltrrd φxXA·˙BLCnJ