This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnmpt2ip

Description: Continuity of inner product; analogue of cnmpt22f which cannot be used directly because .i is not a function. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses cnmpt1ip.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
cnmpt1ip.c ⊢ 𝐶 = ( TopOpen ‘ ℂfld )
cnmpt1ip.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
cnmpt1ip.r ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
cnmpt1ip.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
cnmpt2ip.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
cnmpt2ip.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
cnmpt2ip.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
Assertion cnmpt2ip ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 , 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cnmpt1ip.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
2 cnmpt1ip.c ⊢ 𝐶 = ( TopOpen ‘ ℂfld )
3 cnmpt1ip.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
4 cnmpt1ip.r ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
5 cnmpt1ip.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
6 cnmpt2ip.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
7 cnmpt2ip.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
8 cnmpt2ip.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
9 txtopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
10 5 6 9 syl2anc ⊢ ( 𝜑 → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
11 cphngp ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
12 ngptps ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ TopSp )
13 4 11 12 3syl ⊢ ( 𝜑 → 𝑊 ∈ TopSp )
14 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
15 14 1 istps ⊢ ( 𝑊 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
16 13 15 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
17 cnf2 ⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
18 10 16 7 17 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
19 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
20 19 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝑊 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
21 18 20 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝑊 ) )
22 21 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝑊 ) )
23 22 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ( Base ‘ 𝑊 ) )
24 cnf2 ⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
25 10 16 8 24 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
26 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
27 26 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝑊 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝑊 ) )
28 25 27 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝑊 ) )
29 28 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝑊 ) )
30 29 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ( Base ‘ 𝑊 ) )
31 eqid ⊢ ( ·if ‘ 𝑊 ) = ( ·if ‘ 𝑊 )
32 14 3 31 ipfval ⊢ ( ( 𝐴 ∈ ( Base ‘ 𝑊 ) ∧ 𝐵 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) = ( 𝐴 , 𝐵 ) )
33 23 30 32 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) = ( 𝐴 , 𝐵 ) )
34 33 3impa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) = ( 𝐴 , 𝐵 ) )
35 34 mpoeq3dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 , 𝐵 ) ) )
36 31 1 2 ipcn ⊢ ( 𝑊 ∈ ℂPreHil → ( ·if ‘ 𝑊 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐶 ) )
37 4 36 syl ⊢ ( 𝜑 → ( ·if ‘ 𝑊 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐶 ) )
38 5 6 7 8 37 cnmpt22f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 ( ·if ‘ 𝑊 ) 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐶 ) )
39 35 38 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 , 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐶 ) )