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 ⊢A∈ℋ∧B∈ℋ→-1⋅ℎA-ℎB=B-ℎA

Proof

Step Hyp Ref Expression
1 oveq1 ⊢A=ifA∈ℋA0ℎ→A-ℎB=ifA∈ℋA0ℎ-ℎB
2 1 oveq2d ⊢A=ifA∈ℋA0ℎ→-1⋅ℎA-ℎB=-1⋅ℎifA∈ℋA0ℎ-ℎB
3 oveq2 ⊢A=ifA∈ℋA0ℎ→B-ℎA=B-ℎifA∈ℋA0ℎ
4 2 3 eqeq12d ⊢A=ifA∈ℋA0ℎ→-1⋅ℎA-ℎB=B-ℎA↔-1⋅ℎifA∈ℋA0ℎ-ℎB=B-ℎifA∈ℋA0ℎ
5 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB=ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
6 5 oveq2d ⊢B=ifB∈ℋB0ℎ→-1⋅ℎifA∈ℋA0ℎ-ℎB=-1⋅ℎifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
7 oveq1 ⊢B=ifB∈ℋB0ℎ→B-ℎifA∈ℋA0ℎ=ifB∈ℋB0ℎ-ℎifA∈ℋA0ℎ
8 6 7 eqeq12d ⊢B=ifB∈ℋB0ℎ→-1⋅ℎifA∈ℋA0ℎ-ℎB=B-ℎifA∈ℋA0ℎ↔-1⋅ℎifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=ifB∈ℋB0ℎ-ℎifA∈ℋA0ℎ
9 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
10 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
11 9 10 hvnegdii ⊢-1⋅ℎifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=ifB∈ℋB0ℎ-ℎifA∈ℋA0ℎ
12 4 8 11 dedth2h ⊢A∈ℋ∧B∈ℋ→-1⋅ℎA-ℎB=B-ℎA