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	$$⊢T\in \mathrm{LinOp}$$
Assertion	lnopsubi	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{-}_{ℎ}B\right)=T\left(A\right){-}_{ℎ}T\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		lnopl.1	$$⊢T\in \mathrm{LinOp}$$
2		neg1cn	$$⊢-1\in ℂ$$
3	1	lnopaddmuli	$$⊢\left(-1\in ℂ\wedge A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=T\left(A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}T\left(B\right)\right)$$
4	2 3	mp3an1	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)=T\left(A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}T\left(B\right)\right)$$
5		hvsubval	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{-}_{ℎ}B=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
6	5	fveq2d	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{-}_{ℎ}B\right)=T\left(A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\right)$$
7	1	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
8	7	ffvelcdmi	$$⊢A\in \mathscr{H}\to T\left(A\right)\in \mathscr{H}$$
9	7	ffvelcdmi	$$⊢B\in \mathscr{H}\to T\left(B\right)\in \mathscr{H}$$
10		hvsubval	$$⊢\left(T\left(A\right)\in \mathscr{H}\wedge T\left(B\right)\in \mathscr{H}\right)\to T\left(A\right){-}_{ℎ}T\left(B\right)=T\left(A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}T\left(B\right)\right)$$
11	8 9 10	syl2an	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A\right){-}_{ℎ}T\left(B\right)=T\left(A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}T\left(B\right)\right)$$
12	4 6 11	3eqtr4d	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{-}_{ℎ}B\right)=T\left(A\right){-}_{ℎ}T\left(B\right)$$