Theorem honegsubi

Description: Relationship between Hilbert operator addition and subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hodseq.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
	hodseq.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	honegsubi	$$⊢S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=S{-}_{\mathrm{op}}T$$

Proof

Step	Hyp	Ref	Expression
1		hodseq.2	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
2		hodseq.3	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
3		neg1cn	$$⊢-1\in ℂ$$
4		homulcl	$$⊢\left(-1\in ℂ\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(-1{·}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
5	3 2 4	mp2an	$$⊢\left(-1{·}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
6		hosval	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge \left(-1{·}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\right)\left(x\right)=S\left(x\right){+}_{ℎ}\left(-1{·}_{\mathrm{op}}T\right)\left(x\right)$$
7	1 5 6	mp3an12	$$⊢x\in \mathscr{H}\to \left(S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\right)\left(x\right)=S\left(x\right){+}_{ℎ}\left(-1{·}_{\mathrm{op}}T\right)\left(x\right)$$
8	1	ffvelcdmi	$$⊢x\in \mathscr{H}\to S\left(x\right)\in \mathscr{H}$$
9	2	ffvelcdmi	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
10		hvsubval	$$⊢\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)=S\left(x\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}T\left(x\right)\right)$$
11	8 9 10	syl2anc	$$⊢x\in \mathscr{H}\to S\left(x\right){-}_{ℎ}T\left(x\right)=S\left(x\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}T\left(x\right)\right)$$
12		homval	$$⊢\left(-1\in ℂ\wedge T:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(-1{·}_{\mathrm{op}}T\right)\left(x\right)=-1{\cdot }_{ℎ}T\left(x\right)$$
13	3 2 12	mp3an12	$$⊢x\in \mathscr{H}\to \left(-1{·}_{\mathrm{op}}T\right)\left(x\right)=-1{\cdot }_{ℎ}T\left(x\right)$$
14	13	oveq2d	$$⊢x\in \mathscr{H}\to S\left(x\right){+}_{ℎ}\left(-1{·}_{\mathrm{op}}T\right)\left(x\right)=S\left(x\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}T\left(x\right)\right)$$
15	11 14	eqtr4d	$$⊢x\in \mathscr{H}\to S\left(x\right){-}_{ℎ}T\left(x\right)=S\left(x\right){+}_{ℎ}\left(-1{·}_{\mathrm{op}}T\right)\left(x\right)$$
16	7 15	eqtr4d	$$⊢x\in \mathscr{H}\to \left(S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\right)\left(x\right)=S\left(x\right){-}_{ℎ}T\left(x\right)$$
17		hodval	$$⊢\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)$$
18	1 2 17	mp3an12	$$⊢x\in \mathscr{H}\to \left(S{-}_{\mathrm{op}}T\right)\left(x\right)=S\left(x\right){-}_{ℎ}T\left(x\right)$$
19	16 18	eqtr4d	$$⊢x\in \mathscr{H}\to \left(S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\right)\left(x\right)=\left(S{-}_{\mathrm{op}}T\right)\left(x\right)$$
20	19	rgen	$$⊢\forall x\in \mathscr{H}\left(S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\right)\left(x\right)=\left(S{-}_{\mathrm{op}}T\right)\left(x\right)$$
21	1 5	hoaddcli	$$⊢\left(S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\right):\mathscr{H}⟶\mathscr{H}$$
22	1 2	hosubcli	$$⊢\left(S{-}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
23	21 22	hoeqi	$$⊢\forall x\in \mathscr{H}\left(S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\right)\left(x\right)=\left(S{-}_{\mathrm{op}}T\right)\left(x\right)\leftrightarrow S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=S{-}_{\mathrm{op}}T$$
24	20 23	mpbi	$$⊢S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=S{-}_{\mathrm{op}}T$$