Metamath Proof Explorer

Theorem lnopmulsubi

Description: Product/subtraction 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 lnopmulsubi ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B - ℎ C = A ⋅ ℎ T ⁡ B - ℎ T ⁡ C

Proof

Step Hyp Ref Expression
1 lnopl.1 ⊢ T ∈ LinOp
2 hvmulcl ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B ∈ ℋ
3 1 lnopsubi ⊢ A ⋅ ℎ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B - ℎ C = T ⁡ A ⋅ ℎ B - ℎ T ⁡ C
4 2 3 stoic3 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B - ℎ C = T ⁡ A ⋅ ℎ B - ℎ T ⁡ C
5 1 lnopmuli ⊢ A ∈ ℂ ∧ B ∈ ℋ → T ⁡ A ⋅ ℎ B = A ⋅ ℎ T ⁡ B
6 5 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B = A ⋅ ℎ T ⁡ B
7 6 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B - ℎ T ⁡ C = A ⋅ ℎ T ⁡ B - ℎ T ⁡ C
8 4 7 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ B - ℎ C = A ⋅ ℎ T ⁡ B - ℎ T ⁡ C