Metamath Proof Explorer

Theorem hosubneg

Description: Relationship between operator subtraction and negative. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hosubneg 
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T -op ( -u 1 .op U ) ) = ( T +op U ) )

Proof

Step Hyp Ref Expression
1 neg1cn 
 |-  -u 1 e. CC
2 homulcl 
 |-  ( ( -u 1 e. CC /\ U : ~H --> ~H ) -> ( -u 1 .op U ) : ~H --> ~H )
3 1 2 mpan 
 |-  ( U : ~H --> ~H -> ( -u 1 .op U ) : ~H --> ~H )
4 honegsub 
 |-  ( ( T : ~H --> ~H /\ ( -u 1 .op U ) : ~H --> ~H ) -> ( T +op ( -u 1 .op ( -u 1 .op U ) ) ) = ( T -op ( -u 1 .op U ) ) )
5 3 4 sylan2 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( -u 1 .op ( -u 1 .op U ) ) ) = ( T -op ( -u 1 .op U ) ) )
6 honegneg 
 |-  ( U : ~H --> ~H -> ( -u 1 .op ( -u 1 .op U ) ) = U )
7 6 oveq2d 
 |-  ( U : ~H --> ~H -> ( T +op ( -u 1 .op ( -u 1 .op U ) ) ) = ( T +op U ) )
8 7 adantl 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( -u 1 .op ( -u 1 .op U ) ) ) = ( T +op U ) )
9 5 8 eqtr3d 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T -op ( -u 1 .op U ) ) = ( T +op U ) )