# 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$