Theorem 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={\mathrm{Base}}_W$$
	ipcn.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	ipcn.d	$$⊢D=\mathrm{dist}\left(W\right)$$
	ipcn.n	$$⊢N=\mathrm{norm}\left(W\right)$$
	ipcn.t	$$⊢T=\frac{\frac{R}{2}}{N\left(A\right)+1}$$
	ipcn.u	$$⊢U=\frac{\frac{R}{2}}{N\left(B\right)+T}$$
	ipcn.w	$$⊢\phi \to W\in \mathrm{CPreHil}$$
	ipcn.a	$$⊢\phi \to A\in V$$
	ipcn.b	$$⊢\phi \to B\in V$$
	ipcn.r	$$⊢\phi \to R\in {ℝ}^{+}$$
	ipcn.x	$$⊢\phi \to X\in V$$
	ipcn.y	$$⊢\phi \to Y\in V$$
	ipcn.1	$$⊢\phi \to ADX<U$$
	ipcn.2	$$⊢\phi \to BDY<T$$
Assertion	ipcnlem2	$$⊢\phi \to \left|\left(A\underset{\dot{}}{,}B\right)-\left(X\underset{\dot{}}{,}Y\right)\right|<R$$

Proof

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