# Metamath Proof Explorer

## Theorem cnlnadjlem4

Description: Lemma for cnlnadji . The values of auxiliary function F are vectors. (Contributed by NM, 17-Feb-2006) (Proof shortened by Mario Carneiro, 10-Sep-2015) (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)$
cnlnadjlem.4 ${⊢}{B}=\left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
cnlnadjlem.5 ${⊢}{F}=\left({y}\in ℋ⟼{B}\right)$
Assertion cnlnadjlem4 ${⊢}{A}\in ℋ\to {F}\left({A}\right)\in ℋ$

### 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 cnlnadjlem.4 ${⊢}{B}=\left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
5 cnlnadjlem.5 ${⊢}{F}=\left({y}\in ℋ⟼{B}\right)$
6 1 2 3 4 cnlnadjlem3 ${⊢}{y}\in ℋ\to {B}\in ℋ$
7 5 6 fmpti ${⊢}{F}:ℋ⟶ℋ$
8 7 ffvelrni ${⊢}{A}\in ℋ\to {F}\left({A}\right)\in ℋ$