Theorem hodsi

Description: Relationship between Hilbert space operator difference and sum. (Contributed by NM, 17-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hods.1	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
	hods.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	hods.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	hodsi	$$⊢R{-}_{\mathrm{op}}S=T\leftrightarrow S{+}_{\mathrm{op}}T=R$$

Proof

Step	Hyp	Ref	Expression
1		hods.1	$$⊢R:\mathscr{H}⟶\mathscr{H}$$
2		hods.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
3		hods.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
4	1	ffvelcdmi	$$⊢x\in \mathscr{H}\to R\left(x\right)\in \mathscr{H}$$
5	2	ffvelcdmi	$$⊢x\in \mathscr{H}\to S\left(x\right)\in \mathscr{H}$$
6	3	ffvelcdmi	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
7		hvsubadd	$$⊢\left(R\left(x\right)\in \mathscr{H}\wedge S\left(x\right)\in \mathscr{H}\wedge T\left(x\right)\in \mathscr{H}\right)\to \left(R\left(x\right){-}_{ℎ}S\left(x\right)=T\left(x\right)\leftrightarrow S\left(x\right){+}_{ℎ}T\left(x\right)=R\left(x\right)\right)$$
8	4 5 6 7	syl3anc	$$⊢x\in \mathscr{H}\to \left(R\left(x\right){-}_{ℎ}S\left(x\right)=T\left(x\right)\leftrightarrow S\left(x\right){+}_{ℎ}T\left(x\right)=R\left(x\right)\right)$$
9		hodval	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(R{-}_{\mathrm{op}}S\right)\left(x\right)=R\left(x\right){-}_{ℎ}S\left(x\right)$$
10	1 2 9	mp3an12	$$⊢x\in \mathscr{H}\to \left(R{-}_{\mathrm{op}}S\right)\left(x\right)=R\left(x\right){-}_{ℎ}S\left(x\right)$$
11	10	eqeq1d	$$⊢x\in \mathscr{H}\to \left(\left(R{-}_{\mathrm{op}}S\right)\left(x\right)=T\left(x\right)\leftrightarrow R\left(x\right){-}_{ℎ}S\left(x\right)=T\left(x\right)\right)$$
12		hosval	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}T\right)\left(x\right)=S\left(x\right){+}_{ℎ}T\left(x\right)$$
13	2 3 12	mp3an12	$$⊢x\in \mathscr{H}\to \left(S{+}_{\mathrm{op}}T\right)\left(x\right)=S\left(x\right){+}_{ℎ}T\left(x\right)$$
14	13	eqeq1d	$$⊢x\in \mathscr{H}\to \left(\left(S{+}_{\mathrm{op}}T\right)\left(x\right)=R\left(x\right)\leftrightarrow S\left(x\right){+}_{ℎ}T\left(x\right)=R\left(x\right)\right)$$
15	8 11 14	3bitr4d	$$⊢x\in \mathscr{H}\to \left(\left(R{-}_{\mathrm{op}}S\right)\left(x\right)=T\left(x\right)\leftrightarrow \left(S{+}_{\mathrm{op}}T\right)\left(x\right)=R\left(x\right)\right)$$
16	15	ralbiia	$$⊢\forall x\in \mathscr{H}\left(R{-}_{\mathrm{op}}S\right)\left(x\right)=T\left(x\right)\leftrightarrow \forall x\in \mathscr{H}\left(S{+}_{\mathrm{op}}T\right)\left(x\right)=R\left(x\right)$$
17	1 2	hosubcli	$$⊢\left(R{-}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}$$
18	17 3	hoeqi	$$⊢\forall x\in \mathscr{H}\left(R{-}_{\mathrm{op}}S\right)\left(x\right)=T\left(x\right)\leftrightarrow R{-}_{\mathrm{op}}S=T$$
19	2 3	hoaddcli	$$⊢\left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
20	19 1	hoeqi	$$⊢\forall x\in \mathscr{H}\left(S{+}_{\mathrm{op}}T\right)\left(x\right)=R\left(x\right)\leftrightarrow S{+}_{\mathrm{op}}T=R$$
21	16 18 20	3bitr3i	$$⊢R{-}_{\mathrm{op}}S=T\leftrightarrow S{+}_{\mathrm{op}}T=R$$