Metamath Proof Explorer

Theorem lnopsubmuli

Description: Subtraction/product property of a linear Hilbert space operator. (Contributed by NM, 2-Jul-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 lnopl.1 ⊢ T ∈ LinOp
2 hvmulcl ⊢ A ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
3 1 lnopsubi ⊢ B ∈ ℋ ∧ A ⋅ ℎ C ∈ ℋ → T ⁡ B - ℎ A ⋅ ℎ C = T ⁡ B - ℎ T ⁡ A ⋅ ℎ C
4 2 3 sylan2 ⊢ B ∈ ℋ ∧ A ∈ ℂ ∧ C ∈ ℋ → T ⁡ B - ℎ A ⋅ ℎ C = T ⁡ B - ℎ T ⁡ A ⋅ ℎ C
5 4 3impb ⊢ B ∈ ℋ ∧ A ∈ ℂ ∧ C ∈ ℋ → T ⁡ B - ℎ A ⋅ ℎ C = T ⁡ B - ℎ T ⁡ A ⋅ ℎ C
6 5 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ B - ℎ A ⋅ ℎ C = T ⁡ B - ℎ T ⁡ A ⋅ ℎ C
7 1 lnopmuli ⊢ A ∈ ℂ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ C = A ⋅ ℎ T ⁡ C
8 7 oveq2d ⊢ A ∈ ℂ ∧ C ∈ ℋ → T ⁡ B - ℎ T ⁡ A ⋅ ℎ C = T ⁡ B - ℎ A ⋅ ℎ T ⁡ C
9 8 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ B - ℎ T ⁡ A ⋅ ℎ C = T ⁡ B - ℎ A ⋅ ℎ T ⁡ C
10 6 9 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ B - ℎ A ⋅ ℎ C = T ⁡ B - ℎ A ⋅ ℎ T ⁡ C