Theorem hial02

Description: A vector whose inner product is always zero is zero. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hial02	⊢ ( 𝐴 ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih 𝐴 ) = 0 ↔ 𝐴 = 0ℎ ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ·ih 𝐴 ) = ( 𝐴 ·ih 𝐴 ) )
2	1	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ·ih 𝐴 ) = 0 ↔ ( 𝐴 ·ih 𝐴 ) = 0 ) )
3	2	rspcv	⊢ ( 𝐴 ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih 𝐴 ) = 0 → ( 𝐴 ·ih 𝐴 ) = 0 ) )
4		his6	⊢ ( 𝐴 ∈ ℋ → ( ( 𝐴 ·ih 𝐴 ) = 0 ↔ 𝐴 = 0ℎ ) )
5	3 4	sylibd	⊢ ( 𝐴 ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih 𝐴 ) = 0 → 𝐴 = 0ℎ ) )
6		oveq2	⊢ ( 𝐴 = 0ℎ → ( 𝑥 ·ih 𝐴 ) = ( 𝑥 ·ih 0ℎ ) )
7		hi02	⊢ ( 𝑥 ∈ ℋ → ( 𝑥 ·ih 0ℎ ) = 0 )
8	6 7	sylan9eq	⊢ ( ( 𝐴 = 0ℎ ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·ih 𝐴 ) = 0 )
9	8	ex	⊢ ( 𝐴 = 0ℎ → ( 𝑥 ∈ ℋ → ( 𝑥 ·ih 𝐴 ) = 0 ) )
10	9	a1i	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 = 0ℎ → ( 𝑥 ∈ ℋ → ( 𝑥 ·ih 𝐴 ) = 0 ) ) )
11	10	ralrimdv	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 = 0ℎ → ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih 𝐴 ) = 0 ) )
12	5 11	impbid	⊢ ( 𝐴 ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih 𝐴 ) = 0 ↔ 𝐴 = 0ℎ ) )