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 \mathscr{H}⟼T\left(g\right){\cdot }_{\mathrm{ih}}y\right)$$
	cnlnadjlem.4	$$⊢B=\left(\iota w\in \mathscr{H}|\forall v\in \mathscr{H}T\left(v\right){\cdot }_{\mathrm{ih}}y=v{\cdot }_{\mathrm{ih}}w\right)$$
	cnlnadjlem.5	$$⊢F=\left(y\in \mathscr{H}⟼B\right)$$
Assertion	cnlnadjlem4	$$⊢A\in \mathscr{H}\to F\left(A\right)\in \mathscr{H}$$

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