ipcnlem2

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 ℝ^{+}$
	ipcn.x	$⊢ φ \to X \in V$
	ipcn.y	$⊢ φ \to Y \in V$
	ipcn.1	$⊢ φ \to A D X < U$
	ipcn.2	$⊢ φ \to B D Y < T$
Assertion	ipcnlem2	$⊢ φ \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		ipcn.x	$⊢ φ \to X \in V$
12		ipcn.y	$⊢ φ \to Y \in V$
13		ipcn.1	$⊢ φ \to A D X < U$
14		ipcn.2	$⊢ φ \to B D Y < T$
15	1 2	cphipcl	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to A \underset{˙}{,} B \in ℂ$
16	7 8 9 15	syl3anc	$⊢ φ \to A \underset{˙}{,} B \in ℂ$
17	1 2	cphipcl	$⊢ (W \in CPreHil \land X \in V \land Y \in V) \to X \underset{˙}{,} Y \in ℂ$
18	7 11 12 17	syl3anc	$⊢ φ \to X \underset{˙}{,} Y \in ℂ$
19	1 2	cphipcl	$⊢ (W \in CPreHil \land A \in V \land Y \in V) \to A \underset{˙}{,} Y \in ℂ$
20	7 8 12 19	syl3anc	$⊢ φ \to A \underset{˙}{,} Y \in ℂ$
21	10	rpred	$⊢ φ \to R \in ℝ$
22	16 20	subcld	$⊢ φ \to (A \underset{˙}{,} B) - (A \underset{˙}{,} Y) \in ℂ$
23	22	abscld	$⊢ φ \to \|(A \underset{˙}{,} B) - (A \underset{˙}{,} Y)\| \in ℝ$
24		cphnlm	$⊢ W \in CPreHil \to W \in NrmMod$
25	7 24	syl	$⊢ φ \to W \in NrmMod$
26		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
27	25 26	syl	$⊢ φ \to W \in NrmGrp$
28	1 4	nmcl	$⊢ (W \in NrmGrp \land A \in V) \to N (A) \in ℝ$
29	27 8 28	syl2anc	$⊢ φ \to N (A) \in ℝ$
30	1 4	nmge0	$⊢ (W \in NrmGrp \land A \in V) \to 0 \leq N (A)$
31	27 8 30	syl2anc	$⊢ φ \to 0 \leq N (A)$
32	29 31	ge0p1rpd	$⊢ φ \to N (A) + 1 \in ℝ^{+}$
33	32	rpred	$⊢ φ \to N (A) + 1 \in ℝ$
34		ngpms	$⊢ W \in NrmGrp \to W \in MetSp$
35	27 34	syl	$⊢ φ \to W \in MetSp$
36	1 3	mscl	$⊢ (W \in MetSp \land B \in V \land Y \in V) \to B D Y \in ℝ$
37	35 9 12 36	syl3anc	$⊢ φ \to B D Y \in ℝ$
38	33 37	remulcld	$⊢ φ \to (N (A) + 1) (B D Y) \in ℝ$
39	21	rehalfcld	$⊢ φ \to \frac{R}{2} \in ℝ$
40	29 37	remulcld	$⊢ φ \to N (A) (B D Y) \in ℝ$
41		eqid	$⊢ -_{W} = -_{W}$
42	2 1 41	cphsubdi	$⊢ (W \in CPreHil \land (A \in V \land B \in V \land Y \in V)) \to A \underset{˙}{,} (B -_{W} Y) = (A \underset{˙}{,} B) - (A \underset{˙}{,} Y)$
43	7 8 9 12 42	syl13anc	$⊢ φ \to A \underset{˙}{,} (B -_{W} Y) = (A \underset{˙}{,} B) - (A \underset{˙}{,} Y)$
44	43	fveq2d	$⊢ φ \to \|A \underset{˙}{,} (B -_{W} Y)\| = \|(A \underset{˙}{,} B) - (A \underset{˙}{,} Y)\|$
45		ngpgrp	$⊢ W \in NrmGrp \to W \in Grp$
46	27 45	syl	$⊢ φ \to W \in Grp$
47	1 41	grpsubcl	$⊢ (W \in Grp \land B \in V \land Y \in V) \to B -_{W} Y \in V$
48	46 9 12 47	syl3anc	$⊢ φ \to B -_{W} Y \in V$
49	1 2 4	ipcau	$⊢ (W \in CPreHil \land A \in V \land B -_{W} Y \in V) \to \|A \underset{˙}{,} (B -_{W} Y)\| \leq N (A) N (B -_{W} Y)$
50	7 8 48 49	syl3anc	$⊢ φ \to \|A \underset{˙}{,} (B -_{W} Y)\| \leq N (A) N (B -_{W} Y)$
51	4 1 41 3	ngpds	$⊢ (W \in NrmGrp \land B \in V \land Y \in V) \to B D Y = N (B -_{W} Y)$
52	27 9 12 51	syl3anc	$⊢ φ \to B D Y = N (B -_{W} Y)$
53	52	oveq2d	$⊢ φ \to N (A) (B D Y) = N (A) N (B -_{W} Y)$
54	50 53	breqtrrd	$⊢ φ \to \|A \underset{˙}{,} (B -_{W} Y)\| \leq N (A) (B D Y)$
55	44 54	eqbrtrrd	$⊢ φ \to \|(A \underset{˙}{,} B) - (A \underset{˙}{,} Y)\| \leq N (A) (B D Y)$
56		msxms	$⊢ W \in MetSp \to W \in ∞MetSp$
57	35 56	syl	$⊢ φ \to W \in ∞MetSp$
58	1 3	xmsge0	$⊢ (W \in ∞MetSp \land B \in V \land Y \in V) \to 0 \leq B D Y$
59	57 9 12 58	syl3anc	$⊢ φ \to 0 \leq B D Y$
60	29	lep1d	$⊢ φ \to N (A) \leq N (A) + 1$
61	29 33 37 59 60	lemul1ad	$⊢ φ \to N (A) (B D Y) \leq (N (A) + 1) (B D Y)$
62	23 40 38 55 61	letrd	$⊢ φ \to \|(A \underset{˙}{,} B) - (A \underset{˙}{,} Y)\| \leq (N (A) + 1) (B D Y)$
63	14 5	breqtrdi	$⊢ φ \to B D Y < \frac{\frac{R}{2}}{N (A) + 1}$
64	37 39 32	ltmuldiv2d	$⊢ φ \to ((N (A) + 1) (B D Y) < \frac{R}{2} \leftrightarrow B D Y < \frac{\frac{R}{2}}{N (A) + 1})$
65	63 64	mpbird	$⊢ φ \to (N (A) + 1) (B D Y) < \frac{R}{2}$
66	23 38 39 62 65	lelttrd	$⊢ φ \to \|(A \underset{˙}{,} B) - (A \underset{˙}{,} Y)\| < \frac{R}{2}$
67	20 18	subcld	$⊢ φ \to (A \underset{˙}{,} Y) - (X \underset{˙}{,} Y) \in ℂ$
68	67	abscld	$⊢ φ \to \|(A \underset{˙}{,} Y) - (X \underset{˙}{,} Y)\| \in ℝ$
69	1 3	mscl	$⊢ (W \in MetSp \land A \in V \land X \in V) \to A D X \in ℝ$
70	35 8 11 69	syl3anc	$⊢ φ \to A D X \in ℝ$
71	1 4	nmcl	$⊢ (W \in NrmGrp \land B \in V) \to N (B) \in ℝ$
72	27 9 71	syl2anc	$⊢ φ \to N (B) \in ℝ$
73	10	rphalfcld	$⊢ φ \to \frac{R}{2} \in ℝ^{+}$
74	73 32	rpdivcld	$⊢ φ \to \frac{\frac{R}{2}}{N (A) + 1} \in ℝ^{+}$
75	5 74	eqeltrid	$⊢ φ \to T \in ℝ^{+}$
76	75	rpred	$⊢ φ \to T \in ℝ$
77	72 76	readdcld	$⊢ φ \to N (B) + T \in ℝ$
78	70 77	remulcld	$⊢ φ \to (A D X) (N (B) + T) \in ℝ$
79	1 4	nmcl	$⊢ (W \in NrmGrp \land Y \in V) \to N (Y) \in ℝ$
80	27 12 79	syl2anc	$⊢ φ \to N (Y) \in ℝ$
81	70 80	remulcld	$⊢ φ \to (A D X) N (Y) \in ℝ$
82	2 1 41	cphsubdir	$⊢ (W \in CPreHil \land (A \in V \land X \in V \land Y \in V)) \to (A -_{W} X) \underset{˙}{,} Y = (A \underset{˙}{,} Y) - (X \underset{˙}{,} Y)$
83	7 8 11 12 82	syl13anc	$⊢ φ \to (A -_{W} X) \underset{˙}{,} Y = (A \underset{˙}{,} Y) - (X \underset{˙}{,} Y)$
84	83	fveq2d	$⊢ φ \to \|(A -_{W} X) \underset{˙}{,} Y\| = \|(A \underset{˙}{,} Y) - (X \underset{˙}{,} Y)\|$
85	1 41	grpsubcl	$⊢ (W \in Grp \land A \in V \land X \in V) \to A -_{W} X \in V$
86	46 8 11 85	syl3anc	$⊢ φ \to A -_{W} X \in V$
87	1 2 4	ipcau	$⊢ (W \in CPreHil \land A -_{W} X \in V \land Y \in V) \to \|(A -_{W} X) \underset{˙}{,} Y\| \leq N (A -_{W} X) N (Y)$
88	7 86 12 87	syl3anc	$⊢ φ \to \|(A -_{W} X) \underset{˙}{,} Y\| \leq N (A -_{W} X) N (Y)$
89	4 1 41 3	ngpds	$⊢ (W \in NrmGrp \land A \in V \land X \in V) \to A D X = N (A -_{W} X)$
90	27 8 11 89	syl3anc	$⊢ φ \to A D X = N (A -_{W} X)$
91	90	oveq1d	$⊢ φ \to (A D X) N (Y) = N (A -_{W} X) N (Y)$
92	88 91	breqtrrd	$⊢ φ \to \|(A -_{W} X) \underset{˙}{,} Y\| \leq (A D X) N (Y)$
93	84 92	eqbrtrrd	$⊢ φ \to \|(A \underset{˙}{,} Y) - (X \underset{˙}{,} Y)\| \leq (A D X) N (Y)$
94	1 3	xmsge0	$⊢ (W \in ∞MetSp \land A \in V \land X \in V) \to 0 \leq A D X$
95	57 8 11 94	syl3anc	$⊢ φ \to 0 \leq A D X$
96	80 72	resubcld	$⊢ φ \to N (Y) - N (B) \in ℝ$
97	1 4 41	nm2dif	$⊢ (W \in NrmGrp \land Y \in V \land B \in V) \to N (Y) - N (B) \leq N (Y -_{W} B)$
98	27 12 9 97	syl3anc	$⊢ φ \to N (Y) - N (B) \leq N (Y -_{W} B)$
99	4 1 41 3	ngpdsr	$⊢ (W \in NrmGrp \land B \in V \land Y \in V) \to B D Y = N (Y -_{W} B)$
100	27 9 12 99	syl3anc	$⊢ φ \to B D Y = N (Y -_{W} B)$
101	98 100	breqtrrd	$⊢ φ \to N (Y) - N (B) \leq B D Y$
102	37 76 14	ltled	$⊢ φ \to B D Y \leq T$
103	96 37 76 101 102	letrd	$⊢ φ \to N (Y) - N (B) \leq T$
104	80 72 76	lesubadd2d	$⊢ φ \to (N (Y) - N (B) \leq T \leftrightarrow N (Y) \leq N (B) + T)$
105	103 104	mpbid	$⊢ φ \to N (Y) \leq N (B) + T$
106	80 77 70 95 105	lemul2ad	$⊢ φ \to (A D X) N (Y) \leq (A D X) (N (B) + T)$
107	68 81 78 93 106	letrd	$⊢ φ \to \|(A \underset{˙}{,} Y) - (X \underset{˙}{,} Y)\| \leq (A D X) (N (B) + T)$
108	13 6	breqtrdi	$⊢ φ \to A D X < \frac{\frac{R}{2}}{N (B) + T}$
109		0red	$⊢ φ \to 0 \in ℝ$
110	1 4	nmge0	$⊢ (W \in NrmGrp \land B \in V) \to 0 \leq N (B)$
111	27 9 110	syl2anc	$⊢ φ \to 0 \leq N (B)$
112	72 75	ltaddrpd	$⊢ φ \to N (B) < N (B) + T$
113	109 72 77 111 112	lelttrd	$⊢ φ \to 0 < N (B) + T$
114		ltmuldiv	$⊢ (A D X \in ℝ \land \frac{R}{2} \in ℝ \land (N (B) + T \in ℝ \land 0 < N (B) + T)) \to ((A D X) (N (B) + T) < \frac{R}{2} \leftrightarrow A D X < \frac{\frac{R}{2}}{N (B) + T})$
115	70 39 77 113 114	syl112anc	$⊢ φ \to ((A D X) (N (B) + T) < \frac{R}{2} \leftrightarrow A D X < \frac{\frac{R}{2}}{N (B) + T})$
116	108 115	mpbird	$⊢ φ \to (A D X) (N (B) + T) < \frac{R}{2}$
117	68 78 39 107 116	lelttrd	$⊢ φ \to \|(A \underset{˙}{,} Y) - (X \underset{˙}{,} Y)\| < \frac{R}{2}$
118	16 18 20 21 66 117	abs3lemd	$⊢ φ \to \|(A \underset{˙}{,} B) - (X \underset{˙}{,} Y)\| < R$

Metamath Proof Explorer

Theorem ipcnlem2

Proof