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 e. LinOp
	cnlnadjlem.2	|- T e. ContOp
	cnlnadjlem.3	|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
	cnlnadjlem.4	|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
	cnlnadjlem.5	|- F = ( y e. ~H |-> B )
Assertion	cnlnadjlem4	|- ( A e. ~H -> ( F ` A ) e. ~H )

Proof

Step	Hyp	Ref	Expression
1		cnlnadjlem.1	|- T e. LinOp
2		cnlnadjlem.2	|- T e. ContOp
3		cnlnadjlem.3	|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
4		cnlnadjlem.4	|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
5		cnlnadjlem.5	|- F = ( y e. ~H |-> B )
6	1 2 3 4	cnlnadjlem3	|- ( y e. ~H -> B e. ~H )
7	5 6	fmpti	|- F : ~H --> ~H
8	7	ffvelrni	|- ( A e. ~H -> ( F ` A ) e. ~H )