ipcn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ipcn		Structured version Visualization version GIF version

Theorem ipcn 25475

Description: The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.)

**Hypotheses**
Ref	Expression
ipcn.f	⊢ , = (·_if‘𝑊)
ipcn.j	⊢ 𝐽 = (TopOpen‘𝑊)
ipcn.k	⊢ 𝐾 = (TopOpen‘ℂ_fld)

**Assertion**
Ref	Expression
ipcn	⊢ (𝑊 ∈ ℂPreHil → , ∈ ((𝐽 ×_t 𝐽) Cn 𝐾))

Proof of Theorem ipcn Dummy variables 𝑠 𝑟 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cphphl 25400	. . . . 5 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)
2		eqid 2760	. . . . . 6 ⊢ (Base‘𝑊) = (Base‘𝑊)
3		ipcn.f	. . . . . 6 ⊢ , = (·_if‘𝑊)
4		eqid 2760	. . . . . 6 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2760	. . . . . 6 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6	2, 3, 4, 5	phlipf 21866	. . . . 5 ⊢ (𝑊 ∈ PreHil → , :((Base‘𝑊) × (Base‘𝑊))⟶(Base‘(Scalar‘𝑊)))
7	1, 6	syl 18	. . . 4 ⊢ (𝑊 ∈ ℂPreHil → , :((Base‘𝑊) × (Base‘𝑊))⟶(Base‘(Scalar‘𝑊)))
8		cphclm 25418	. . . . 5 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod)
9	4, 5	clmsscn 25308	. . . . 5 ⊢ (𝑊 ∈ ℂMod → (Base‘(Scalar‘𝑊)) ⊆ ℂ)
10	8, 9	syl 18	. . . 4 ⊢ (𝑊 ∈ ℂPreHil → (Base‘(Scalar‘𝑊)) ⊆ ℂ)
11	7, 10	fssd 6721	. . 3 ⊢ (𝑊 ∈ ℂPreHil → , :((Base‘𝑊) × (Base‘𝑊))⟶ℂ)
12		eqid 2760	. . . . . . 7 ⊢ (·_𝑖‘𝑊) = (·_𝑖‘𝑊)
13		eqid 2760	. . . . . . 7 ⊢ (dist‘𝑊) = (dist‘𝑊)
14		eqid 2760	. . . . . . 7 ⊢ (norm‘𝑊) = (norm‘𝑊)
15		eqid 2760	. . . . . . 7 ⊢ ((𝑟 / 2) / (((norm‘𝑊)‘𝑥) + 1)) = ((𝑟 / 2) / (((norm‘𝑊)‘𝑥) + 1))
16		eqid 2760	. . . . . . 7 ⊢ ((𝑟 / 2) / (((norm‘𝑊)‘𝑦) + ((𝑟 / 2) / (((norm‘𝑊)‘𝑥) + 1)))) = ((𝑟 / 2) / (((norm‘𝑊)‘𝑦) + ((𝑟 / 2) / (((norm‘𝑊)‘𝑥) + 1))))
17		simpll 779	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ 𝑟 ∈ ℝ⁺) → 𝑊 ∈ ℂPreHil)
18		simplrl 789	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ 𝑟 ∈ ℝ⁺) → 𝑥 ∈ (Base‘𝑊))
19		simplrr 790	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ 𝑟 ∈ ℝ⁺) → 𝑦 ∈ (Base‘𝑊))
20		simpr 490	. . . . . . 7 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ⁺)
21	2, 12, 13, 14, 15, 16, 17, 18, 19, 20	ipcnlem1 25474	. . . . . 6 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ 𝑟 ∈ ℝ⁺) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥(dist‘𝑊)𝑧) < 𝑠 ∧ (𝑦(dist‘𝑊)𝑤) < 𝑠) → (abs‘((𝑥(·_𝑖‘𝑊)𝑦) − (𝑧(·_𝑖‘𝑊)𝑤))) < 𝑟))
22	21	ralrimiva 3154	. . . . 5 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥(dist‘𝑊)𝑧) < 𝑠 ∧ (𝑦(dist‘𝑊)𝑤) < 𝑠) → (abs‘((𝑥(·_𝑖‘𝑊)𝑦) − (𝑧(·_𝑖‘𝑊)𝑤))) < 𝑟))
23		simplrl 789	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → 𝑥 ∈ (Base‘𝑊))
24		simprl 783	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → 𝑧 ∈ (Base‘𝑊))
25	23, 24	ovresd 7581	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → (𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) = (𝑥(dist‘𝑊)𝑧))
26	25	breq1d 5113	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → ((𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) < 𝑠 ↔ (𝑥(dist‘𝑊)𝑧) < 𝑠))
27		simplrr 790	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → 𝑦 ∈ (Base‘𝑊))
28		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → 𝑤 ∈ (Base‘𝑊))
29	27, 28	ovresd 7581	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → (𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) = (𝑦(dist‘𝑊)𝑤))
30	29	breq1d 5113	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → ((𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) < 𝑠 ↔ (𝑦(dist‘𝑊)𝑤) < 𝑠))
31	26, 30	anbi12d 644	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → (((𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) < 𝑠 ∧ (𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) < 𝑠) ↔ ((𝑥(dist‘𝑊)𝑧) < 𝑠 ∧ (𝑦(dist‘𝑊)𝑤) < 𝑠)))
32	11	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → , :((Base‘𝑊) × (Base‘𝑊))⟶ℂ)
33	32, 23, 27	fovcdmd 7587	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → (𝑥 , 𝑦) ∈ ℂ)
34	32, 24, 28	fovcdmd 7587	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → (𝑧 , 𝑤) ∈ ℂ)
35		eqid 2760	. . . . . . . . . . . . 13 ⊢ (abs ∘ − ) = (abs ∘ − )
36	35	cnmetdval 24997	. . . . . . . . . . . 12 ⊢ (((𝑥 , 𝑦) ∈ ℂ ∧ (𝑧 , 𝑤) ∈ ℂ) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) = (abs‘((𝑥 , 𝑦) − (𝑧 , 𝑤))))
37	33, 34, 36	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) = (abs‘((𝑥 , 𝑦) − (𝑧 , 𝑤))))
38	2, 12, 3	ipfval 21863	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑥 , 𝑦) = (𝑥(·_𝑖‘𝑊)𝑦))
39	23, 27, 38	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → (𝑥 , 𝑦) = (𝑥(·_𝑖‘𝑊)𝑦))
40	2, 12, 3	ipfval 21863	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊)) → (𝑧 , 𝑤) = (𝑧(·_𝑖‘𝑊)𝑤))
41	40	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → (𝑧 , 𝑤) = (𝑧(·_𝑖‘𝑊)𝑤))
42	39, 41	oveq12d 7432	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → ((𝑥 , 𝑦) − (𝑧 , 𝑤)) = ((𝑥(·_𝑖‘𝑊)𝑦) − (𝑧(·_𝑖‘𝑊)𝑤)))
43	42	fveq2d 6883	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → (abs‘((𝑥 , 𝑦) − (𝑧 , 𝑤))) = (abs‘((𝑥(·_𝑖‘𝑊)𝑦) − (𝑧(·_𝑖‘𝑊)𝑤))))
44	37, 43	eqtrd 2795	. . . . . . . . . 10 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) = (abs‘((𝑥(·_𝑖‘𝑊)𝑦) − (𝑧(·_𝑖‘𝑊)𝑤))))
45	44	breq1d 5113	. . . . . . . . 9 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → (((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) < 𝑟 ↔ (abs‘((𝑥(·_𝑖‘𝑊)𝑦) − (𝑧(·_𝑖‘𝑊)𝑤))) < 𝑟))
46	31, 45	imbi12d 347	. . . . . . . 8 ⊢ (((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) ∧ (𝑧 ∈ (Base‘𝑊) ∧ 𝑤 ∈ (Base‘𝑊))) → ((((𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) < 𝑠 ∧ (𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) < 𝑠) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) < 𝑟) ↔ (((𝑥(dist‘𝑊)𝑧) < 𝑠 ∧ (𝑦(dist‘𝑊)𝑤) < 𝑠) → (abs‘((𝑥(·_𝑖‘𝑊)𝑦) − (𝑧(·_𝑖‘𝑊)𝑤))) < 𝑟)))
47	46	2ralbidva 3224	. . . . . . 7 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) < 𝑠 ∧ (𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) < 𝑠) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) < 𝑟) ↔ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥(dist‘𝑊)𝑧) < 𝑠 ∧ (𝑦(dist‘𝑊)𝑤) < 𝑠) → (abs‘((𝑥(·_𝑖‘𝑊)𝑦) − (𝑧(·_𝑖‘𝑊)𝑤))) < 𝑟)))
48	47	rexbidv 3186	. . . . . 6 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) < 𝑠 ∧ (𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) < 𝑠) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) < 𝑟) ↔ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥(dist‘𝑊)𝑧) < 𝑠 ∧ (𝑦(dist‘𝑊)𝑤) < 𝑠) → (abs‘((𝑥(·_𝑖‘𝑊)𝑦) − (𝑧(·_𝑖‘𝑊)𝑤))) < 𝑟)))
49	48	ralbidv 3185	. . . . 5 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) < 𝑠 ∧ (𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) < 𝑠) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) < 𝑟) ↔ ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥(dist‘𝑊)𝑧) < 𝑠 ∧ (𝑦(dist‘𝑊)𝑤) < 𝑠) → (abs‘((𝑥(·_𝑖‘𝑊)𝑦) − (𝑧(·_𝑖‘𝑊)𝑤))) < 𝑟)))
50	22, 49	mpbird 260	. . . 4 ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) < 𝑠 ∧ (𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) < 𝑠) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) < 𝑟))
51	50	ralrimivva 3205	. . 3 ⊢ (𝑊 ∈ ℂPreHil → ∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) < 𝑠 ∧ (𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) < 𝑠) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) < 𝑟))
52		cphngp 25402	. . . . . . 7 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)
53		ngpms 24827	. . . . . . 7 ⊢ (𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp)
54	52, 53	syl 18	. . . . . 6 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ MetSp)
55		msxms 24681	. . . . . 6 ⊢ (𝑊 ∈ MetSp → 𝑊 ∈ ∞MetSp)
56	54, 55	syl 18	. . . . 5 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ∞MetSp)
57		eqid 2760	. . . . . 6 ⊢ ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) = ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))
58	2, 57	xmsxmet 24683	. . . . 5 ⊢ (𝑊 ∈ ∞MetSp → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (∞Met‘(Base‘𝑊)))
59	56, 58	syl 18	. . . 4 ⊢ (𝑊 ∈ ℂPreHil → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (∞Met‘(Base‘𝑊)))
60		cnxmet 24999	. . . . 5 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
61	60	a1i 11	. . . 4 ⊢ (𝑊 ∈ ℂPreHil → (abs ∘ − ) ∈ (∞Met‘ℂ))
62		eqid 2760	. . . . 5 ⊢ (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) = (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))
63		ipcn.k	. . . . . 6 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
64	63	cnfldtopn 25008	. . . . 5 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
65	62, 62, 64	txmetcn 24775	. . . 4 ⊢ ((((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (∞Met‘(Base‘𝑊)) ∧ ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (∞Met‘(Base‘𝑊)) ∧ (abs ∘ − ) ∈ (∞Met‘ℂ)) → ( , ∈ (((MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ×_t (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))) Cn 𝐾) ↔ ( , :((Base‘𝑊) × (Base‘𝑊))⟶ℂ ∧ ∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) < 𝑠 ∧ (𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) < 𝑠) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) < 𝑟))))
66	59, 59, 61, 65	syl3anc 1398	. . 3 ⊢ (𝑊 ∈ ℂPreHil → ( , ∈ (((MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ×_t (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))) Cn 𝐾) ↔ ( , :((Base‘𝑊) × (Base‘𝑊))⟶ℂ ∧ ∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑥((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑧) < 𝑠 ∧ (𝑦((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝑤) < 𝑠) → ((𝑥 , 𝑦)(abs ∘ − )(𝑧 , 𝑤)) < 𝑟))))
67	11, 51, 66	mpbir2and 726	. 2 ⊢ (𝑊 ∈ ℂPreHil → , ∈ (((MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ×_t (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))) Cn 𝐾))
68		ipcn.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝑊)
69	68, 2, 57	mstopn 24679	. . . . 5 ⊢ (𝑊 ∈ MetSp → 𝐽 = (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))))
70	54, 69	syl 18	. . . 4 ⊢ (𝑊 ∈ ℂPreHil → 𝐽 = (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))))
71	70, 70	oveq12d 7432	. . 3 ⊢ (𝑊 ∈ ℂPreHil → (𝐽 ×_t 𝐽) = ((MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ×_t (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))))
72	71	oveq1d 7429	. 2 ⊢ (𝑊 ∈ ℂPreHil → ((𝐽 ×_t 𝐽) Cn 𝐾) = (((MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ×_t (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))) Cn 𝐾))
73	67, 72	eleqtrrd 2863	1 ⊢ (𝑊 ∈ ℂPreHil → , ∈ ((𝐽 ×_t 𝐽) Cn 𝐾))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3076 ∃wrex 3086 ⊆ wss 3899 class class class wbr 5103 × cxp 5653 ↾ cres 5657 ∘ ccom 5659 ⟶wf 6529 ‘cfv 6533 (class class class)co 7414 ℂcc 11123 1c1 11126 + caddc 11128 < clt 11268 − cmin 11466 / cdiv 11896 2c2 12320 ℝ⁺crp 13043 abscabs 15322 Basecbs 17302 Scalarcsca 17346 ·_𝑖cip 17348 distcds 17352 TopOpenctopn 17507 ∞Metcxmet 21571 MetOpencmopn 21576 ℂ_fldccnfld 21586 PreHilcphl 21838 ·_ifcipf 21839 Cn ccn 23450 ×_t ctx 23787 ∞MetSpcxms 24544 MetSpcms 24545 normcnm 24803 NrmGrpcngp 24804 ℂModcclm 25291 ℂPreHilccph 25395

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202 ax-pre-sup 11203 ax-addf 11204 ax-mulf 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8160 df-tpos 8225 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8456 df-2o 8457 df-er 8697 df-map 8829 df-ixp 8906 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-fsupp 9333 df-fi 9382 df-sup 9413 df-inf 9414 df-oi 9483 df-card 9945 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-div 11897 df-nn 12259 df-2 12328 df-3 12329 df-4 12330 df-5 12331 df-6 12332 df-7 12333 df-8 12334 df-9 12335 df-n0 12530 df-z 12617 df-dec 12738 df-uz 12889 df-q 12999 df-rp 13044 df-xneg 13164 df-xadd 13165 df-xmul 13166 df-ico 13405 df-icc 13406 df-fz 13563 df-fzo 13711 df-seq 14067 df-exp 14127 df-hash 14396 df-cj 15187 df-re 15188 df-im 15189 df-sqrt 15323 df-abs 15324 df-struct 17240 df-sets 17257 df-slot 17275 df-ndx 17287 df-base 17303 df-ress 17324 df-plusg 17356 df-mulr 17357 df-starv 17358 df-sca 17359 df-vsca 17360 df-ip 17361 df-tset 17362 df-ple 17363 df-ds 17365 df-unif 17366 df-hom 17367 df-cco 17368 df-rest 17508 df-topn 17509 df-0g 17527 df-gsum 17528 df-topgen 17529 df-pt 17530 df-prds 17533 df-xrs 17589 df-qtop 17594 df-imas 17595 df-xps 17597 df-mre 17671 df-mrc 17672 df-acs 17674 df-mgm 18731 df-sgrp 18822 df-mnd 18838 df-mhm 18892 df-submnd 18893 df-grp 19061 df-minusg 19062 df-sbg 19063 df-mulg 19192 df-subg 19247 df-ghm 19342 df-cntz 19445 df-cmn 19910 df-abl 19911 df-mgp 20275 df-rng 20289 df-ur 20322 df-ring 20375 df-cring 20376 df-oppr 20479 df-dvdsr 20499 df-unit 20500 df-invr 20530 df-dvr 20543 df-rhm 20614 df-subrng 20709 df-subrg 20733 df-drng 20893 df-staf 21006 df-srng 21007 df-lmod 21047 df-lmhm 21207 df-lvec 21288 df-sra 21358 df-rgmod 21359 df-psmet 21578 df-xmet 21579 df-met 21580 df-bl 21581 df-mopn 21582 df-cnfld 21587 df-phl 21840 df-ipf 21841 df-top 23120 df-topon 23137 df-topsp 23159 df-bases 23172 df-cn 23453 df-cnp 23454 df-tx 23789 df-hmeo 23982 df-xms 24547 df-ms 24548 df-tms 24549 df-nm 24809 df-ngp 24810 df-tng 24811 df-nlm 24813 df-clm 25292 df-cph 25397 df-tcph 25398

This theorem is used by: cnmpt1ip 25476 cnmpt2ip 25477

W3C validator