Theorem cnlnadjlem1

Description: Lemma for cnlnadji (Theorem 3.10 of Beran p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional G . (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cnlnadjlem.1	$$⊢T\in \mathrm{LinOp}$$
	cnlnadjlem.2	$$⊢T\in \mathrm{ContOp}$$
	cnlnadjlem.3	$$⊢G=\left(g\in \mathscr{H}⟼T\left(g\right){\cdot }_{\mathrm{ih}}y\right)$$
Assertion	cnlnadjlem1	$$⊢A\in \mathscr{H}\to G\left(A\right)=T\left(A\right){\cdot }_{\mathrm{ih}}y$$

Proof

Step	Hyp	Ref	Expression
1		cnlnadjlem.1	$$⊢T\in \mathrm{LinOp}$$
2		cnlnadjlem.2	$$⊢T\in \mathrm{ContOp}$$
3		cnlnadjlem.3	$$⊢G=\left(g\in \mathscr{H}⟼T\left(g\right){\cdot }_{\mathrm{ih}}y\right)$$
4		fveq2	$$⊢g=A\to T\left(g\right)=T\left(A\right)$$
5	4	oveq1d	$$⊢g=A\to T\left(g\right){\cdot }_{\mathrm{ih}}y=T\left(A\right){\cdot }_{\mathrm{ih}}y$$
6		ovex	$$⊢T\left(A\right){\cdot }_{\mathrm{ih}}y\in \mathrm{V}$$
7	5 3 6	fvmpt	$$⊢A\in \mathscr{H}\to G\left(A\right)=T\left(A\right){\cdot }_{\mathrm{ih}}y$$