Metamath Proof Explorer

Theorem hial2eq

Description: Two vectors whose inner product is always equal are equal. (Contributed by NM, 16-Nov-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hvsubcl ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B ∈ ℋ
2 oveq2 ⊢ x = A - ℎ B → A ⋅ ih x = A ⋅ ih A - ℎ B
3 oveq2 ⊢ x = A - ℎ B → B ⋅ ih x = B ⋅ ih A - ℎ B
4 2 3 eqeq12d ⊢ x = A - ℎ B → A ⋅ ih x = B ⋅ ih x ↔ A ⋅ ih A - ℎ B = B ⋅ ih A - ℎ B
5 4 rspcv ⊢ A - ℎ B ∈ ℋ → ∀ x ∈ ℋ A ⋅ ih x = B ⋅ ih x → A ⋅ ih A - ℎ B = B ⋅ ih A - ℎ B
6 1 5 syl ⊢ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ A ⋅ ih x = B ⋅ ih x → A ⋅ ih A - ℎ B = B ⋅ ih A - ℎ B
7 hi2eq ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih A - ℎ B = B ⋅ ih A - ℎ B ↔ A = B
8 6 7 sylibd ⊢ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ A ⋅ ih x = B ⋅ ih x → A = B
9 oveq1 ⊢ A = B → A ⋅ ih x = B ⋅ ih x
10 9 ralrimivw ⊢ A = B → ∀ x ∈ ℋ A ⋅ ih x = B ⋅ ih x
11 8 10 impbid1 ⊢ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ A ⋅ ih x = B ⋅ ih x ↔ A = B