# Metamath Proof Explorer

Description: Every continuous linear operator has an adjoint. Theorem 3.10 of Beran p. 104. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadj.1 ${⊢}{T}\in \mathrm{LinOp}$
cnlnadj.2 ${⊢}{T}\in \mathrm{ContOp}$
Assertion cnlnadji ${⊢}\exists {t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)$

### Proof

Step Hyp Ref Expression
1 cnlnadj.1 ${⊢}{T}\in \mathrm{LinOp}$
2 cnlnadj.2 ${⊢}{T}\in \mathrm{ContOp}$
3 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)$
4 oveq2 ${⊢}{f}={w}\to {v}{\cdot }_{\mathrm{ih}}{f}={v}{\cdot }_{\mathrm{ih}}{w}$
5 4 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)$
6 5 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)$
7 6 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)$
8 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)$
9 1 2 3 7 8 cnlnadjlem9 ${⊢}\exists {t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)$