Metamath Proof Explorer

Theorem lnopsubi

Description: Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005) (New usage is discouraged.)

Ref Expression
Hypothesis lnopl.1 ⊢ T ∈ LinOp
Assertion lnopsubi ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A - ℎ B = T ⁡ A - ℎ T ⁡ B

Proof

Step Hyp Ref Expression
1 lnopl.1 ⊢ T ∈ LinOp
2 neg1cn ⊢ − 1 ∈ ℂ
3 1 lnopaddmuli ⊢ − 1 ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A + ℎ -1 ⋅ ℎ B = T ⁡ A + ℎ -1 ⋅ ℎ T ⁡ B
4 2 3 mp3an1 ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A + ℎ -1 ⋅ ℎ B = T ⁡ A + ℎ -1 ⋅ ℎ T ⁡ B
5 hvsubval ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B = A + ℎ -1 ⋅ ℎ B
6 5 fveq2d ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A - ℎ B = T ⁡ A + ℎ -1 ⋅ ℎ B
7 1 lnopfi ⊢ T : ℋ ⟶ ℋ
8 7 ffvelcdmi ⊢ A ∈ ℋ → T ⁡ A ∈ ℋ
9 7 ffvelcdmi ⊢ B ∈ ℋ → T ⁡ B ∈ ℋ
10 hvsubval ⊢ T ⁡ A ∈ ℋ ∧ T ⁡ B ∈ ℋ → T ⁡ A - ℎ T ⁡ B = T ⁡ A + ℎ -1 ⋅ ℎ T ⁡ B
11 8 9 10 syl2an ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A - ℎ T ⁡ B = T ⁡ A + ℎ -1 ⋅ ℎ T ⁡ B
12 4 6 11 3eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A - ℎ B = T ⁡ A - ℎ T ⁡ B