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 hoaddid1i ( 𝑇 +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 hoaddid1i ( 𝑈 +op 0hop ) = 𝑈
23 21 22 eqtri ( 0hop +op 𝑈 ) = 𝑈
24 6 19 23 3eqtr3g ( ( 𝑇op 𝑈 ) = 0hop𝑇 = 𝑈 )
25 oveq1 ( 𝑇 = 𝑈 → ( 𝑇op 𝑈 ) = ( 𝑈op 𝑈 ) )
26 25 13 syl6eq ( 𝑇 = 𝑈 → ( 𝑇op 𝑈 ) = 0hop )
27 24 26 impbii ( ( 𝑇op 𝑈 ) = 0hop𝑇 = 𝑈 )