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 | ⊢ 𝑇 ∈ LinOp | |
| cnlnadjlem.2 | ⊢ 𝑇 ∈ ContOp | ||
| cnlnadjlem.3 | ⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) ) | ||
| Assertion | cnlnadjlem1 | ⊢ ( 𝐴 ∈ ℋ → ( 𝐺 ‘ 𝐴 ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝑦 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnlnadjlem.1 | ⊢ 𝑇 ∈ LinOp | |
| 2 | cnlnadjlem.2 | ⊢ 𝑇 ∈ ContOp | |
| 3 | cnlnadjlem.3 | ⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) ) | |
| 4 | fveq2 | ⊢ ( 𝑔 = 𝐴 → ( 𝑇 ‘ 𝑔 ) = ( 𝑇 ‘ 𝐴 ) ) | |
| 5 | 4 | oveq1d | ⊢ ( 𝑔 = 𝐴 → ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝑦 ) ) |
| 6 | ovex | ⊢ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝑦 ) ∈ V | |
| 7 | 5 3 6 | fvmpt | ⊢ ( 𝐴 ∈ ℋ → ( 𝐺 ‘ 𝐴 ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝑦 ) ) |