Metamath Proof Explorer

Theorem honegsubdi2

Description: Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 honegsubdi 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T -op U ) ) = ( ( -u 1 .op T ) +op U ) )
2 neg1cn 
 |-  -u 1 e. CC
3 homulcl 
 |-  ( ( -u 1 e. CC /\ T : ~H --> ~H ) -> ( -u 1 .op T ) : ~H --> ~H )
4 2 3 mpan 
 |-  ( T : ~H --> ~H -> ( -u 1 .op T ) : ~H --> ~H )
5 hoaddcom 
 |-  ( ( ( -u 1 .op T ) : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( -u 1 .op T ) +op U ) = ( U +op ( -u 1 .op T ) ) )
6 4 5 sylan 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( -u 1 .op T ) +op U ) = ( U +op ( -u 1 .op T ) ) )
7 honegsub 
 |-  ( ( U : ~H --> ~H /\ T : ~H --> ~H ) -> ( U +op ( -u 1 .op T ) ) = ( U -op T ) )
8 7 ancoms 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( U +op ( -u 1 .op T ) ) = ( U -op T ) )
9 1 6 8 3eqtrd 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T -op U ) ) = ( U -op T ) )