Theorem hosmval

Description: Value of the sum of two Hilbert space operators. (Contributed by NM, 9-Nov-2000) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
2	1 1	elmap	$$⊢S\in \left({\mathscr{H}}^{\mathscr{H}}\right)\leftrightarrow S:\mathscr{H}⟶\mathscr{H}$$
3	1 1	elmap	$$⊢T\in \left({\mathscr{H}}^{\mathscr{H}}\right)\leftrightarrow T:\mathscr{H}⟶\mathscr{H}$$
4		fveq1	$$⊢f=S\to f\left(x\right)=S\left(x\right)$$
5	4	oveq1d	$$⊢f=S\to f\left(x\right){+}_{ℎ}g\left(x\right)=S\left(x\right){+}_{ℎ}g\left(x\right)$$
6	5	mpteq2dv	$$⊢f=S\to \left(x\in \mathscr{H}⟼f\left(x\right){+}_{ℎ}g\left(x\right)\right)=\left(x\in \mathscr{H}⟼S\left(x\right){+}_{ℎ}g\left(x\right)\right)$$
7		fveq1	$$⊢g=T\to g\left(x\right)=T\left(x\right)$$
8	7	oveq2d	$$⊢g=T\to S\left(x\right){+}_{ℎ}g\left(x\right)=S\left(x\right){+}_{ℎ}T\left(x\right)$$
9	8	mpteq2dv	$$⊢g=T\to \left(x\in \mathscr{H}⟼S\left(x\right){+}_{ℎ}g\left(x\right)\right)=\left(x\in \mathscr{H}⟼S\left(x\right){+}_{ℎ}T\left(x\right)\right)$$
10		df-hosum	$$⊢{+}_{\mathrm{op}}=\left(f\in \left({\mathscr{H}}^{\mathscr{H}}\right),g\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼f\left(x\right){+}_{ℎ}g\left(x\right)\right)\right)$$
11	1	mptex	$$⊢\left(x\in \mathscr{H}⟼S\left(x\right){+}_{ℎ}T\left(x\right)\right)\in \mathrm{V}$$
12	6 9 10 11	ovmpo	$$⊢\left(S\in \left({\mathscr{H}}^{\mathscr{H}}\right)\wedge T\in \left({\mathscr{H}}^{\mathscr{H}}\right)\right)\to S{+}_{\mathrm{op}}T=\left(x\in \mathscr{H}⟼S\left(x\right){+}_{ℎ}T\left(x\right)\right)$$
13	2 3 12	syl2anbr	$$⊢\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)$$