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

Theorem cnmpt1vsca 22490
Description: Continuity of scalar multiplication; analogue of cnmpt12f 21963 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 . . . . . 6 (𝜑𝐿 ∈ (TopOn‘𝑋))
2 cnmpt1vsca.w . . . . . . . 8 (𝜑𝑊 ∈ TopMod)
3 tlmtrg.f . . . . . . . . 9 𝐹 = (Scalar‘𝑊)
43tlmscatps 22487 . . . . . . . 8 (𝑊 ∈ TopMod → 𝐹 ∈ TopSp)
52, 4syl 17 . . . . . . 7 (𝜑𝐹 ∈ TopSp)
6 eqid 2795 . . . . . . . 8 (Base‘𝐹) = (Base‘𝐹)
7 cnmpt1vsca.k . . . . . . . 8 𝐾 = (TopOpen‘𝐹)
86, 7istps 21231 . . . . . . 7 (𝐹 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘(Base‘𝐹)))
95, 8sylib 219 . . . . . 6 (𝜑𝐾 ∈ (TopOn‘(Base‘𝐹)))
10 cnmpt1vsca.a . . . . . 6 (𝜑 → (𝑥𝑋𝐴) ∈ (𝐿 Cn 𝐾))
11 cnf2 21546 . . . . . 6 ((𝐿 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐹)) ∧ (𝑥𝑋𝐴) ∈ (𝐿 Cn 𝐾)) → (𝑥𝑋𝐴):𝑋⟶(Base‘𝐹))
121, 9, 10, 11syl3anc 1364 . . . . 5 (𝜑 → (𝑥𝑋𝐴):𝑋⟶(Base‘𝐹))
1312fvmptelrn 6745 . . . 4 ((𝜑𝑥𝑋) → 𝐴 ∈ (Base‘𝐹))
14 tlmtps 22484 . . . . . . . 8 (𝑊 ∈ TopMod → 𝑊 ∈ TopSp)
152, 14syl 17 . . . . . . 7 (𝜑𝑊 ∈ TopSp)
16 eqid 2795 . . . . . . . 8 (Base‘𝑊) = (Base‘𝑊)
17 cnmpt1vsca.j . . . . . . . 8 𝐽 = (TopOpen‘𝑊)
1816, 17istps 21231 . . . . . . 7 (𝑊 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘(Base‘𝑊)))
1915, 18sylib 219 . . . . . 6 (𝜑𝐽 ∈ (TopOn‘(Base‘𝑊)))
20 cnmpt1vsca.b . . . . . 6 (𝜑 → (𝑥𝑋𝐵) ∈ (𝐿 Cn 𝐽))
21 cnf2 21546 . . . . . 6 ((𝐿 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘(Base‘𝑊)) ∧ (𝑥𝑋𝐵) ∈ (𝐿 Cn 𝐽)) → (𝑥𝑋𝐵):𝑋⟶(Base‘𝑊))
221, 19, 20, 21syl3anc 1364 . . . . 5 (𝜑 → (𝑥𝑋𝐵):𝑋⟶(Base‘𝑊))
2322fvmptelrn 6745 . . . 4 ((𝜑𝑥𝑋) → 𝐵 ∈ (Base‘𝑊))
24 eqid 2795 . . . . 5 ( ·sf𝑊) = ( ·sf𝑊)
25 cnmpt1vsca.t . . . . 5 · = ( ·𝑠𝑊)
2616, 3, 6, 24, 25scafval 19348 . . . 4 ((𝐴 ∈ (Base‘𝐹) ∧ 𝐵 ∈ (Base‘𝑊)) → (𝐴( ·sf𝑊)𝐵) = (𝐴 · 𝐵))
2713, 23, 26syl2anc 584 . . 3 ((𝜑𝑥𝑋) → (𝐴( ·sf𝑊)𝐵) = (𝐴 · 𝐵))
2827mpteq2dva 5060 . 2 (𝜑 → (𝑥𝑋 ↦ (𝐴( ·sf𝑊)𝐵)) = (𝑥𝑋 ↦ (𝐴 · 𝐵)))
2924, 17, 3, 7vscacn 22482 . . . 4 (𝑊 ∈ TopMod → ( ·sf𝑊) ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
302, 29syl 17 . . 3 (𝜑 → ( ·sf𝑊) ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
311, 10, 20, 30cnmpt12f 21963 . 2 (𝜑 → (𝑥𝑋 ↦ (𝐴( ·sf𝑊)𝐵)) ∈ (𝐿 Cn 𝐽))
3228, 31eqeltrrd 2884 1 (𝜑 → (𝑥𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝐿 Cn 𝐽))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1522  wcel 2081  cmpt 5045  wf 6226  cfv 6230  (class class class)co 7021  Basecbs 16317  Scalarcsca 16402   ·𝑠 cvsca 16403  TopOpenctopn 16529   ·sf cscaf 19330  TopOnctopon 21207  TopSpctps 21229   Cn ccn 21521   ×t ctx 21857  TopModctlm 22454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-fv 6238  df-ov 7024  df-oprab 7025  df-mpo 7026  df-1st 7550  df-2nd 7551  df-map 8263  df-slot 16321  df-base 16323  df-topgen 16551  df-scaf 19332  df-top 21191  df-topon 21208  df-topsp 21230  df-bases 21243  df-cn 21524  df-tx 21859  df-tmd 22369  df-tgp 22370  df-trg 22456  df-tlm 22458
This theorem is referenced by:  tlmtgp  22492
  Copyright terms: Public domain W3C validator