Theorem cnlnadjeu

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

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		fveq1	$$⊢T=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\to T\left(x\right)=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\left(x\right)$$
2	1	oveq1d	$$⊢T=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\to T\left(x\right){\cdot }_{\mathrm{ih}}y=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\left(x\right){\cdot }_{\mathrm{ih}}y$$
3	2	eqeq1d	$$⊢T=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\to \left(T\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}t\left(y\right)\leftrightarrow if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}t\left(y\right)\right)$$
4	3	2ralbidv	$$⊢T=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\to \left(\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)\leftrightarrow \forall x\in \mathscr{H}\forall y\in \mathscr{H}if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}t\left(y\right)\right)$$
5	4	reubidv	$$⊢T=if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\to \left(\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)\leftrightarrow \exists !t\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}t\left(y\right)\right)$$
6		inss1	$$⊢\mathrm{LinOp}\cap \mathrm{ContOp}\subseteq \mathrm{LinOp}$$
7		0lnop	$$⊢0_{\mathrm{hop}}\in \mathrm{LinOp}$$
8		0cnop	$$⊢0_{\mathrm{hop}}\in \mathrm{ContOp}$$
9		elin	$$⊢0_{\mathrm{hop}}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\leftrightarrow \left(0_{\mathrm{hop}}\in \mathrm{LinOp}\wedge 0_{\mathrm{hop}}\in \mathrm{ContOp}\right)$$
10	7 8 9	mpbir2an	$$⊢0_{\mathrm{hop}}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)$$
11	10	elimel	$$⊢if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)$$
12	6 11	sselii	$$⊢if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\in \mathrm{LinOp}$$
13		inss2	$$⊢\mathrm{LinOp}\cap \mathrm{ContOp}\subseteq \mathrm{ContOp}$$
14	13 11	sselii	$$⊢if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\in \mathrm{ContOp}$$
15	12 14	cnlnadjeui	$$⊢\exists !t\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\forall x\in \mathscr{H}\forall y\in \mathscr{H}if\left(T\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right),T,0_{\mathrm{hop}}\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}t\left(y\right)$$
16	5 15	dedth	$$⊢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)$$