# Metamath Proof Explorer

Description: Lemma for cnlnadji . G is a continuous linear functional. (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 ${⊢}{T}\in \mathrm{LinOp}$
cnlnadjlem.2 ${⊢}{T}\in \mathrm{ContOp}$
cnlnadjlem.3 ${⊢}{G}=\left({g}\in ℋ⟼{T}\left({g}\right){\cdot }_{\mathrm{ih}}{y}\right)$
Assertion cnlnadjlem2 ${⊢}{y}\in ℋ\to \left({G}\in \mathrm{LinFn}\wedge {G}\in \mathrm{ContFn}\right)$

### Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 ${⊢}{T}\in \mathrm{LinOp}$
2 cnlnadjlem.2 ${⊢}{T}\in \mathrm{ContOp}$
3 cnlnadjlem.3 ${⊢}{G}=\left({g}\in ℋ⟼{T}\left({g}\right){\cdot }_{\mathrm{ih}}{y}\right)$
4 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
5 4 ffvelrni ${⊢}{g}\in ℋ\to {T}\left({g}\right)\in ℋ$
6 hicl ${⊢}\left({T}\left({g}\right)\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({g}\right){\cdot }_{\mathrm{ih}}{y}\in ℂ$
7 5 6 sylan ${⊢}\left({g}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({g}\right){\cdot }_{\mathrm{ih}}{y}\in ℂ$
8 7 ancoms ${⊢}\left({y}\in ℋ\wedge {g}\in ℋ\right)\to {T}\left({g}\right){\cdot }_{\mathrm{ih}}{y}\in ℂ$
9 8 3 fmptd ${⊢}{y}\in ℋ\to {G}:ℋ⟶ℂ$
10 hvmulcl ${⊢}\left({x}\in ℂ\wedge {w}\in ℋ\right)\to {x}{\cdot }_{ℎ}{w}\in ℋ$
11 1 lnopaddi ${⊢}\left({x}{\cdot }_{ℎ}{w}\in ℋ\wedge {z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right)={T}\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{T}\left({z}\right)$
12 11 3adant3 ${⊢}\left({x}{\cdot }_{ℎ}{w}\in ℋ\wedge {z}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right)={T}\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{T}\left({z}\right)$
13 12 oveq1d ${⊢}\left({x}{\cdot }_{ℎ}{w}\in ℋ\wedge {z}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{y}$
14 4 ffvelrni ${⊢}{x}{\cdot }_{ℎ}{w}\in ℋ\to {T}\left({x}{\cdot }_{ℎ}{w}\right)\in ℋ$
15 4 ffvelrni ${⊢}{z}\in ℋ\to {T}\left({z}\right)\in ℋ$
16 id ${⊢}{y}\in ℋ\to {y}\in ℋ$
17 ax-his2 ${⊢}\left({T}\left({x}{\cdot }_{ℎ}{w}\right)\in ℋ\wedge {T}\left({z}\right)\in ℋ\wedge {y}\in ℋ\right)\to \left({T}\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}{\cdot }_{ℎ}{w}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\right)$
18 14 15 16 17 syl3an ${⊢}\left({x}{\cdot }_{ℎ}{w}\in ℋ\wedge {z}\in ℋ\wedge {y}\in ℋ\right)\to \left({T}\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{T}\left({z}\right)\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}{\cdot }_{ℎ}{w}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\right)$
19 13 18 eqtrd ${⊢}\left({x}{\cdot }_{ℎ}{w}\in ℋ\wedge {z}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}{\cdot }_{ℎ}{w}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\right)$
20 19 3comr ${⊢}\left({y}\in ℋ\wedge {x}{\cdot }_{ℎ}{w}\in ℋ\wedge {z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}{\cdot }_{ℎ}{w}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\right)$
21 20 3expa ${⊢}\left(\left({y}\in ℋ\wedge {x}{\cdot }_{ℎ}{w}\in ℋ\right)\wedge {z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}{\cdot }_{ℎ}{w}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\right)$
22 10 21 sylanl2 ${⊢}\left(\left({y}\in ℋ\wedge \left({x}\in ℂ\wedge {w}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to {T}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}{\cdot }_{ℎ}{w}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\right)$
23 hvaddcl ${⊢}\left({x}{\cdot }_{ℎ}{w}\in ℋ\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\in ℋ$
24 10 23 sylan ${⊢}\left(\left({x}\in ℂ\wedge {w}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\in ℋ$
25 1 2 3 cnlnadjlem1 ${⊢}\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\in ℋ\to {G}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right)={T}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{y}$
26 24 25 syl ${⊢}\left(\left({x}\in ℂ\wedge {w}\in ℋ\right)\wedge {z}\in ℋ\right)\to {G}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right)={T}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{y}$
27 26 adantll ${⊢}\left(\left({y}\in ℋ\wedge \left({x}\in ℂ\wedge {w}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to {G}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right)={T}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right){\cdot }_{\mathrm{ih}}{y}$
28 4 ffvelrni ${⊢}{w}\in ℋ\to {T}\left({w}\right)\in ℋ$
29 ax-his3 ${⊢}\left({x}\in ℂ\wedge {T}\left({w}\right)\in ℋ\wedge {y}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{T}\left({w}\right)\right){\cdot }_{\mathrm{ih}}{y}={x}\left({T}\left({w}\right){\cdot }_{\mathrm{ih}}{y}\right)$
30 28 29 syl3an2 ${⊢}\left({x}\in ℂ\wedge {w}\in ℋ\wedge {y}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{T}\left({w}\right)\right){\cdot }_{\mathrm{ih}}{y}={x}\left({T}\left({w}\right){\cdot }_{\mathrm{ih}}{y}\right)$
31 30 3comr ${⊢}\left({y}\in ℋ\wedge {x}\in ℂ\wedge {w}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{T}\left({w}\right)\right){\cdot }_{\mathrm{ih}}{y}={x}\left({T}\left({w}\right){\cdot }_{\mathrm{ih}}{y}\right)$
32 31 3expb ${⊢}\left({y}\in ℋ\wedge \left({x}\in ℂ\wedge {w}\in ℋ\right)\right)\to \left({x}{\cdot }_{ℎ}{T}\left({w}\right)\right){\cdot }_{\mathrm{ih}}{y}={x}\left({T}\left({w}\right){\cdot }_{\mathrm{ih}}{y}\right)$
33 1 lnopmuli ${⊢}\left({x}\in ℂ\wedge {w}\in ℋ\right)\to {T}\left({x}{\cdot }_{ℎ}{w}\right)={x}{\cdot }_{ℎ}{T}\left({w}\right)$
34 33 oveq1d ${⊢}\left({x}\in ℂ\wedge {w}\in ℋ\right)\to {T}\left({x}{\cdot }_{ℎ}{w}\right){\cdot }_{\mathrm{ih}}{y}=\left({x}{\cdot }_{ℎ}{T}\left({w}\right)\right){\cdot }_{\mathrm{ih}}{y}$
35 34 adantl ${⊢}\left({y}\in ℋ\wedge \left({x}\in ℂ\wedge {w}\in ℋ\right)\right)\to {T}\left({x}{\cdot }_{ℎ}{w}\right){\cdot }_{\mathrm{ih}}{y}=\left({x}{\cdot }_{ℎ}{T}\left({w}\right)\right){\cdot }_{\mathrm{ih}}{y}$
36 1 2 3 cnlnadjlem1 ${⊢}{w}\in ℋ\to {G}\left({w}\right)={T}\left({w}\right){\cdot }_{\mathrm{ih}}{y}$
37 36 oveq2d ${⊢}{w}\in ℋ\to {x}{G}\left({w}\right)={x}\left({T}\left({w}\right){\cdot }_{\mathrm{ih}}{y}\right)$
38 37 ad2antll ${⊢}\left({y}\in ℋ\wedge \left({x}\in ℂ\wedge {w}\in ℋ\right)\right)\to {x}{G}\left({w}\right)={x}\left({T}\left({w}\right){\cdot }_{\mathrm{ih}}{y}\right)$
39 32 35 38 3eqtr4rd ${⊢}\left({y}\in ℋ\wedge \left({x}\in ℂ\wedge {w}\in ℋ\right)\right)\to {x}{G}\left({w}\right)={T}\left({x}{\cdot }_{ℎ}{w}\right){\cdot }_{\mathrm{ih}}{y}$
40 1 2 3 cnlnadjlem1 ${⊢}{z}\in ℋ\to {G}\left({z}\right)={T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}$
41 39 40 oveqan12d ${⊢}\left(\left({y}\in ℋ\wedge \left({x}\in ℂ\wedge {w}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to {x}{G}\left({w}\right)+{G}\left({z}\right)=\left({T}\left({x}{\cdot }_{ℎ}{w}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\right)$
42 22 27 41 3eqtr4d ${⊢}\left(\left({y}\in ℋ\wedge \left({x}\in ℂ\wedge {w}\in ℋ\right)\right)\wedge {z}\in ℋ\right)\to {G}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right)={x}{G}\left({w}\right)+{G}\left({z}\right)$
43 42 ralrimiva ${⊢}\left({y}\in ℋ\wedge \left({x}\in ℂ\wedge {w}\in ℋ\right)\right)\to \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right)={x}{G}\left({w}\right)+{G}\left({z}\right)$
44 43 ralrimivva ${⊢}{y}\in ℋ\to \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right)={x}{G}\left({w}\right)+{G}\left({z}\right)$
45 ellnfn ${⊢}{G}\in \mathrm{LinFn}↔\left({G}:ℋ⟶ℂ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left(\left({x}{\cdot }_{ℎ}{w}\right){+}_{ℎ}{z}\right)={x}{G}\left({w}\right)+{G}\left({z}\right)\right)$
46 9 44 45 sylanbrc ${⊢}{y}\in ℋ\to {G}\in \mathrm{LinFn}$
47 1 2 nmcopexi ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
48 normcl ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left({y}\right)\in ℝ$
49 remulcl ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ\wedge {norm}_{ℎ}\left({y}\right)\in ℝ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right)\in ℝ$
50 47 48 49 sylancr ${⊢}{y}\in ℋ\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right)\in ℝ$
51 40 adantr ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to {G}\left({z}\right)={T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}$
52 hicl ${⊢}\left({T}\left({z}\right)\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\in ℂ$
53 15 52 sylan ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\in ℂ$
54 51 53 eqeltrd ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to {G}\left({z}\right)\in ℂ$
55 54 abscld ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to \left|{G}\left({z}\right)\right|\in ℝ$
56 normcl ${⊢}{T}\left({z}\right)\in ℋ\to {norm}_{ℎ}\left({T}\left({z}\right)\right)\in ℝ$
57 15 56 syl ${⊢}{z}\in ℋ\to {norm}_{ℎ}\left({T}\left({z}\right)\right)\in ℝ$
58 remulcl ${⊢}\left({norm}_{ℎ}\left({T}\left({z}\right)\right)\in ℝ\wedge {norm}_{ℎ}\left({y}\right)\in ℝ\right)\to {norm}_{ℎ}\left({T}\left({z}\right)\right){norm}_{ℎ}\left({y}\right)\in ℝ$
59 57 48 58 syl2an ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({z}\right)\right){norm}_{ℎ}\left({y}\right)\in ℝ$
60 normcl ${⊢}{z}\in ℋ\to {norm}_{ℎ}\left({z}\right)\in ℝ$
61 remulcl ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ\wedge {norm}_{ℎ}\left({z}\right)\in ℝ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)\in ℝ$
62 47 60 61 sylancr ${⊢}{z}\in ℋ\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)\in ℝ$
63 remulcl ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)\in ℝ\wedge {norm}_{ℎ}\left({y}\right)\in ℝ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right){norm}_{ℎ}\left({y}\right)\in ℝ$
64 62 48 63 syl2an ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right){norm}_{ℎ}\left({y}\right)\in ℝ$
65 51 fveq2d ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to \left|{G}\left({z}\right)\right|=\left|{T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\right|$
66 bcs ${⊢}\left({T}\left({z}\right)\in ℋ\wedge {y}\in ℋ\right)\to \left|{T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\right|\le {norm}_{ℎ}\left({T}\left({z}\right)\right){norm}_{ℎ}\left({y}\right)$
67 15 66 sylan ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to \left|{T}\left({z}\right){\cdot }_{\mathrm{ih}}{y}\right|\le {norm}_{ℎ}\left({T}\left({z}\right)\right){norm}_{ℎ}\left({y}\right)$
68 65 67 eqbrtrd ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to \left|{G}\left({z}\right)\right|\le {norm}_{ℎ}\left({T}\left({z}\right)\right){norm}_{ℎ}\left({y}\right)$
69 57 adantr ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({z}\right)\right)\in ℝ$
70 62 adantr ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)\in ℝ$
71 normge0 ${⊢}{y}\in ℋ\to 0\le {norm}_{ℎ}\left({y}\right)$
72 48 71 jca ${⊢}{y}\in ℋ\to \left({norm}_{ℎ}\left({y}\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({y}\right)\right)$
73 72 adantl ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to \left({norm}_{ℎ}\left({y}\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({y}\right)\right)$
74 1 2 nmcoplbi ${⊢}{z}\in ℋ\to {norm}_{ℎ}\left({T}\left({z}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)$
75 74 adantr ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({z}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)$
76 lemul1a ${⊢}\left(\left({norm}_{ℎ}\left({T}\left({z}\right)\right)\in ℝ\wedge {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)\in ℝ\wedge \left({norm}_{ℎ}\left({y}\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left({y}\right)\right)\right)\wedge {norm}_{ℎ}\left({T}\left({z}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)\right)\to {norm}_{ℎ}\left({T}\left({z}\right)\right){norm}_{ℎ}\left({y}\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right){norm}_{ℎ}\left({y}\right)$
77 69 70 73 75 76 syl31anc ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({z}\right)\right){norm}_{ℎ}\left({y}\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right){norm}_{ℎ}\left({y}\right)$
78 55 59 64 68 77 letrd ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to \left|{G}\left({z}\right)\right|\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right){norm}_{ℎ}\left({y}\right)$
79 60 recnd ${⊢}{z}\in ℋ\to {norm}_{ℎ}\left({z}\right)\in ℂ$
80 48 recnd ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left({y}\right)\in ℂ$
81 47 recni ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℂ$
82 mul32 ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in ℂ\wedge {norm}_{ℎ}\left({z}\right)\in ℂ\wedge {norm}_{ℎ}\left({y}\right)\in ℂ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right){norm}_{ℎ}\left({y}\right)={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right){norm}_{ℎ}\left({z}\right)$
83 81 82 mp3an1 ${⊢}\left({norm}_{ℎ}\left({z}\right)\in ℂ\wedge {norm}_{ℎ}\left({y}\right)\in ℂ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right){norm}_{ℎ}\left({y}\right)={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right){norm}_{ℎ}\left({z}\right)$
84 79 80 83 syl2an ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right){norm}_{ℎ}\left({y}\right)={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right){norm}_{ℎ}\left({z}\right)$
85 78 84 breqtrd ${⊢}\left({z}\in ℋ\wedge {y}\in ℋ\right)\to \left|{G}\left({z}\right)\right|\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right){norm}_{ℎ}\left({z}\right)$
86 85 ancoms ${⊢}\left({y}\in ℋ\wedge {z}\in ℋ\right)\to \left|{G}\left({z}\right)\right|\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right){norm}_{ℎ}\left({z}\right)$
87 86 ralrimiva ${⊢}{y}\in ℋ\to \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left|{G}\left({z}\right)\right|\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right){norm}_{ℎ}\left({z}\right)$
88 oveq1 ${⊢}{x}={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right)\to {x}{norm}_{ℎ}\left({z}\right)={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right){norm}_{ℎ}\left({z}\right)$
89 88 breq2d ${⊢}{x}={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right)\to \left(\left|{G}\left({z}\right)\right|\le {x}{norm}_{ℎ}\left({z}\right)↔\left|{G}\left({z}\right)\right|\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right){norm}_{ℎ}\left({z}\right)\right)$
90 89 ralbidv ${⊢}{x}={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right)\to \left(\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left|{G}\left({z}\right)\right|\le {x}{norm}_{ℎ}\left({z}\right)↔\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left|{G}\left({z}\right)\right|\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right){norm}_{ℎ}\left({z}\right)\right)$
91 90 rspcev ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right)\in ℝ\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left|{G}\left({z}\right)\right|\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right){norm}_{ℎ}\left({z}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left|{G}\left({z}\right)\right|\le {x}{norm}_{ℎ}\left({z}\right)$
92 50 87 91 syl2anc ${⊢}{y}\in ℋ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left|{G}\left({z}\right)\right|\le {x}{norm}_{ℎ}\left({z}\right)$
93 lnfncon ${⊢}{G}\in \mathrm{LinFn}\to \left({G}\in \mathrm{ContFn}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left|{G}\left({z}\right)\right|\le {x}{norm}_{ℎ}\left({z}\right)\right)$
94 46 93 syl ${⊢}{y}\in ℋ\to \left({G}\in \mathrm{ContFn}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left|{G}\left({z}\right)\right|\le {x}{norm}_{ℎ}\left({z}\right)\right)$
95 92 94 mpbird ${⊢}{y}\in ℋ\to {G}\in \mathrm{ContFn}$
96 46 95 jca ${⊢}{y}\in ℋ\to \left({G}\in \mathrm{LinFn}\wedge {G}\in \mathrm{ContFn}\right)$