Metamath Proof Explorer

Theorem honegsubdi

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

Ref Expression
Assertion honegsubdi 
|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T -op U ) ) = ( ( -u 1 .op 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 honegdi 
 |-  ( ( T : ~H --> ~H /\ ( -u 1 .op U ) : ~H --> ~H ) -> ( -u 1 .op ( T +op ( -u 1 .op U ) ) ) = ( ( -u 1 .op T ) +op ( -u 1 .op ( -u 1 .op U ) ) ) )
5 3 4 sylan2 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T +op ( -u 1 .op U ) ) ) = ( ( -u 1 .op T ) +op ( -u 1 .op ( -u 1 .op U ) ) ) )
6 honegsub 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( -u 1 .op U ) ) = ( T -op U ) )
7 6 oveq2d 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T +op ( -u 1 .op U ) ) ) = ( -u 1 .op ( T -op U ) ) )
8 honegneg 
 |-  ( U : ~H --> ~H -> ( -u 1 .op ( -u 1 .op U ) ) = U )
9 8 adantl 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( -u 1 .op U ) ) = U )
10 9 oveq2d 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( -u 1 .op T ) +op ( -u 1 .op ( -u 1 .op U ) ) ) = ( ( -u 1 .op T ) +op U ) )
11 5 7 10 3eqtr3d 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( -u 1 .op ( T -op U ) ) = ( ( -u 1 .op T ) +op U ) )