Metamath Proof Explorer

Theorem hi2eq

Description: Lemma used to prove equality of vectors. (Contributed by NM, 16-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion hi2eq ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih A - ℎ B = B ⋅ ih A - ℎ B ↔ A = B

Proof

Step Hyp Ref Expression
1 hvsubcl ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B ∈ ℋ
2 his2sub ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ A - ℎ B ∈ ℋ → A - ℎ B ⋅ ih A - ℎ B = A ⋅ ih A - ℎ B − B ⋅ ih A - ℎ B
3 1 2 mpd3an3 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B ⋅ ih A - ℎ B = A ⋅ ih A - ℎ B − B ⋅ ih A - ℎ B
4 3 eqeq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B ⋅ ih A - ℎ B = 0 ↔ A ⋅ ih A - ℎ B − B ⋅ ih A - ℎ B = 0
5 his6 ⊢ A - ℎ B ∈ ℋ → A - ℎ B ⋅ ih A - ℎ B = 0 ↔ A - ℎ B = 0 ℎ
6 1 5 syl ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B ⋅ ih A - ℎ B = 0 ↔ A - ℎ B = 0 ℎ
7 4 6 bitr3d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih A - ℎ B − B ⋅ ih A - ℎ B = 0 ↔ A - ℎ B = 0 ℎ
8 hicl ⊢ A ∈ ℋ ∧ A - ℎ B ∈ ℋ → A ⋅ ih A - ℎ B ∈ ℂ
9 1 8 syldan ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih A - ℎ B ∈ ℂ
10 simpr ⊢ A ∈ ℋ ∧ B ∈ ℋ → B ∈ ℋ
11 hicl ⊢ B ∈ ℋ ∧ A - ℎ B ∈ ℋ → B ⋅ ih A - ℎ B ∈ ℂ
12 10 1 11 syl2anc ⊢ A ∈ ℋ ∧ B ∈ ℋ → B ⋅ ih A - ℎ B ∈ ℂ
13 9 12 subeq0ad ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih A - ℎ B − B ⋅ ih A - ℎ B = 0 ↔ A ⋅ ih A - ℎ B = B ⋅ ih A - ℎ B
14 hvsubeq0 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B = 0 ℎ ↔ A = B
15 7 13 14 3bitr3d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih A - ℎ B = B ⋅ ih A - ℎ B ↔ A = B