ipcnlem1

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

	Ref	Expression
Hypotheses	ipcn.v	$⊢ V = {Base}_{W}$
	ipcn.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	ipcn.d	$⊢ D = dist (W)$
	ipcn.n	$⊢ N = norm (W)$
	ipcn.t	$⊢ T = \frac{\frac{R}{2}}{N (A) + 1}$
	ipcn.u	$⊢ U = \frac{\frac{R}{2}}{N (B) + T}$
	ipcn.w	$⊢ φ \to W \in CPreHil$
	ipcn.a	$⊢ φ \to A \in V$
	ipcn.b	$⊢ φ \to B \in V$
	ipcn.r	$⊢ φ \to R \in ℝ^{+}$
Assertion	ipcnlem1	$⊢ φ \to \exists r \in ℝ^{+} \forall x \in V \forall y \in V ((A D x < r \land B D y < r) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R)$

Proof

Step	Hyp	Ref	Expression
1		ipcn.v	$⊢ V = {Base}_{W}$
2		ipcn.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		ipcn.d	$⊢ D = dist (W)$
4		ipcn.n	$⊢ N = norm (W)$
5		ipcn.t	$⊢ T = \frac{\frac{R}{2}}{N (A) + 1}$
6		ipcn.u	$⊢ U = \frac{\frac{R}{2}}{N (B) + T}$
7		ipcn.w	$⊢ φ \to W \in CPreHil$
8		ipcn.a	$⊢ φ \to A \in V$
9		ipcn.b	$⊢ φ \to B \in V$
10		ipcn.r	$⊢ φ \to R \in ℝ^{+}$
11	10	rphalfcld	$⊢ φ \to \frac{R}{2} \in ℝ^{+}$
12		cphnlm	$⊢ W \in CPreHil \to W \in NrmMod$
13	7 12	syl	$⊢ φ \to W \in NrmMod$
14		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
15	13 14	syl	$⊢ φ \to W \in NrmGrp$
16	1 4	nmcl	$⊢ (W \in NrmGrp \land A \in V) \to N (A) \in ℝ$
17	15 8 16	syl2anc	$⊢ φ \to N (A) \in ℝ$
18	1 4	nmge0	$⊢ (W \in NrmGrp \land A \in V) \to 0 \leq N (A)$
19	15 8 18	syl2anc	$⊢ φ \to 0 \leq N (A)$
20	17 19	ge0p1rpd	$⊢ φ \to N (A) + 1 \in ℝ^{+}$
21	11 20	rpdivcld	$⊢ φ \to \frac{\frac{R}{2}}{N (A) + 1} \in ℝ^{+}$
22	5 21	eqeltrid	$⊢ φ \to T \in ℝ^{+}$
23	1 4	nmcl	$⊢ (W \in NrmGrp \land B \in V) \to N (B) \in ℝ$
24	15 9 23	syl2anc	$⊢ φ \to N (B) \in ℝ$
25	22	rpred	$⊢ φ \to T \in ℝ$
26	24 25	readdcld	$⊢ φ \to N (B) + T \in ℝ$
27		0red	$⊢ φ \to 0 \in ℝ$
28	1 4	nmge0	$⊢ (W \in NrmGrp \land B \in V) \to 0 \leq N (B)$
29	15 9 28	syl2anc	$⊢ φ \to 0 \leq N (B)$
30	24 22	ltaddrpd	$⊢ φ \to N (B) < N (B) + T$
31	27 24 26 29 30	lelttrd	$⊢ φ \to 0 < N (B) + T$
32	26 31	elrpd	$⊢ φ \to N (B) + T \in ℝ^{+}$
33	11 32	rpdivcld	$⊢ φ \to \frac{\frac{R}{2}}{N (B) + T} \in ℝ^{+}$
34	6 33	eqeltrid	$⊢ φ \to U \in ℝ^{+}$
35	22 34	ifcld	$⊢ φ \to if (T \leq U, T, U) \in ℝ^{+}$
36	7	adantr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to W \in CPreHil$
37	8	adantr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to A \in V$
38	9	adantr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to B \in V$
39	10	adantr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to R \in ℝ^{+}$
40		simprll	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to x \in V$
41		simprlr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to y \in V$
42	15	adantr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to W \in NrmGrp$
43		ngpms	$⊢ W \in NrmGrp \to W \in MetSp$
44	42 43	syl	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to W \in MetSp$
45	1 3	mscl	$⊢ (W \in MetSp \land A \in V \land x \in V) \to A D x \in ℝ$
46	44 37 40 45	syl3anc	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to A D x \in ℝ$
47	35	adantr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to if (T \leq U, T, U) \in ℝ^{+}$
48	47	rpred	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to if (T \leq U, T, U) \in ℝ$
49	34	rpred	$⊢ φ \to U \in ℝ$
50	49	adantr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to U \in ℝ$
51		simprrl	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to A D x < if (T \leq U, T, U)$
52	25	adantr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to T \in ℝ$
53		min2	$⊢ (T \in ℝ \land U \in ℝ) \to if (T \leq U, T, U) \leq U$
54	52 50 53	syl2anc	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to if (T \leq U, T, U) \leq U$
55	46 48 50 51 54	ltletrd	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to A D x < U$
56	15 43	syl	$⊢ φ \to W \in MetSp$
57	56	adantr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to W \in MetSp$
58	1 3	mscl	$⊢ (W \in MetSp \land B \in V \land y \in V) \to B D y \in ℝ$
59	57 38 41 58	syl3anc	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to B D y \in ℝ$
60		simprrr	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to B D y < if (T \leq U, T, U)$
61		min1	$⊢ (T \in ℝ \land U \in ℝ) \to if (T \leq U, T, U) \leq T$
62	52 50 61	syl2anc	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to if (T \leq U, T, U) \leq T$
63	59 48 52 60 62	ltletrd	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to B D y < T$
64	1 2 3 4 5 6 36 37 38 39 40 41 55 63	ipcnlem2	$⊢ (φ \land ((x \in V \land y \in V) \land (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R$
65	64	expr	$⊢ (φ \land (x \in V \land y \in V)) \to ((A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R)$
66	65	ralrimivva	$⊢ φ \to \forall x \in V \forall y \in V ((A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R)$
67		breq2	$⊢ r = if (T \leq U, T, U) \to (A D x < r \leftrightarrow A D x < if (T \leq U, T, U))$
68		breq2	$⊢ r = if (T \leq U, T, U) \to (B D y < r \leftrightarrow B D y < if (T \leq U, T, U))$
69	67 68	anbi12d	$⊢ r = if (T \leq U, T, U) \to ((A D x < r \land B D y < r) \leftrightarrow (A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)))$
70	69	imbi1d	$⊢ r = if (T \leq U, T, U) \to (((A D x < r \land B D y < r) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R) \leftrightarrow ((A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R))$
71	70	2ralbidv	$⊢ r = if (T \leq U, T, U) \to (\forall x \in V \forall y \in V ((A D x < r \land B D y < r) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R) \leftrightarrow \forall x \in V \forall y \in V ((A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R))$
72	71	rspcev	$⊢ (if (T \leq U, T, U) \in ℝ^{+} \land \forall x \in V \forall y \in V ((A D x < if (T \leq U, T, U) \land B D y < if (T \leq U, T, U)) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R)) \to \exists r \in ℝ^{+} \forall x \in V \forall y \in V ((A D x < r \land B D y < r) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R)$
73	35 66 72	syl2anc	$⊢ φ \to \exists r \in ℝ^{+} \forall x \in V \forall y \in V ((A D x < r \land B D y < r) \to \|(A \underset{˙}{,} B) - (x \underset{˙}{,} y)\| < R)$

Metamath Proof Explorer

Theorem ipcnlem1

Proof