Metamath Proof Explorer


Theorem hvnegdi

Description: Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

Ref Expression
Assertion hvnegdi ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( - 1 · ( 𝐴 𝐵 ) ) = ( 𝐵 𝐴 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( 𝐴 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) )
2 1 oveq2d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( - 1 · ( 𝐴 𝐵 ) ) = ( - 1 · ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) )
3 oveq2 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( 𝐵 𝐴 ) = ( 𝐵 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
4 2 3 eqeq12d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( - 1 · ( 𝐴 𝐵 ) ) = ( 𝐵 𝐴 ) ↔ ( - 1 · ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) = ( 𝐵 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) )
5 oveq2 ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
6 5 oveq2d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( - 1 · ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) = ( - 1 · ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) )
7 oveq1 ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( 𝐵 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) = ( if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) − if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
8 6 7 eqeq12d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( ( - 1 · ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) = ( 𝐵 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ↔ ( - 1 · ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) = ( if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) − if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) ) )
9 ifhvhv0 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ∈ ℋ
10 ifhvhv0 if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ∈ ℋ
11 9 10 hvnegdii ( - 1 · ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) = ( if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) − if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) )
12 4 8 11 dedth2h ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( - 1 · ( 𝐴 𝐵 ) ) = ( 𝐵 𝐴 ) )