This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 : ℋ ⟶ ℋ
hosd1.3 ⊢ 𝑈 : ℋ ⟶ ℋ
Assertion hosubeq0i ( ( 𝑇 −op 𝑈 ) = 0hop ↔ 𝑇 = 𝑈 )

Proof

Step Hyp Ref Expression
1 hosd1.2 ⊢ 𝑇 : ℋ ⟶ ℋ
2 hosd1.3 ⊢ 𝑈 : ℋ ⟶ ℋ
3 1 2 honegsubi ⊢ ( 𝑇 +op ( - 1 ·op 𝑈 ) ) = ( 𝑇 −op 𝑈 )
4 3 eqeq1i ⊢ ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) = 0hop ↔ ( 𝑇 −op 𝑈 ) = 0hop )
5 oveq1 ⊢ ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) = 0hop → ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) +op 𝑈 ) = ( 0hop +op 𝑈 ) )
6 4 5 sylbir ⊢ ( ( 𝑇 −op 𝑈 ) = 0hop → ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) +op 𝑈 ) = ( 0hop +op 𝑈 ) )
7 neg1cn ⊢ - 1 ∈ ℂ
8 homulcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ )
9 7 2 8 mp2an ⊢ ( - 1 ·op 𝑈 ) : ℋ ⟶ ℋ
10 1 9 2 hoadd32i ⊢ ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) +op 𝑈 ) = ( ( 𝑇 +op 𝑈 ) +op ( - 1 ·op 𝑈 ) )
11 1 2 9 hoaddassi ⊢ ( ( 𝑇 +op 𝑈 ) +op ( - 1 ·op 𝑈 ) ) = ( 𝑇 +op ( 𝑈 +op ( - 1 ·op 𝑈 ) ) )
12 2 2 honegsubi ⊢ ( 𝑈 +op ( - 1 ·op 𝑈 ) ) = ( 𝑈 −op 𝑈 )
13 2 hodidi ⊢ ( 𝑈 −op 𝑈 ) = 0hop
14 12 13 eqtri ⊢ ( 𝑈 +op ( - 1 ·op 𝑈 ) ) = 0hop
15 14 oveq2i ⊢ ( 𝑇 +op ( 𝑈 +op ( - 1 ·op 𝑈 ) ) ) = ( 𝑇 +op 0hop )
16 1 hoaddridi ⊢ ( 𝑇 +op 0hop ) = 𝑇
17 15 16 eqtri ⊢ ( 𝑇 +op ( 𝑈 +op ( - 1 ·op 𝑈 ) ) ) = 𝑇
18 11 17 eqtri ⊢ ( ( 𝑇 +op 𝑈 ) +op ( - 1 ·op 𝑈 ) ) = 𝑇
19 10 18 eqtri ⊢ ( ( 𝑇 +op ( - 1 ·op 𝑈 ) ) +op 𝑈 ) = 𝑇
20 ho0f ⊢ 0hop : ℋ ⟶ ℋ
21 20 2 hoaddcomi ⊢ ( 0hop +op 𝑈 ) = ( 𝑈 +op 0hop )
22 2 hoaddridi ⊢ ( 𝑈 +op 0hop ) = 𝑈
23 21 22 eqtri ⊢ ( 0hop +op 𝑈 ) = 𝑈
24 6 19 23 3eqtr3g ⊢ ( ( 𝑇 −op 𝑈 ) = 0hop → 𝑇 = 𝑈 )
25 oveq1 ⊢ ( 𝑇 = 𝑈 → ( 𝑇 −op 𝑈 ) = ( 𝑈 −op 𝑈 ) )
26 25 13 eqtrdi ⊢ ( 𝑇 = 𝑈 → ( 𝑇 −op 𝑈 ) = 0hop )
27 24 26 impbii ⊢ ( ( 𝑇 −op 𝑈 ) = 0hop ↔ 𝑇 = 𝑈 )