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 - op U = 0 hop T = U

Proof

Step Hyp Ref Expression
1 hosd1.2 T :
2 hosd1.3 U :
3 1 2 honegsubi T + op -1 · op U = T - op U
4 3 eqeq1i T + op -1 · op U = 0 hop T - op U = 0 hop
5 oveq1 T + op -1 · op U = 0 hop T + op -1 · op U + op U = 0 hop + op U
6 4 5 sylbir T - op U = 0 hop T + op -1 · op U + op U = 0 hop + op U
7 neg1cn 1
8 homulcl 1 U : -1 · op U :
9 7 2 8 mp2an -1 · op U :
10 1 9 2 hoadd32i T + op -1 · op U + op U = T + op U + op -1 · op U
11 1 2 9 hoaddassi T + op U + op -1 · op U = T + op U + op -1 · op U
12 2 2 honegsubi U + op -1 · op U = U - op U
13 2 hodidi U - op U = 0 hop
14 12 13 eqtri U + op -1 · op U = 0 hop
15 14 oveq2i T + op U + op -1 · op U = T + op 0 hop
16 1 hoaddid1i T + op 0 hop = T
17 15 16 eqtri T + op U + op -1 · op U = T
18 11 17 eqtri T + op U + op -1 · op U = T
19 10 18 eqtri T + op -1 · op U + op U = T
20 ho0f 0 hop :
21 20 2 hoaddcomi 0 hop + op U = U + op 0 hop
22 2 hoaddid1i U + op 0 hop = U
23 21 22 eqtri 0 hop + op U = U
24 6 19 23 3eqtr3g T - op U = 0 hop T = U
25 oveq1 T = U T - op U = U - op U
26 25 13 syl6eq T = U T - op U = 0 hop
27 24 26 impbii T - op U = 0 hop T = U