This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝐴 ·ih 𝑥 ) = ( 𝐵 ·ih 𝑥 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 hvsubcl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) ∈ ℋ )
2 oveq2 ⊢ ( 𝑥 = ( 𝐴 −ℎ 𝐵 ) → ( 𝐴 ·ih 𝑥 ) = ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) )
3 oveq2 ⊢ ( 𝑥 = ( 𝐴 −ℎ 𝐵 ) → ( 𝐵 ·ih 𝑥 ) = ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) )
4 2 3 eqeq12d ⊢ ( 𝑥 = ( 𝐴 −ℎ 𝐵 ) → ( ( 𝐴 ·ih 𝑥 ) = ( 𝐵 ·ih 𝑥 ) ↔ ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) = ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ) )
5 4 rspcv ⊢ ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( 𝐴 ·ih 𝑥 ) = ( 𝐵 ·ih 𝑥 ) → ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) = ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ) )
6 1 5 syl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝐴 ·ih 𝑥 ) = ( 𝐵 ·ih 𝑥 ) → ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) = ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ) )
7 hi2eq ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) = ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )
8 6 7 sylibd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝐴 ·ih 𝑥 ) = ( 𝐵 ·ih 𝑥 ) → 𝐴 = 𝐵 ) )
9 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ·ih 𝑥 ) = ( 𝐵 ·ih 𝑥 ) )
10 9 ralrimivw ⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 ∈ ℋ ( 𝐴 ·ih 𝑥 ) = ( 𝐵 ·ih 𝑥 ) )
11 8 10 impbid1 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝐴 ·ih 𝑥 ) = ( 𝐵 ·ih 𝑥 ) ↔ 𝐴 = 𝐵 ) )