Metamath Proof Explorer

Theorem lnopaddmuli

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

Ref Expression
Hypothesis lnopl.1 ⊢ T ∈ LinOp
Assertion lnopaddmuli ⊢ 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 lnopaddi ⊢ 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 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → T ⁡ A ⋅ ℎ C = A ⋅ ℎ T ⁡ C
9 8 oveq2d ⊢ 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