This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lnopsubi

Description: Subtraction property for a linear Hilbert space operator. (Contributed by NM, 1-Jul-2005) (New usage is discouraged.)

Ref Expression
Hypothesis lnopl.1 ⊢ 𝑇 ∈ LinOp
Assertion lnopsubi ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lnopl.1 ⊢ 𝑇 ∈ LinOp
2 neg1cn ⊢ - 1 ∈ ℂ
3 1 lnopaddmuli ⊢ ( ( - 1 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( 𝑇 ‘ 𝐴 ) +ℎ ( - 1 ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) )
4 2 3 mp3an1 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( 𝑇 ‘ 𝐴 ) +ℎ ( - 1 ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) )
5 hvsubval ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
6 5 fveq2d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( 𝑇 ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) )
7 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
8 7 ffvelcdmi ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
9 7 ffvelcdmi ⊢ ( 𝐵 ∈ ℋ → ( 𝑇 ‘ 𝐵 ) ∈ ℋ )
10 hvsubval ⊢ ( ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝐵 ) ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) +ℎ ( - 1 ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) )
11 8 9 10 syl2an ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) +ℎ ( - 1 ·ℎ ( 𝑇 ‘ 𝐵 ) ) ) )
12 4 6 11 3eqtr4d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) −ℎ ( 𝑇 ‘ 𝐵 ) ) )