Metamath Proof Explorer

Theorem hvaddcan

Description: Cancellation law for vector addition. (Contributed by NM, 18-May-2005) (New usage is discouraged.)

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

Proof

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