# Metamath Proof Explorer

## Theorem hosubeq0i

Description: If the difference between two operators is zero, they are equal. (Contributed by NM, 27-Jul-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hosd1.2 ${⊢}{T}:ℋ⟶ℋ$
hosd1.3 ${⊢}{U}:ℋ⟶ℋ$
Assertion hosubeq0i ${⊢}{T}{-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}↔{T}={U}$

### Proof

Step Hyp Ref Expression
1 hosd1.2 ${⊢}{T}:ℋ⟶ℋ$
2 hosd1.3 ${⊢}{U}:ℋ⟶ℋ$
3 1 2 honegsubi ${⊢}{T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={T}{-}_{\mathrm{op}}{U}$
4 3 eqeq1i ${⊢}{T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={0}_{\mathrm{hop}}↔{T}{-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}$
5 oveq1 ${⊢}{T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={0}_{\mathrm{hop}}\to \left({T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right){+}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}{+}_{\mathrm{op}}{U}$
6 4 5 sylbir ${⊢}{T}{-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}\to \left({T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right){+}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}{+}_{\mathrm{op}}{U}$
7 neg1cn ${⊢}-1\in ℂ$
8 homulcl ${⊢}\left(-1\in ℂ\wedge {U}:ℋ⟶ℋ\right)\to \left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
9 7 2 8 mp2an ${⊢}\left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
10 1 9 2 hoadd32i ${⊢}\left({T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right){+}_{\mathrm{op}}{U}=\left({T}{+}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)$
11 1 2 9 hoaddassi ${⊢}\left({T}{+}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={T}{+}_{\mathrm{op}}\left({U}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)$
12 2 2 honegsubi ${⊢}{U}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={U}{-}_{\mathrm{op}}{U}$
13 2 hodidi ${⊢}{U}{-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}$
14 12 13 eqtri ${⊢}{U}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={0}_{\mathrm{hop}}$
15 14 oveq2i ${⊢}{T}{+}_{\mathrm{op}}\left({U}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)={T}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}$
16 1 hoaddid1i ${⊢}{T}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}={T}$
17 15 16 eqtri ${⊢}{T}{+}_{\mathrm{op}}\left({U}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)={T}$
18 11 17 eqtri ${⊢}\left({T}{+}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={T}$
19 10 18 eqtri ${⊢}\left({T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right){+}_{\mathrm{op}}{U}={T}$
20 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
21 20 2 hoaddcomi ${⊢}{0}_{\mathrm{hop}}{+}_{\mathrm{op}}{U}={U}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}$
22 2 hoaddid1i ${⊢}{U}{+}_{\mathrm{op}}{0}_{\mathrm{hop}}={U}$
23 21 22 eqtri ${⊢}{0}_{\mathrm{hop}}{+}_{\mathrm{op}}{U}={U}$
24 6 19 23 3eqtr3g ${⊢}{T}{-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}\to {T}={U}$
25 oveq1 ${⊢}{T}={U}\to {T}{-}_{\mathrm{op}}{U}={U}{-}_{\mathrm{op}}{U}$
26 25 13 syl6eq ${⊢}{T}={U}\to {T}{-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}$
27 24 26 impbii ${⊢}{T}{-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}↔{T}={U}$