# Metamath Proof Explorer

## 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}:ℋ⟶ℋ$
hods.2 ${⊢}{S}:ℋ⟶ℋ$
hods.3 ${⊢}{T}:ℋ⟶ℋ$
Assertion hodsi ${⊢}{R}{-}_{\mathrm{op}}{S}={T}↔{S}{+}_{\mathrm{op}}{T}={R}$

### Proof

Step Hyp Ref Expression
1 hods.1 ${⊢}{R}:ℋ⟶ℋ$
2 hods.2 ${⊢}{S}:ℋ⟶ℋ$
3 hods.3 ${⊢}{T}:ℋ⟶ℋ$
4 1 ffvelrni ${⊢}{x}\in ℋ\to {R}\left({x}\right)\in ℋ$
5 2 ffvelrni ${⊢}{x}\in ℋ\to {S}\left({x}\right)\in ℋ$
6 3 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
7 hvsubadd ${⊢}\left({R}\left({x}\right)\in ℋ\wedge {S}\left({x}\right)\in ℋ\wedge {T}\left({x}\right)\in ℋ\right)\to \left({R}\left({x}\right){-}_{ℎ}{S}\left({x}\right)={T}\left({x}\right)↔{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)={R}\left({x}\right)\right)$
8 4 5 6 7 syl3anc ${⊢}{x}\in ℋ\to \left({R}\left({x}\right){-}_{ℎ}{S}\left({x}\right)={T}\left({x}\right)↔{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)={R}\left({x}\right)\right)$
9 hodval ${⊢}\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge {x}\in ℋ\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 ℋ\to \left({R}{-}_{\mathrm{op}}{S}\right)\left({x}\right)={R}\left({x}\right){-}_{ℎ}{S}\left({x}\right)$
11 10 eqeq1d ${⊢}{x}\in ℋ\to \left(\left({R}{-}_{\mathrm{op}}{S}\right)\left({x}\right)={T}\left({x}\right)↔{R}\left({x}\right){-}_{ℎ}{S}\left({x}\right)={T}\left({x}\right)\right)$
12 hosval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\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 ℋ\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
14 13 eqeq1d ${⊢}{x}\in ℋ\to \left(\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={R}\left({x}\right)↔{S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)={R}\left({x}\right)\right)$
15 8 11 14 3bitr4d ${⊢}{x}\in ℋ\to \left(\left({R}{-}_{\mathrm{op}}{S}\right)\left({x}\right)={T}\left({x}\right)↔\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={R}\left({x}\right)\right)$
16 15 ralbiia ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({R}{-}_{\mathrm{op}}{S}\right)\left({x}\right)={T}\left({x}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={R}\left({x}\right)$
17 1 2 hosubcli ${⊢}\left({R}{-}_{\mathrm{op}}{S}\right):ℋ⟶ℋ$
18 17 3 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({R}{-}_{\mathrm{op}}{S}\right)\left({x}\right)={T}\left({x}\right)↔{R}{-}_{\mathrm{op}}{S}={T}$
19 2 3 hoaddcli ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
20 19 1 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={R}\left({x}\right)↔{S}{+}_{\mathrm{op}}{T}={R}$
21 16 18 20 3bitr3i ${⊢}{R}{-}_{\mathrm{op}}{S}={T}↔{S}{+}_{\mathrm{op}}{T}={R}$