# Metamath Proof Explorer

## Theorem hosubneg

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

Ref Expression
Assertion hosubneg ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {T}{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={T}{+}_{\mathrm{op}}{U}$

### Proof

Step Hyp Ref Expression
1 neg1cn ${⊢}-1\in ℂ$
2 homulcl ${⊢}\left(-1\in ℂ\wedge {U}:ℋ⟶ℋ\right)\to \left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
3 1 2 mpan ${⊢}{U}:ℋ⟶ℋ\to \left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
4 honegsub ${⊢}\left({T}:ℋ⟶ℋ\wedge \left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)\to {T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)={T}{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)$
5 3 4 sylan2 ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)={T}{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)$
6 honegneg ${⊢}{U}:ℋ⟶ℋ\to -1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={U}$
7 6 oveq2d ${⊢}{U}:ℋ⟶ℋ\to {T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)={T}{+}_{\mathrm{op}}{U}$
8 7 adantl ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)={T}{+}_{\mathrm{op}}{U}$
9 5 8 eqtr3d ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {T}{-}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={T}{+}_{\mathrm{op}}{U}$