# Metamath Proof Explorer

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 ℋ⟼{T}\left({g}\right){\cdot }_{\mathrm{ih}}{y}\right)$
Assertion cnlnadjlem1 ${⊢}{A}\in ℋ\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 ℋ⟼{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 ℋ\to {G}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{y}$