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 𝑥 ) ↔ 𝐴 = 𝐵 ) )