Description: Lemma for cnlnadji (Theorem 3.10 of Beran p. 104: every continuous linear operator has an adjoint). The value of the auxiliary functional G . (Contributed by NM, 16-Feb-2006) (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 ) ) |
||
| Assertion | cnlnadjlem1 | |- ( A e. ~H -> ( G ` A ) = ( ( T ` A ) .ih y ) ) |
| 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 | fveq2 | |- ( g = A -> ( T ` g ) = ( T ` A ) ) |
|
| 5 | 4 | oveq1d | |- ( g = A -> ( ( T ` g ) .ih y ) = ( ( T ` A ) .ih y ) ) |
| 6 | ovex | |- ( ( T ` A ) .ih y ) e. _V |
|
| 7 | 5 3 6 | fvmpt | |- ( A e. ~H -> ( G ` A ) = ( ( T ` A ) .ih y ) ) |