Metamath Proof Explorer

Theorem hvsubadd

Description: Relationship between vector subtraction and addition. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion hvsubadd ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB=C↔B+ℎC=A

Proof

Step Hyp Ref Expression
1 oveq1 ⊢A=ifA∈ℋA0ℎ→A-ℎB=ifA∈ℋA0ℎ-ℎB
2 1 eqeq1d ⊢A=ifA∈ℋA0ℎ→A-ℎB=C↔ifA∈ℋA0ℎ-ℎB=C
3 eqeq2 ⊢A=ifA∈ℋA0ℎ→B+ℎC=A↔B+ℎC=ifA∈ℋA0ℎ
4 2 3 bibi12d ⊢A=ifA∈ℋA0ℎ→A-ℎB=C↔B+ℎC=A↔ifA∈ℋA0ℎ-ℎB=C↔B+ℎC=ifA∈ℋA0ℎ
5 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB=ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
6 5 eqeq1d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB=C↔ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=C
7 oveq1 ⊢B=ifB∈ℋB0ℎ→B+ℎC=ifB∈ℋB0ℎ+ℎC
8 7 eqeq1d ⊢B=ifB∈ℋB0ℎ→B+ℎC=ifA∈ℋA0ℎ↔ifB∈ℋB0ℎ+ℎC=ifA∈ℋA0ℎ
9 6 8 bibi12d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB=C↔B+ℎC=ifA∈ℋA0ℎ↔ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=C↔ifB∈ℋB0ℎ+ℎC=ifA∈ℋA0ℎ
10 eqeq2 ⊢C=ifC∈ℋC0ℎ→ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=C↔ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=ifC∈ℋC0ℎ
11 oveq2 ⊢C=ifC∈ℋC0ℎ→ifB∈ℋB0ℎ+ℎC=ifB∈ℋB0ℎ+ℎifC∈ℋC0ℎ
12 11 eqeq1d ⊢C=ifC∈ℋC0ℎ→ifB∈ℋB0ℎ+ℎC=ifA∈ℋA0ℎ↔ifB∈ℋB0ℎ+ℎifC∈ℋC0ℎ=ifA∈ℋA0ℎ
13 10 12 bibi12d ⊢C=ifC∈ℋC0ℎ→ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=C↔ifB∈ℋB0ℎ+ℎC=ifA∈ℋA0ℎ↔ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=ifC∈ℋC0ℎ↔ifB∈ℋB0ℎ+ℎifC∈ℋC0ℎ=ifA∈ℋA0ℎ
14 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
15 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
16 ifhvhv0 ⊢ifC∈ℋC0ℎ∈ℋ
17 14 15 16 hvsubaddi ⊢ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ=ifC∈ℋC0ℎ↔ifB∈ℋB0ℎ+ℎifC∈ℋC0ℎ=ifA∈ℋA0ℎ
18 4 9 13 17 dedth3h ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB=C↔B+ℎC=A