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 : ~H --> ~H
hosd1.3 
|- U : ~H --> ~H
Assertion hosubeq0i 
|- ( ( T -op U ) = 0hop <-> T = U )

Proof

Step Hyp Ref Expression
1 hosd1.2 
 |-  T : ~H --> ~H
2 hosd1.3 
 |-  U : ~H --> ~H
3 1 2 honegsubi 
 |-  ( T +op ( -u 1 .op U ) ) = ( T -op U )
4 3 eqeq1i 
 |-  ( ( T +op ( -u 1 .op U ) ) = 0hop <-> ( T -op U ) = 0hop )
5 oveq1 
 |-  ( ( T +op ( -u 1 .op U ) ) = 0hop -> ( ( T +op ( -u 1 .op U ) ) +op U ) = ( 0hop +op U ) )
6 4 5 sylbir 
 |-  ( ( T -op U ) = 0hop -> ( ( T +op ( -u 1 .op U ) ) +op U ) = ( 0hop +op U ) )
7 neg1cn 
 |-  -u 1 e. CC
8 homulcl 
 |-  ( ( -u 1 e. CC /\ U : ~H --> ~H ) -> ( -u 1 .op U ) : ~H --> ~H )
9 7 2 8 mp2an 
 |-  ( -u 1 .op U ) : ~H --> ~H
10 1 9 2 hoadd32i 
 |-  ( ( T +op ( -u 1 .op U ) ) +op U ) = ( ( T +op U ) +op ( -u 1 .op U ) )
11 1 2 9 hoaddassi 
 |-  ( ( T +op U ) +op ( -u 1 .op U ) ) = ( T +op ( U +op ( -u 1 .op U ) ) )
12 2 2 honegsubi 
 |-  ( U +op ( -u 1 .op U ) ) = ( U -op U )
13 2 hodidi 
 |-  ( U -op U ) = 0hop
14 12 13 eqtri 
 |-  ( U +op ( -u 1 .op U ) ) = 0hop
15 14 oveq2i 
 |-  ( T +op ( U +op ( -u 1 .op U ) ) ) = ( T +op 0hop )
16 1 hoaddid1i 
 |-  ( T +op 0hop ) = T
17 15 16 eqtri 
 |-  ( T +op ( U +op ( -u 1 .op U ) ) ) = T
18 11 17 eqtri 
 |-  ( ( T +op U ) +op ( -u 1 .op U ) ) = T
19 10 18 eqtri 
 |-  ( ( T +op ( -u 1 .op U ) ) +op U ) = T
20 ho0f 
 |-  0hop : ~H --> ~H
21 20 2 hoaddcomi 
 |-  ( 0hop +op U ) = ( U +op 0hop )
22 2 hoaddid1i 
 |-  ( U +op 0hop ) = U
23 21 22 eqtri 
 |-  ( 0hop +op U ) = U
24 6 19 23 3eqtr3g 
 |-  ( ( T -op U ) = 0hop -> T = U )
25 oveq1 
 |-  ( T = U -> ( T -op U ) = ( U -op U ) )
26 25 13 eqtrdi 
 |-  ( T = U -> ( T -op U ) = 0hop )
27 24 26 impbii 
 |-  ( ( T -op U ) = 0hop <-> T = U )