Metamath Proof Explorer

Theorem hial2eq2

Description: Two vectors whose inner product is always equal are equal. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion hial2eq2 ⊢ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ x ⋅ ih A = x ⋅ ih B ↔ A = B

Proof

Step Hyp Ref Expression
1 ax-his1 ⊢ A ∈ ℋ ∧ x ∈ ℋ → A ⋅ ih x = x ⋅ ih A ‾
2 ax-his1 ⊢ B ∈ ℋ ∧ x ∈ ℋ → B ⋅ ih x = x ⋅ ih B ‾
3 1 2 eqeqan12d ⊢ A ∈ ℋ ∧ x ∈ ℋ ∧ B ∈ ℋ ∧ x ∈ ℋ → A ⋅ ih x = B ⋅ ih x ↔ x ⋅ ih A ‾ = x ⋅ ih B ‾
4 hicl ⊢ x ∈ ℋ ∧ A ∈ ℋ → x ⋅ ih A ∈ ℂ
5 4 ancoms ⊢ A ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih A ∈ ℂ
6 hicl ⊢ x ∈ ℋ ∧ B ∈ ℋ → x ⋅ ih B ∈ ℂ
7 6 ancoms ⊢ B ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih B ∈ ℂ
8 cj11 ⊢ x ⋅ ih A ∈ ℂ ∧ x ⋅ ih B ∈ ℂ → x ⋅ ih A ‾ = x ⋅ ih B ‾ ↔ x ⋅ ih A = x ⋅ ih B
9 5 7 8 syl2an ⊢ A ∈ ℋ ∧ x ∈ ℋ ∧ B ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih A ‾ = x ⋅ ih B ‾ ↔ x ⋅ ih A = x ⋅ ih B
10 3 9 bitr2d ⊢ A ∈ ℋ ∧ x ∈ ℋ ∧ B ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih A = x ⋅ ih B ↔ A ⋅ ih x = B ⋅ ih x
11 10 anandirs ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ x ∈ ℋ → x ⋅ ih A = x ⋅ ih B ↔ A ⋅ ih x = B ⋅ ih x
12 11 ralbidva ⊢ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ x ⋅ ih A = x ⋅ ih B ↔ ∀ x ∈ ℋ A ⋅ ih x = B ⋅ ih x
13 hial2eq ⊢ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ A ⋅ ih x = B ⋅ ih x ↔ A = B
14 12 13 bitrd ⊢ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ x ⋅ ih A = x ⋅ ih B ↔ A = B