# 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`
` |-  ( ( T +op ( -u 1 .op U ) ) +op U ) = ( ( T +op U ) +op ( -u 1 .op U ) )`
` |-  ( ( 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 )`
` |-  ( 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`
` |-  ( 0hop +op U ) = ( U +op 0hop )`
` |-  ( U +op 0hop ) = U`
` |-  ( 0hop +op U ) = U`
` |-  ( ( T -op U ) = 0hop -> T = U )`
` |-  ( T = U -> ( T -op U ) = ( U -op U ) )`
` |-  ( T = U -> ( T -op U ) = 0hop )`
` |-  ( ( T -op U ) = 0hop <-> T = U )`