Metamath Proof Explorer

Theorem lnopcon

Description: A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopcon ${⊢}{T}\in \mathrm{LinOp}\to \left({T}\in \mathrm{ContOp}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)$

Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({T}\in \mathrm{ContOp}↔if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{ContOp}\right)$
2 fveq1 ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\to {T}\left({y}\right)=if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)$
3 2 fveq2d ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\to {norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left(if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)$
4 3 breq1d ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({norm}_{ℎ}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)↔{norm}_{ℎ}\left(if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)$
5 4 rexralbidv ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)$
6 1 5 bibi12d ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\left({T}\in \mathrm{ContOp}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)↔\left(if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{ContOp}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)\right)$
7 idlnop ${⊢}{\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}$
8 7 elimel ${⊢}if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}$
9 8 lnopconi ${⊢}if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{ContOp}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(if\left({T}\in \mathrm{LinOp},{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)$
10 6 9 dedth ${⊢}{T}\in \mathrm{LinOp}\to \left({T}\in \mathrm{ContOp}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)\right)$