Theorem hosubcli

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

	Ref	Expression
Hypotheses	hoeq.1	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	hoeq.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	hosubcli	$$⊢\left(S{-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
2		hoeq.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
3		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)$$
4	1 2 3	mp2an	$$⊢S{-}_{\mathrm{op}}T=\left(x\in \mathscr{H}⟼S\left(x\right){-}_{ℎ}T\left(x\right)\right)$$
5	1	ffvelcdmi	$$⊢x\in \mathscr{H}\to S\left(x\right)\in \mathscr{H}$$
6	2	ffvelcdmi	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
7		hvsubcl	$$⊢\left(S\left(x\right)\in \mathscr{H}\wedge T\left(x\right)\in \mathscr{H}\right)\to S\left(x\right){-}_{ℎ}T\left(x\right)\in \mathscr{H}$$
8	5 6 7	syl2anc	$$⊢x\in \mathscr{H}\to S\left(x\right){-}_{ℎ}T\left(x\right)\in \mathscr{H}$$
9	4 8	fmpti	$$⊢\left(S{-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$