# Metamath Proof Explorer

## Theorem 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}={\mathrm{Base}}_{{W}}$
ipcn.h
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 {ℝ}^{+}$
Assertion ipcnlem1

### Proof

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