Proof of Theorem cnmpt2vsca
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cnmpt1vsca.l | . . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑋)) | 
| 2 |  | cnmpt2vsca.m | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑌)) | 
| 3 |  | txtopon 23600 | . . . . . . . . . 10
⊢ ((𝐿 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ (TopOn‘𝑌)) → (𝐿 ×t 𝑀) ∈ (TopOn‘(𝑋 × 𝑌))) | 
| 4 | 1, 2, 3 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐿 ×t 𝑀) ∈ (TopOn‘(𝑋 × 𝑌))) | 
| 5 |  | cnmpt1vsca.w | . . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ TopMod) | 
| 6 |  | tlmtrg.f | . . . . . . . . . . . 12
⊢ 𝐹 = (Scalar‘𝑊) | 
| 7 | 6 | tlmscatps 24200 | . . . . . . . . . . 11
⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp) | 
| 8 | 5, 7 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ TopSp) | 
| 9 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘𝐹) =
(Base‘𝐹) | 
| 10 |  | cnmpt1vsca.k | . . . . . . . . . . 11
⊢ 𝐾 = (TopOpen‘𝐹) | 
| 11 | 9, 10 | istps 22941 | . . . . . . . . . 10
⊢ (𝐹 ∈ TopSp ↔ 𝐾 ∈
(TopOn‘(Base‘𝐹))) | 
| 12 | 8, 11 | sylib 218 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝐹))) | 
| 13 |  | cnmpt2vsca.a | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐿 ×t 𝑀) Cn 𝐾)) | 
| 14 |  | cnf2 23258 | . . . . . . . . 9
⊢ (((𝐿 ×t 𝑀) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐹)) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐿 ×t 𝑀) Cn 𝐾)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶(Base‘𝐹)) | 
| 15 | 4, 12, 13, 14 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶(Base‘𝐹)) | 
| 16 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) | 
| 17 | 16 | fmpo 8094 | . . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ (Base‘𝐹) ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶(Base‘𝐹)) | 
| 18 | 15, 17 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ (Base‘𝐹)) | 
| 19 | 18 | r19.21bi 3250 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐴 ∈ (Base‘𝐹)) | 
| 20 | 19 | r19.21bi 3250 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ (Base‘𝐹)) | 
| 21 |  | tlmtps 24197 | . . . . . . . . . . 11
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp) | 
| 22 | 5, 21 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ TopSp) | 
| 23 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘𝑊) =
(Base‘𝑊) | 
| 24 |  | cnmpt1vsca.j | . . . . . . . . . . 11
⊢ 𝐽 = (TopOpen‘𝑊) | 
| 25 | 23, 24 | istps 22941 | . . . . . . . . . 10
⊢ (𝑊 ∈ TopSp ↔ 𝐽 ∈
(TopOn‘(Base‘𝑊))) | 
| 26 | 22, 25 | sylib 218 | . . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝑊))) | 
| 27 |  | cnmpt2vsca.b | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐿 ×t 𝑀) Cn 𝐽)) | 
| 28 |  | cnf2 23258 | . . . . . . . . 9
⊢ (((𝐿 ×t 𝑀) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐽 ∈ (TopOn‘(Base‘𝑊)) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐿 ×t 𝑀) Cn 𝐽)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶(Base‘𝑊)) | 
| 29 | 4, 26, 27, 28 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶(Base‘𝑊)) | 
| 30 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) | 
| 31 | 30 | fmpo 8094 | . . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐵 ∈ (Base‘𝑊) ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶(Base‘𝑊)) | 
| 32 | 29, 31 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐵 ∈ (Base‘𝑊)) | 
| 33 | 32 | r19.21bi 3250 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐵 ∈ (Base‘𝑊)) | 
| 34 | 33 | r19.21bi 3250 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝐵 ∈ (Base‘𝑊)) | 
| 35 |  | eqid 2736 | . . . . . 6
⊢ (
·sf ‘𝑊) = ( ·sf
‘𝑊) | 
| 36 |  | cnmpt1vsca.t | . . . . . 6
⊢  · = (
·𝑠 ‘𝑊) | 
| 37 | 23, 6, 9, 35, 36 | scafval 20880 | . . . . 5
⊢ ((𝐴 ∈ (Base‘𝐹) ∧ 𝐵 ∈ (Base‘𝑊)) → (𝐴( ·sf
‘𝑊)𝐵) = (𝐴 · 𝐵)) | 
| 38 | 20, 34, 37 | syl2anc 584 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝐴( ·sf
‘𝑊)𝐵) = (𝐴 · 𝐵)) | 
| 39 | 38 | 3impa 1109 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝐴( ·sf
‘𝑊)𝐵) = (𝐴 · 𝐵)) | 
| 40 | 39 | mpoeq3dva 7511 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴( ·sf
‘𝑊)𝐵)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 · 𝐵))) | 
| 41 | 35, 24, 6, 10 | vscacn 24195 | . . . 4
⊢ (𝑊 ∈ TopMod → (
·sf ‘𝑊) ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) | 
| 42 | 5, 41 | syl 17 | . . 3
⊢ (𝜑 → (
·sf ‘𝑊) ∈ ((𝐾 ×t 𝐽) Cn 𝐽)) | 
| 43 | 1, 2, 13, 27, 42 | cnmpt22f 23684 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴( ·sf
‘𝑊)𝐵)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽)) | 
| 44 | 40, 43 | eqeltrrd 2841 | 1
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 · 𝐵)) ∈ ((𝐿 ×t 𝑀) Cn 𝐽)) |