Theorem hodval

Description: Value of the difference of two Hilbert space operators. (Contributed by NM, 10-Nov-2000) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	hodval	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}T\right)\left(A\right)=S\left(A\right){-}_{ℎ}T\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		hodmval	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to S{-}_{\mathrm{op}}T=\left(x\in \mathscr{H}⟼S\left(x\right){-}_{ℎ}T\left(x\right)\right)$$
2	1	fveq1d	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}T\right)\left(A\right)=\left(x\in \mathscr{H}⟼S\left(x\right){-}_{ℎ}T\left(x\right)\right)\left(A\right)$$
3		fveq2	$$⊢x=A\to S\left(x\right)=S\left(A\right)$$
4		fveq2	$$⊢x=A\to T\left(x\right)=T\left(A\right)$$
5	3 4	oveq12d	$$⊢x=A\to S\left(x\right){-}_{ℎ}T\left(x\right)=S\left(A\right){-}_{ℎ}T\left(A\right)$$
6		eqid	$$⊢\left(x\in \mathscr{H}⟼S\left(x\right){-}_{ℎ}T\left(x\right)\right)=\left(x\in \mathscr{H}⟼S\left(x\right){-}_{ℎ}T\left(x\right)\right)$$
7		ovex	$$⊢S\left(A\right){-}_{ℎ}T\left(A\right)\in \mathrm{V}$$
8	5 6 7	fvmpt	$$⊢A\in \mathscr{H}\to \left(x\in \mathscr{H}⟼S\left(x\right){-}_{ℎ}T\left(x\right)\right)\left(A\right)=S\left(A\right){-}_{ℎ}T\left(A\right)$$
9	2 8	sylan9eq	$$⊢\left(\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\wedge A\in \mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}T\right)\left(A\right)=S\left(A\right){-}_{ℎ}T\left(A\right)$$
10	9	3impa	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge A\in \mathscr{H}\right)\to \left(S{-}_{\mathrm{op}}T\right)\left(A\right)=S\left(A\right){-}_{ℎ}T\left(A\right)$$