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