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	$⊢ P = \cdot_{𝑖OLD} (U)$
	dipcn.c	$⊢ C = IndMet (U)$
	dipcn.j	$⊢ J = MetOpen (C)$
	dipcn.k	$⊢ K = TopOpen (ℂ_{fld})$
Assertion	dipcn	$⊢ U \in NrmCVec \to P \in ((J \times_{t} J) Cn K)$

Proof

Step	Hyp	Ref	Expression
1		dipcn.p	$⊢ P = \cdot_{𝑖OLD} (U)$
2		dipcn.c	$⊢ C = IndMet (U)$
3		dipcn.j	$⊢ J = MetOpen (C)$
4		dipcn.k	$⊢ K = TopOpen (ℂ_{fld})$
5		eqid	$⊢ BaseSet (U) = BaseSet (U)$
6		eqid	$⊢ +_{v} (U) = +_{v} (U)$
7		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
8		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
9	5 6 7 8 1	dipfval	$⊢ U \in NrmCVec \to P = (x \in BaseSet (U), y \in BaseSet (U) ⟼ \frac{\sum_{k = 1}^{4} i^{k} {{norm}_{CV} (U) (x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y))}^{2}}{4})$
10	5 2	imsxmet	$⊢ U \in NrmCVec \to C \in ∞Met (BaseSet (U))$
11	3	mopntopon	$⊢ C \in ∞Met (BaseSet (U)) \to J \in TopOn (BaseSet (U))$
12	10 11	syl	$⊢ U \in NrmCVec \to J \in TopOn (BaseSet (U))$
13		fzfid	$⊢ U \in NrmCVec \to (1 \dots 4) \in Fin$
14	12	adantr	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to J \in TopOn (BaseSet (U))$
15	4	cnfldtopon	$⊢ K \in TopOn (ℂ)$
16	15	a1i	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to K \in TopOn (ℂ)$
17		ax-icn	$⊢ i \in ℂ$
18		elfznn	$⊢ k \in (1 \dots 4) \to k \in ℕ$
19	18	adantl	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to k \in ℕ$
20	19	nnnn0d	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to k \in ℕ_{0}$
21		expcl	$⊢ (i \in ℂ \land k \in ℕ_{0}) \to i^{k} \in ℂ$
22	17 20 21	sylancr	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to i^{k} \in ℂ$
23	14 14 16 22	cnmpt2c	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to (x \in BaseSet (U), y \in BaseSet (U) ⟼ i^{k}) \in ((J \times_{t} J) Cn K)$
24	14 14	cnmpt1st	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to (x \in BaseSet (U), y \in BaseSet (U) ⟼ x) \in ((J \times_{t} J) Cn J)$
25	14 14	cnmpt2nd	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to (x \in BaseSet (U), y \in BaseSet (U) ⟼ y) \in ((J \times_{t} J) Cn J)$
26	2 3 7 4	smcn	$⊢ U \in NrmCVec \to \cdot_{𝑠OLD} (U) \in ((K \times_{t} J) Cn J)$
27	26	adantr	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to \cdot_{𝑠OLD} (U) \in ((K \times_{t} J) Cn J)$
28	14 14 23 25 27	cnmpt22f	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to (x \in BaseSet (U), y \in BaseSet (U) ⟼ i^{k} \cdot_{𝑠OLD} (U) y) \in ((J \times_{t} J) Cn J)$
29	2 3 6	vacn	$⊢ U \in NrmCVec \to +_{v} (U) \in ((J \times_{t} J) Cn J)$
30	29	adantr	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to +_{v} (U) \in ((J \times_{t} J) Cn J)$
31	14 14 24 28 30	cnmpt22f	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to (x \in BaseSet (U), y \in BaseSet (U) ⟼ x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y)) \in ((J \times_{t} J) Cn J)$
32	8 2 3 4	nmcnc	$⊢ U \in NrmCVec \to {norm}_{CV} (U) \in (J Cn K)$
33	32	adantr	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to {norm}_{CV} (U) \in (J Cn K)$
34	14 14 31 33	cnmpt21f	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to (x \in BaseSet (U), y \in BaseSet (U) ⟼ {norm}_{CV} (U) (x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y))) \in ((J \times_{t} J) Cn K)$
35	4	sqcn	$⊢ (z \in ℂ ⟼ z^{2}) \in (K Cn K)$
36	35	a1i	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to (z \in ℂ ⟼ z^{2}) \in (K Cn K)$
37		oveq1	$⊢ z = {norm}_{CV} (U) (x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y)) \to z^{2} = {{norm}_{CV} (U) (x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y))}^{2}$
38	14 14 34 16 36 37	cnmpt21	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to (x \in BaseSet (U), y \in BaseSet (U) ⟼ {{norm}_{CV} (U) (x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y))}^{2}) \in ((J \times_{t} J) Cn K)$
39	4	mulcn	$⊢ \times \in ((K \times_{t} K) Cn K)$
40	39	a1i	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to \times \in ((K \times_{t} K) Cn K)$
41	14 14 23 38 40	cnmpt22f	$⊢ (U \in NrmCVec \land k \in (1 \dots 4)) \to (x \in BaseSet (U), y \in BaseSet (U) ⟼ i^{k} {{norm}_{CV} (U) (x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y))}^{2}) \in ((J \times_{t} J) Cn K)$
42	4 12 13 12 41	fsum2cn	$⊢ U \in NrmCVec \to (x \in BaseSet (U), y \in BaseSet (U) ⟼ \sum_{k = 1}^{4} i^{k} {{norm}_{CV} (U) (x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y))}^{2}) \in ((J \times_{t} J) Cn K)$
43	15	a1i	$⊢ U \in NrmCVec \to K \in TopOn (ℂ)$
44		4cn	$⊢ 4 \in ℂ$
45		4ne0	$⊢ 4 \neq 0$
46	4	divccn	$⊢ (4 \in ℂ \land 4 \neq 0) \to (z \in ℂ ⟼ \frac{z}{4}) \in (K Cn K)$
47	44 45 46	mp2an	$⊢ (z \in ℂ ⟼ \frac{z}{4}) \in (K Cn K)$
48	47	a1i	$⊢ U \in NrmCVec \to (z \in ℂ ⟼ \frac{z}{4}) \in (K Cn K)$
49		oveq1	$⊢ z = \sum_{k = 1}^{4} i^{k} {{norm}_{CV} (U) (x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y))}^{2} \to \frac{z}{4} = \frac{\sum_{k = 1}^{4} i^{k} {{norm}_{CV} (U) (x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y))}^{2}}{4}$
50	12 12 42 43 48 49	cnmpt21	$⊢ U \in NrmCVec \to (x \in BaseSet (U), y \in BaseSet (U) ⟼ \frac{\sum_{k = 1}^{4} i^{k} {{norm}_{CV} (U) (x +_{v} (U) (i^{k} \cdot_{𝑠OLD} (U) y))}^{2}}{4}) \in ((J \times_{t} J) Cn K)$
51	9 50	eqeltrd	$⊢ U \in NrmCVec \to P \in ((J \times_{t} J) Cn K)$

Metamath Proof Explorer

Theorem dipcn

Proof