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 𝑇 ∈ LinOp
Assertion lnopsubmuli ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) − ( 𝐴 · ( 𝑇𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 lnopl.1 𝑇 ∈ LinOp
2 hvmulcl ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 · 𝐶 ) ∈ ℋ )
3 1 lnopsubi ( ( 𝐵 ∈ ℋ ∧ ( 𝐴 · 𝐶 ) ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) − ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) )
4 2 3 sylan2 ( ( 𝐵 ∈ ℋ ∧ ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) ) → ( 𝑇 ‘ ( 𝐵 ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) − ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) )
5 4 3impb ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) − ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) )
6 5 3com12 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) − ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) )
7 1 lnopmuli ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) = ( 𝐴 · ( 𝑇𝐶 ) ) )
8 7 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( ( 𝑇𝐵 ) − ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) − ( 𝐴 · ( 𝑇𝐶 ) ) ) )
9 8 3adant2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝑇𝐵 ) − ( 𝑇 ‘ ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) − ( 𝐴 · ( 𝑇𝐶 ) ) ) )
10 6 9 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐵 ( 𝐴 · 𝐶 ) ) ) = ( ( 𝑇𝐵 ) − ( 𝐴 · ( 𝑇𝐶 ) ) ) )