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

Metamath Proof Explorer

Theorem hial0

Description: A vector whose inner product is always zero is zero. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐴 ·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 oveq1 ⊢ ( 𝐴 = 0ℎ → ( 𝐴 ·ih 𝑥 ) = ( 0ℎ ·ih 𝑥 ) )
7 hi01 ⊢ ( 𝑥 ∈ ℋ → ( 0ℎ ·ih 𝑥 ) = 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ℎ ) )