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

Metamath Proof Explorer

Theorem dipcn

Description: Inner product is jointly continuous in both arguments. (Contributed by NM, 21-Aug-2007) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Hypotheses dipcn.p ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
dipcn.c ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
dipcn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
dipcn.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion dipcn ( 𝑈 ∈ NrmCVec → 𝑃 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 dipcn.p ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
2 dipcn.c ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
3 dipcn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
4 dipcn.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
5 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
6 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
7 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
8 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
9 5 6 7 8 1 dipfval ⊢ ( 𝑈 ∈ NrmCVec → 𝑃 = ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) )
10 5 2 imsxmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) )
11 3 mopntopon ⊢ ( 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) → 𝐽 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑈 ) ) )
12 10 11 syl ⊢ ( 𝑈 ∈ NrmCVec → 𝐽 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑈 ) ) )
13 fzfid ⊢ ( 𝑈 ∈ NrmCVec → ( 1 ... 4 ) ∈ Fin )
14 12 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → 𝐽 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑈 ) ) )
15 4 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
16 15 a1i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → 𝐾 ∈ ( TopOn ‘ ℂ ) )
17 ax-icn ⊢ i ∈ ℂ
18 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 4 ) → 𝑘 ∈ ℕ )
19 18 adantl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → 𝑘 ∈ ℕ )
20 19 nnnn0d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → 𝑘 ∈ ℕ0 )
21 expcl ⊢ ( ( i ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( i ↑ 𝑘 ) ∈ ℂ )
22 17 20 21 sylancr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( i ↑ 𝑘 ) ∈ ℂ )
23 14 14 16 22 cnmpt2c ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( i ↑ 𝑘 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
24 14 14 cnmpt1st ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ 𝑥 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
25 14 14 cnmpt2nd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
26 2 3 7 4 smcn ⊢ ( 𝑈 ∈ NrmCVec → ( ·𝑠OLD ‘ 𝑈 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
27 26 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( ·𝑠OLD ‘ 𝑈 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
28 14 14 23 25 27 cnmpt22f ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
29 2 3 6 vacn ⊢ ( 𝑈 ∈ NrmCVec → ( +𝑣 ‘ 𝑈 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
30 29 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( +𝑣 ‘ 𝑈 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
31 14 14 24 28 30 cnmpt22f ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
32 8 2 3 4 nmcnc ⊢ ( 𝑈 ∈ NrmCVec → ( normCV ‘ 𝑈 ) ∈ ( 𝐽 Cn 𝐾 ) )
33 32 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( normCV ‘ 𝑈 ) ∈ ( 𝐽 Cn 𝐾 ) )
34 14 14 31 33 cnmpt21f ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
35 4 sqcn ⊢ ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 2 ) ) ∈ ( 𝐾 Cn 𝐾 )
36 35 a1i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 2 ) ) ∈ ( 𝐾 Cn 𝐾 ) )
37 oveq1 ⊢ ( 𝑧 = ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) → ( 𝑧 ↑ 2 ) = ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) )
38 14 14 34 16 36 37 cnmpt21 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
39 4 mulcn ⊢ · ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
40 39 a1i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → · ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
41 14 14 23 38 40 cnmpt22f ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
42 4 12 13 12 41 fsum2cn ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
43 15 a1i ⊢ ( 𝑈 ∈ NrmCVec → 𝐾 ∈ ( TopOn ‘ ℂ ) )
44 4cn ⊢ 4 ∈ ℂ
45 4ne0 ⊢ 4 ≠ 0
46 4 divccn ⊢ ( ( 4 ∈ ℂ ∧ 4 ≠ 0 ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 / 4 ) ) ∈ ( 𝐾 Cn 𝐾 ) )
47 44 45 46 mp2an ⊢ ( 𝑧 ∈ ℂ ↦ ( 𝑧 / 4 ) ) ∈ ( 𝐾 Cn 𝐾 )
48 47 a1i ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑧 ∈ ℂ ↦ ( 𝑧 / 4 ) ) ∈ ( 𝐾 Cn 𝐾 ) )
49 oveq1 ⊢ ( 𝑧 = Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) → ( 𝑧 / 4 ) = ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) )
50 12 12 42 43 48 49 cnmpt21 ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) , 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ↦ ( Σ 𝑘 ∈ ( 1 ... 4 ) ( ( i ↑ 𝑘 ) · ( ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( ( i ↑ 𝑘 ) ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) ↑ 2 ) ) / 4 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )
51 9 50 eqeltrd ⊢ ( 𝑈 ∈ NrmCVec → 𝑃 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )