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 syl6eq
 |-  ( T = U -> ( T -op U ) = 0hop )
27 24 26 impbii
 |-  ( ( T -op U ) = 0hop <-> T = U )