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