Metamath Proof Explorer

Description: Lemma for cnlnadji . F is continuous. (Contributed by NM, 17-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)$
cnlnadjlem.4 ${⊢}{B}=\left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
cnlnadjlem.5 ${⊢}{F}=\left({y}\in ℋ⟼{B}\right)$
Assertion cnlnadjlem8 ${⊢}{F}\in \mathrm{ContOp}$

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 cnlnadjlem.4 ${⊢}{B}=\left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
5 cnlnadjlem.5 ${⊢}{F}=\left({y}\in ℋ⟼{B}\right)$
6 1 2 nmcopexi ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
7 1 2 3 4 5 cnlnadjlem7 ${⊢}{z}\in ℋ\to {norm}_{ℎ}\left({F}\left({z}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)$
8 7 rgen ${⊢}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({F}\left({z}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)$
9 oveq1 ${⊢}{x}={norm}_{\mathrm{op}}\left({T}\right)\to {x}{norm}_{ℎ}\left({z}\right)={norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)$
10 9 breq2d ${⊢}{x}={norm}_{\mathrm{op}}\left({T}\right)\to \left({norm}_{ℎ}\left({F}\left({z}\right)\right)\le {x}{norm}_{ℎ}\left({z}\right)↔{norm}_{ℎ}\left({F}\left({z}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)\right)$
11 10 ralbidv ${⊢}{x}={norm}_{\mathrm{op}}\left({T}\right)\to \left(\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({F}\left({z}\right)\right)\le {x}{norm}_{ℎ}\left({z}\right)↔\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({F}\left({z}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)\right)$
12 11 rspcev ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({F}\left({z}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({z}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({F}\left({z}\right)\right)\le {x}{norm}_{ℎ}\left({z}\right)$
13 6 8 12 mp2an ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({F}\left({z}\right)\right)\le {x}{norm}_{ℎ}\left({z}\right)$
14 1 2 3 4 5 cnlnadjlem6 ${⊢}{F}\in \mathrm{LinOp}$
15 14 lnopconi ${⊢}{F}\in \mathrm{ContOp}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({F}\left({z}\right)\right)\le {x}{norm}_{ℎ}\left({z}\right)$
16 13 15 mpbir ${⊢}{F}\in \mathrm{ContOp}$