Theorem hoaddcl

Description: The sum of Hilbert space operators is an operator. (Contributed by NM, 21-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	hoaddcl	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to S\left(x\right)\in \mathscr{H}$$
2	1	adantlr	$$⊢\left(\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\wedge x\in \mathscr{H}\right)\to S\left(x\right)\in \mathscr{H}$$
3		ffvelrn	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to T\left(x\right)\in \mathscr{H}$$
4	3	adantll	$$⊢\left(\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\wedge x\in \mathscr{H}\right)\to T\left(x\right)\in \mathscr{H}$$
5		hvaddcl	$$⊢\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}$$
6	2 4 5	syl2anc	$$⊢\left(\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\wedge x\in \mathscr{H}\right)\to S\left(x\right){+}_{ℎ}T\left(x\right)\in \mathscr{H}$$
7	6	fmpttd	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(x\in \mathscr{H}⟼S\left(x\right){+}_{ℎ}T\left(x\right)\right):\mathscr{H}⟶\mathscr{H}$$
8		hosmval	$$⊢\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)$$
9	8	feq1d	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\leftrightarrow \left(x\in \mathscr{H}⟼S\left(x\right){+}_{ℎ}T\left(x\right)\right):\mathscr{H}⟶\mathscr{H}\right)$$
10	7 9	mpbird	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$