ipcn

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

	Ref	Expression
Hypotheses	ipcn.f	$⊢ \underset{˙}{,} = \cdot_{if} (W)$
	ipcn.j	$⊢ J = TopOpen (W)$
	ipcn.k	$⊢ K = TopOpen (ℂ_{fld})$
Assertion	ipcn	$⊢ W \in CPreHil \to \underset{˙}{,} \in ((J \times_{t} J) Cn K)$

Proof

Step	Hyp	Ref	Expression
1		ipcn.f	$⊢ \underset{˙}{,} = \cdot_{if} (W)$
2		ipcn.j	$⊢ J = TopOpen (W)$
3		ipcn.k	$⊢ K = TopOpen (ℂ_{fld})$
4		cphphl	$⊢ W \in CPreHil \to W \in PreHil$
5		eqid	$⊢ {Base}_{W} = {Base}_{W}$
6		eqid	$⊢ Scalar (W) = Scalar (W)$
7		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
8	5 1 6 7	phlipf	$⊢ W \in PreHil \to \underset{˙}{,} : {Base}_{W} \times {Base}_{W} ⟶ {Base}_{Scalar (W)}$
9	4 8	syl	$⊢ W \in CPreHil \to \underset{˙}{,} : {Base}_{W} \times {Base}_{W} ⟶ {Base}_{Scalar (W)}$
10		cphclm	$⊢ W \in CPreHil \to W \in CMod$
11	6 7	clmsscn	$⊢ W \in CMod \to {Base}_{Scalar (W)} \subseteq ℂ$
12	10 11	syl	$⊢ W \in CPreHil \to {Base}_{Scalar (W)} \subseteq ℂ$
13	9 12	fssd	$⊢ W \in CPreHil \to \underset{˙}{,} : {Base}_{W} \times {Base}_{W} ⟶ ℂ$
14		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
15		eqid	$⊢ dist (W) = dist (W)$
16		eqid	$⊢ norm (W) = norm (W)$
17		eqid	$⊢ \frac{\frac{r}{2}}{norm (W) (x) + 1} = \frac{\frac{r}{2}}{norm (W) (x) + 1}$
18		eqid	$⊢ \frac{\frac{r}{2}}{norm (W) (y) + (\frac{\frac{r}{2}}{norm (W) (x) + 1})} = \frac{\frac{r}{2}}{norm (W) (y) + (\frac{\frac{r}{2}}{norm (W) (x) + 1})}$
19		simpll	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land r \in ℝ^{+}) \to W \in CPreHil$
20		simplrl	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land r \in ℝ^{+}) \to x \in {Base}_{W}$
21		simplrr	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land r \in ℝ^{+}) \to y \in {Base}_{W}$
22		simpr	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land r \in ℝ^{+}) \to r \in ℝ^{+}$
23	5 14 15 16 17 18 19 20 21 22	ipcnlem1	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land r \in ℝ^{+}) \to \exists s \in ℝ^{+} \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x dist (W) z < s \land y dist (W) w < s) \to \|(x \cdot_{𝑖} (W) y) - (z \cdot_{𝑖} (W) w)\| < r)$
24	23	ralrimiva	$⊢ (W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \to \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x dist (W) z < s \land y dist (W) w < s) \to \|(x \cdot_{𝑖} (W) y) - (z \cdot_{𝑖} (W) w)\| < r)$
25		simplrl	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to x \in {Base}_{W}$
26		simprl	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to z \in {Base}_{W}$
27	25 26	ovresd	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z = x dist (W) z$
28	27	breq1d	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to (x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z < s \leftrightarrow x dist (W) z < s)$
29		simplrr	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to y \in {Base}_{W}$
30		simprr	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to w \in {Base}_{W}$
31	29 30	ovresd	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w = y dist (W) w$
32	31	breq1d	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to (y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s \leftrightarrow y dist (W) w < s)$
33	28 32	anbi12d	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to ((x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \leftrightarrow (x dist (W) z < s \land y dist (W) w < s))$
34	13	ad2antrr	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to \underset{˙}{,} : {Base}_{W} \times {Base}_{W} ⟶ ℂ$
35	34 25 29	fovrnd	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to x \underset{˙}{,} y \in ℂ$
36	34 26 30	fovrnd	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to z \underset{˙}{,} w \in ℂ$
37		eqid	$⊢ abs \circ - = abs \circ -$
38	37	cnmetdval	$⊢ (x \underset{˙}{,} y \in ℂ \land z \underset{˙}{,} w \in ℂ) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) = \|(x \underset{˙}{,} y) - (z \underset{˙}{,} w)\|$
39	35 36 38	syl2anc	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) = \|(x \underset{˙}{,} y) - (z \underset{˙}{,} w)\|$
40	5 14 1	ipfval	$⊢ (x \in {Base}_{W} \land y \in {Base}_{W}) \to x \underset{˙}{,} y = x \cdot_{𝑖} (W) y$
41	25 29 40	syl2anc	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to x \underset{˙}{,} y = x \cdot_{𝑖} (W) y$
42	5 14 1	ipfval	$⊢ (z \in {Base}_{W} \land w \in {Base}_{W}) \to z \underset{˙}{,} w = z \cdot_{𝑖} (W) w$
43	42	adantl	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to z \underset{˙}{,} w = z \cdot_{𝑖} (W) w$
44	41 43	oveq12d	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to (x \underset{˙}{,} y) - (z \underset{˙}{,} w) = (x \cdot_{𝑖} (W) y) - (z \cdot_{𝑖} (W) w)$
45	44	fveq2d	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to \|(x \underset{˙}{,} y) - (z \underset{˙}{,} w)\| = \|(x \cdot_{𝑖} (W) y) - (z \cdot_{𝑖} (W) w)\|$
46	39 45	eqtrd	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) = \|(x \cdot_{𝑖} (W) y) - (z \cdot_{𝑖} (W) w)\|$
47	46	breq1d	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to ((x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) < r \leftrightarrow \|(x \cdot_{𝑖} (W) y) - (z \cdot_{𝑖} (W) w)\| < r)$
48	33 47	imbi12d	$⊢ ((W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \land (z \in {Base}_{W} \land w \in {Base}_{W})) \to (((x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) < r) \leftrightarrow ((x dist (W) z < s \land y dist (W) w < s) \to \|(x \cdot_{𝑖} (W) y) - (z \cdot_{𝑖} (W) w)\| < r))$
49	48	2ralbidva	$⊢ (W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \to (\forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) < r) \leftrightarrow \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x dist (W) z < s \land y dist (W) w < s) \to \|(x \cdot_{𝑖} (W) y) - (z \cdot_{𝑖} (W) w)\| < r))$
50	49	rexbidv	$⊢ (W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \to (\exists s \in ℝ^{+} \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) < r) \leftrightarrow \exists s \in ℝ^{+} \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x dist (W) z < s \land y dist (W) w < s) \to \|(x \cdot_{𝑖} (W) y) - (z \cdot_{𝑖} (W) w)\| < r))$
51	50	ralbidv	$⊢ (W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \to (\forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) < r) \leftrightarrow \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x dist (W) z < s \land y dist (W) w < s) \to \|(x \cdot_{𝑖} (W) y) - (z \cdot_{𝑖} (W) w)\| < r))$
52	24 51	mpbird	$⊢ (W \in CPreHil \land (x \in {Base}_{W} \land y \in {Base}_{W})) \to \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) < r)$
53	52	ralrimivva	$⊢ W \in CPreHil \to \forall x \in {Base}_{W} \forall y \in {Base}_{W} \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) < r)$
54		cphngp	$⊢ W \in CPreHil \to W \in NrmGrp$
55		ngpms	$⊢ W \in NrmGrp \to W \in MetSp$
56	54 55	syl	$⊢ W \in CPreHil \to W \in MetSp$
57		msxms	$⊢ W \in MetSp \to W \in ∞MetSp$
58	56 57	syl	$⊢ W \in CPreHil \to W \in ∞MetSp$
59		eqid	$⊢ {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} = {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}$
60	5 59	xmsxmet	$⊢ W \in ∞MetSp \to {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} \in ∞Met ({Base}_{W})$
61	58 60	syl	$⊢ W \in CPreHil \to {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} \in ∞Met ({Base}_{W})$
62		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
63	62	a1i	$⊢ W \in CPreHil \to abs \circ - \in ∞Met (ℂ)$
64		eqid	$⊢ MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) = MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})$
65	3	cnfldtopn	$⊢ K = MetOpen (abs \circ -)$
66	64 64 65	txmetcn	$⊢ ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} \in ∞Met ({Base}_{W}) \land {dist (W) ↾}_{({Base}_{W} \times {Base}_{W})} \in ∞Met ({Base}_{W}) \land abs \circ - \in ∞Met (ℂ)) \to (\underset{˙}{,} \in ((MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) \times_{t} MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})) Cn K) \leftrightarrow (\underset{˙}{,} : {Base}_{W} \times {Base}_{W} ⟶ ℂ \land \forall x \in {Base}_{W} \forall y \in {Base}_{W} \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) < r)))$
67	61 61 63 66	syl3anc	$⊢ W \in CPreHil \to (\underset{˙}{,} \in ((MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) \times_{t} MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})) Cn K) \leftrightarrow (\underset{˙}{,} : {Base}_{W} \times {Base}_{W} ⟶ ℂ \land \forall x \in {Base}_{W} \forall y \in {Base}_{W} \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in {Base}_{W} \forall w \in {Base}_{W} ((x ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) z < s \land y ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) w < s) \to (x \underset{˙}{,} y) (abs \circ -) (z \underset{˙}{,} w) < r)))$
68	13 53 67	mpbir2and	$⊢ W \in CPreHil \to \underset{˙}{,} \in ((MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) \times_{t} MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})) Cn K)$
69	2 5 59	mstopn	$⊢ W \in MetSp \to J = MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})$
70	56 69	syl	$⊢ W \in CPreHil \to J = MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})$
71	70 70	oveq12d	$⊢ W \in CPreHil \to J \times_{t} J = MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) \times_{t} MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})$
72	71	oveq1d	$⊢ W \in CPreHil \to (J \times_{t} J) Cn K = (MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})}) \times_{t} MetOpen ({dist (W) ↾}_{({Base}_{W} \times {Base}_{W})})) Cn K$
73	68 72	eleqtrrd	$⊢ W \in CPreHil \to \underset{˙}{,} \in ((J \times_{t} J) Cn K)$

Metamath Proof Explorer

Theorem ipcn

Proof