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 𝐾 ) )