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 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 )