# Metamath Proof Explorer

## 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}:ℋ⟶ℋ$
hodseq.3 ${⊢}{T}:ℋ⟶ℋ$
Assertion honegsubi ${⊢}{S}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)={S}{-}_{\mathrm{op}}{T}$

### Proof

Step Hyp Ref Expression
1 hodseq.2 ${⊢}{S}:ℋ⟶ℋ$
2 hodseq.3 ${⊢}{T}:ℋ⟶ℋ$
3 neg1cn ${⊢}-1\in ℂ$
4 homulcl ${⊢}\left(-1\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left(-1{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
5 3 2 4 mp2an ${⊢}\left(-1{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
6 hosval ${⊢}\left({S}:ℋ⟶ℋ\wedge \left(-1{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge {x}\in ℋ\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 ℋ\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 ffvelrni ${⊢}{x}\in ℋ\to {S}\left({x}\right)\in ℋ$
9 2 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
10 hvsubval ${⊢}\left({S}\left({x}\right)\in ℋ\wedge {T}\left({x}\right)\in ℋ\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 ℋ\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}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left(-1{·}_{\mathrm{op}}{T}\right)\left({x}\right)=-1{\cdot }_{ℎ}{T}\left({x}\right)$
13 3 2 12 mp3an12 ${⊢}{x}\in ℋ\to \left(-1{·}_{\mathrm{op}}{T}\right)\left({x}\right)=-1{\cdot }_{ℎ}{T}\left({x}\right)$
14 13 oveq2d ${⊢}{x}\in ℋ\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 ℋ\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 ℋ\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}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\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 ℋ\to \left({S}{-}_{\mathrm{op}}{T}\right)\left({x}\right)={S}\left({x}\right){-}_{ℎ}{T}\left({x}\right)$
19 16 18 eqtr4d ${⊢}{x}\in ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}\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):ℋ⟶ℋ$
22 1 2 hosubcli ${⊢}\left({S}{-}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
23 21 22 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)\right)\left({x}\right)=\left({S}{-}_{\mathrm{op}}{T}\right)\left({x}\right)↔{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}$