Theorem cnlnadj

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
Assertion	cnlnadj	$$⊢T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \exists t\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}t\left(y\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnlnadjeu	$$⊢T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \exists !t\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}t\left(y\right)$$
2		reurex	$$⊢\exists !t\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}t\left(y\right)\to \exists t\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}t\left(y\right)$$
3	1 2	syl	$$⊢T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \exists t\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}t\left(y\right)$$