Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnmpt1vsca Structured version   Visualization version   GIF version

Theorem cnmpt1vsca 21937
 Description: Continuity of scalar multiplication; analogue of cnmpt12f 21409 which cannot be used directly because ·𝑠 is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
Hypotheses
Ref Expression
tlmtrg.f 𝐹 = (Scalar‘𝑊)
cnmpt1vsca.t · = ( ·𝑠𝑊)
cnmpt1vsca.j 𝐽 = (TopOpen‘𝑊)
cnmpt1vsca.k 𝐾 = (TopOpen‘𝐹)
cnmpt1vsca.w (𝜑𝑊 ∈ TopMod)
cnmpt1vsca.l (𝜑𝐿 ∈ (TopOn‘𝑋))
cnmpt1vsca.a (𝜑 → (𝑥𝑋𝐴) ∈ (𝐿 Cn 𝐾))
cnmpt1vsca.b (𝜑 → (𝑥𝑋𝐵) ∈ (𝐿 Cn 𝐽))
Assertion
Ref Expression
cnmpt1vsca (𝜑 → (𝑥𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝐿 Cn 𝐽))
Distinct variable groups:   𝑥,𝐹   𝑥,𝐽   𝑥,𝐾   𝑥,𝐿   𝜑,𝑥   𝑥,𝑊   𝑥,𝑋
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   · (𝑥)

Proof of Theorem cnmpt1vsca
StepHypRef Expression
1 cnmpt1vsca.l . . . . . . 7 (𝜑𝐿 ∈ (TopOn‘𝑋))
2 cnmpt1vsca.w . . . . . . . . 9 (𝜑𝑊 ∈ TopMod)
3 tlmtrg.f . . . . . . . . . 10 𝐹 = (Scalar‘𝑊)
43tlmscatps 21934 . . . . . . . . 9 (𝑊 ∈ TopMod → 𝐹 ∈ TopSp)
52, 4syl 17 . . . . . . . 8 (𝜑𝐹 ∈ TopSp)
6 eqid 2621 . . . . . . . . 9 (Base‘𝐹) = (Base‘𝐹)
7 cnmpt1vsca.k . . . . . . . . 9 𝐾 = (TopOpen‘𝐹)
86, 7istps 20678 . . . . . . . 8 (𝐹 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝐹)))
95, 8sylib 208 . . . . . . 7 (𝜑𝐾 ∈ (TopOn‘(Base‘𝐹)))
10 cnmpt1vsca.a . . . . . . 7 (𝜑 → (𝑥𝑋𝐴) ∈ (𝐿 Cn 𝐾))
11 cnf2 20993 . . . . . . 7 ((𝐿 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐹)) ∧ (𝑥𝑋𝐴) ∈ (𝐿 Cn 𝐾)) → (𝑥𝑋𝐴):𝑋⟶(Base‘𝐹))
121, 9, 10, 11syl3anc 1323 . . . . . 6 (𝜑 → (𝑥𝑋𝐴):𝑋⟶(Base‘𝐹))
13 eqid 2621 . . . . . . 7 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
1413fmpt 6347 . . . . . 6 (∀𝑥𝑋 𝐴 ∈ (Base‘𝐹) ↔ (𝑥𝑋𝐴):𝑋⟶(Base‘𝐹))
1512, 14sylibr 224 . . . . 5 (𝜑 → ∀𝑥𝑋 𝐴 ∈ (Base‘𝐹))
1615r19.21bi 2928 . . . 4 ((𝜑𝑥𝑋) → 𝐴 ∈ (Base‘𝐹))
17 tlmtps 21931 . . . . . . . . 9 (𝑊 ∈ TopMod → 𝑊 ∈ TopSp)
182, 17syl 17 . . . . . . . 8 (𝜑𝑊 ∈ TopSp)
19 eqid 2621 . . . . . . . . 9 (Base‘𝑊) = (Base‘𝑊)
20 cnmpt1vsca.j . . . . . . . . 9 𝐽 = (TopOpen‘𝑊)
2119, 20istps 20678 . . . . . . . 8 (𝑊 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘(Base‘𝑊)))
2218, 21sylib 208 . . . . . . 7 (𝜑𝐽 ∈ (TopOn‘(Base‘𝑊)))
23 cnmpt1vsca.b . . . . . . 7 (𝜑 → (𝑥𝑋𝐵) ∈ (𝐿 Cn 𝐽))
24 cnf2 20993 . . . . . . 7 ((𝐿 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘(Base‘𝑊)) ∧ (𝑥𝑋𝐵) ∈ (𝐿 Cn 𝐽)) → (𝑥𝑋𝐵):𝑋⟶(Base‘𝑊))
251, 22, 23, 24syl3anc 1323 . . . . . 6 (𝜑 → (𝑥𝑋𝐵):𝑋⟶(Base‘𝑊))
26 eqid 2621 . . . . . . 7 (𝑥𝑋𝐵) = (𝑥𝑋𝐵)
2726fmpt 6347 . . . . . 6 (∀𝑥𝑋 𝐵 ∈ (Base‘𝑊) ↔ (𝑥𝑋𝐵):𝑋⟶(Base‘𝑊))
2825, 27sylibr 224 . . . . 5 (𝜑 → ∀𝑥𝑋 𝐵 ∈ (Base‘𝑊))
2928r19.21bi 2928 . . . 4 ((𝜑𝑥𝑋) → 𝐵 ∈ (Base‘𝑊))
30 eqid 2621 . . . . 5 ( ·sf𝑊) = ( ·sf𝑊)
31 cnmpt1vsca.t . . . . 5 · = ( ·𝑠𝑊)
3219, 3, 6, 30, 31scafval 18822 . . . 4 ((𝐴 ∈ (Base‘𝐹) ∧ 𝐵 ∈ (Base‘𝑊)) → (𝐴( ·sf𝑊)𝐵) = (𝐴 · 𝐵))
3316, 29, 32syl2anc 692 . . 3 ((𝜑𝑥𝑋) → (𝐴( ·sf𝑊)𝐵) = (𝐴 · 𝐵))
3433mpteq2dva 4714 . 2 (𝜑 → (𝑥𝑋 ↦ (𝐴( ·sf𝑊)𝐵)) = (𝑥𝑋 ↦ (𝐴 · 𝐵)))
3530, 20, 3, 7vscacn 21929 . . . 4 (𝑊 ∈ TopMod → ( ·sf𝑊) ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
362, 35syl 17 . . 3 (𝜑 → ( ·sf𝑊) ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
371, 10, 23, 36cnmpt12f 21409 . 2 (𝜑 → (𝑥𝑋 ↦ (𝐴( ·sf𝑊)𝐵)) ∈ (𝐿 Cn 𝐽))
3834, 37eqeltrrd 2699 1 (𝜑 → (𝑥𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝐿 Cn 𝐽))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2908   ↦ cmpt 4683  ⟶wf 5853  ‘cfv 5857  (class class class)co 6615  Basecbs 15800  Scalarcsca 15884   ·𝑠 cvsca 15885  TopOpenctopn 16022   ·sf cscaf 18804  TopOnctopon 20655  TopSpctps 20676   Cn ccn 20968   ×t ctx 21303  TopModctlm 21901 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-fv 5865  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-1st 7128  df-2nd 7129  df-map 7819  df-slot 15804  df-base 15805  df-topgen 16044  df-scaf 18806  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-cn 20971  df-tx 21305  df-tmd 21816  df-tgp 21817  df-trg 21903  df-tlm 21905 This theorem is referenced by:  tlmtgp  21939
 Copyright terms: Public domain W3C validator