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