Metamath Proof Explorer

Theorem lnfnmul

Description: Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion lnfnmul ⊢ T ∈ LinFn ∧ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B = A ⁢ T ⁡ B

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ T = if T ∈ LinFn T ℋ × 0 → T ⁡ A ⋅ ℎ B = if T ∈ LinFn T ℋ × 0 ⁡ A ⋅ ℎ B
2 fveq1 ⊢ T = if T ∈ LinFn T ℋ × 0 → T ⁡ B = if T ∈ LinFn T ℋ × 0 ⁡ B
3 2 oveq2d ⊢ T = if T ∈ LinFn T ℋ × 0 → A ⁢ T ⁡ B = A ⁢ if T ∈ LinFn T ℋ × 0 ⁡ B
4 1 3 eqeq12d ⊢ T = if T ∈ LinFn T ℋ × 0 → T ⁡ A ⋅ ℎ B = A ⁢ T ⁡ B ↔ if T ∈ LinFn T ℋ × 0 ⁡ A ⋅ ℎ B = A ⁢ if T ∈ LinFn T ℋ × 0 ⁡ B
5 4 imbi2d ⊢ T = if T ∈ LinFn T ℋ × 0 → A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B = A ⁢ T ⁡ B ↔ A ∈ ℂ ∧ B ∈ ℋ → if T ∈ LinFn T ℋ × 0 ⁡ A ⋅ ℎ B = A ⁢ if T ∈ LinFn T ℋ × 0 ⁡ B
6 0lnfn ⊢ ℋ × 0 ∈ LinFn
7 6 elimel ⊢ if T ∈ LinFn T ℋ × 0 ∈ LinFn
8 7 lnfnmuli ⊢ A ∈ ℂ ∧ B ∈ ℋ → if T ∈ LinFn T ℋ × 0 ⁡ A ⋅ ℎ B = A ⁢ if T ∈ LinFn T ℋ × 0 ⁡ B
9 5 8 dedth ⊢ T ∈ LinFn → A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B = A ⁢ T ⁡ B
10 9 3impib ⊢ T ∈ LinFn ∧ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B = A ⁢ T ⁡ B