# Metamath Proof Explorer

Description: Property of the norm of an adjoint. Part of proof of Theorem 3.10 of Beran p. 104. (Contributed by NM, 22-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopadjle.1 ${⊢}{T}\in \mathrm{BndLinOp}$
Assertion nmopadjlei ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({adj}_{h}\left({T}\right)\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 nmopadjle.1 ${⊢}{T}\in \mathrm{BndLinOp}$
2 bdopssadj ${⊢}\mathrm{BndLinOp}\subseteq \mathrm{dom}{adj}_{h}$
3 2 1 sselii ${⊢}{T}\in \mathrm{dom}{adj}_{h}$
4 adjvalval ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\right)\to {adj}_{h}\left({T}\right)\left({A}\right)=\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{A}={v}{\cdot }_{\mathrm{ih}}{f}\right)$
5 3 4 mpan ${⊢}{A}\in ℋ\to {adj}_{h}\left({T}\right)\left({A}\right)=\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{A}={v}{\cdot }_{\mathrm{ih}}{f}\right)$
6 oveq2 ${⊢}{z}={A}\to {T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={T}\left({v}\right){\cdot }_{\mathrm{ih}}{A}$
7 6 eqeq1d ${⊢}{z}={A}\to \left({T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}↔{T}\left({v}\right){\cdot }_{\mathrm{ih}}{A}={v}{\cdot }_{\mathrm{ih}}{f}\right)$
8 7 ralbidv ${⊢}{z}={A}\to \left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}↔\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{A}={v}{\cdot }_{\mathrm{ih}}{f}\right)$
9 8 riotabidv ${⊢}{z}={A}\to \left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}\right)=\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{A}={v}{\cdot }_{\mathrm{ih}}{f}\right)$
10 eqid ${⊢}\left({z}\in ℋ⟼\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}\right)\right)=\left({z}\in ℋ⟼\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}\right)\right)$
11 riotaex ${⊢}\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{A}={v}{\cdot }_{\mathrm{ih}}{f}\right)\in \mathrm{V}$
12 9 10 11 fvmpt ${⊢}{A}\in ℋ\to \left({z}\in ℋ⟼\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}\right)\right)\left({A}\right)=\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{A}={v}{\cdot }_{\mathrm{ih}}{f}\right)$
13 5 12 eqtr4d ${⊢}{A}\in ℋ\to {adj}_{h}\left({T}\right)\left({A}\right)=\left({z}\in ℋ⟼\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}\right)\right)\left({A}\right)$
14 13 fveq2d ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({adj}_{h}\left({T}\right)\left({A}\right)\right)={norm}_{ℎ}\left(\left({z}\in ℋ⟼\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}\right)\right)\left({A}\right)\right)$
15 inss1 ${⊢}\mathrm{LinOp}\cap \mathrm{ContOp}\subseteq \mathrm{LinOp}$
16 lncnbd ${⊢}\mathrm{LinOp}\cap \mathrm{ContOp}=\mathrm{BndLinOp}$
17 1 16 eleqtrri ${⊢}{T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)$
18 15 17 sselii ${⊢}{T}\in \mathrm{LinOp}$
19 inss2 ${⊢}\mathrm{LinOp}\cap \mathrm{ContOp}\subseteq \mathrm{ContOp}$
20 19 17 sselii ${⊢}{T}\in \mathrm{ContOp}$
21 eqid ${⊢}\left({g}\in ℋ⟼{T}\left({g}\right){\cdot }_{\mathrm{ih}}{z}\right)=\left({g}\in ℋ⟼{T}\left({g}\right){\cdot }_{\mathrm{ih}}{z}\right)$
22 oveq2 ${⊢}{f}={w}\to {v}{\cdot }_{\mathrm{ih}}{f}={v}{\cdot }_{\mathrm{ih}}{w}$
23 22 eqeq2d ${⊢}{f}={w}\to \left({T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}↔{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
24 23 ralbidv ${⊢}{f}={w}\to \left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}↔\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
25 24 cbvriotavw ${⊢}\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}\right)=\left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
26 18 20 21 25 10 cnlnadjlem7 ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left(\left({z}\in ℋ⟼\left(\iota {f}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{z}={v}{\cdot }_{\mathrm{ih}}{f}\right)\right)\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$
27 14 26 eqbrtrd ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({adj}_{h}\left({T}\right)\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({A}\right)$