Metamath Proof Explorer


Theorem cnmpt2vsca

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 F=ScalarW
cnmpt1vsca.t ·˙=W
cnmpt1vsca.j J=TopOpenW
cnmpt1vsca.k K=TopOpenF
cnmpt1vsca.w φWTopMod
cnmpt1vsca.l φLTopOnX
cnmpt2vsca.m φMTopOnY
cnmpt2vsca.a φxX,yYAL×tMCnK
cnmpt2vsca.b φxX,yYBL×tMCnJ
Assertion cnmpt2vsca φxX,yYA·˙BL×tMCnJ

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 cnmpt2vsca.m φMTopOnY
8 cnmpt2vsca.a φxX,yYAL×tMCnK
9 cnmpt2vsca.b φxX,yYBL×tMCnJ
10 txtopon LTopOnXMTopOnYL×tMTopOnX×Y
11 6 7 10 syl2anc φL×tMTopOnX×Y
12 1 tlmscatps WTopModFTopSp
13 5 12 syl φFTopSp
14 eqid BaseF=BaseF
15 14 4 istps FTopSpKTopOnBaseF
16 13 15 sylib φKTopOnBaseF
17 cnf2 L×tMTopOnX×YKTopOnBaseFxX,yYAL×tMCnKxX,yYA:X×YBaseF
18 11 16 8 17 syl3anc φxX,yYA:X×YBaseF
19 eqid xX,yYA=xX,yYA
20 19 fmpo xXyYABaseFxX,yYA:X×YBaseF
21 18 20 sylibr φxXyYABaseF
22 21 r19.21bi φxXyYABaseF
23 22 r19.21bi φxXyYABaseF
24 tlmtps WTopModWTopSp
25 5 24 syl φWTopSp
26 eqid BaseW=BaseW
27 26 3 istps WTopSpJTopOnBaseW
28 25 27 sylib φJTopOnBaseW
29 cnf2 L×tMTopOnX×YJTopOnBaseWxX,yYBL×tMCnJxX,yYB:X×YBaseW
30 11 28 9 29 syl3anc φxX,yYB:X×YBaseW
31 eqid xX,yYB=xX,yYB
32 31 fmpo xXyYBBaseWxX,yYB:X×YBaseW
33 30 32 sylibr φxXyYBBaseW
34 33 r19.21bi φxXyYBBaseW
35 34 r19.21bi φxXyYBBaseW
36 eqid 𝑠𝑓W=𝑠𝑓W
37 26 1 14 36 2 scafval ABaseFBBaseWA𝑠𝑓WB=A·˙B
38 23 35 37 syl2anc φxXyYA𝑠𝑓WB=A·˙B
39 38 3impa φxXyYA𝑠𝑓WB=A·˙B
40 39 mpoeq3dva φxX,yYA𝑠𝑓WB=xX,yYA·˙B
41 36 3 1 4 vscacn WTopMod𝑠𝑓WK×tJCnJ
42 5 41 syl φ𝑠𝑓WK×tJCnJ
43 6 7 8 9 42 cnmpt22f φxX,yYA𝑠𝑓WBL×tMCnJ
44 40 43 eqeltrrd φxX,yYA·˙BL×tMCnJ