Metamath Proof Explorer

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 ⊢ A ∈ ℋ → ∀ x ∈ ℋ x ⋅ ih A = 0 ↔ A = 0 ℎ

Proof

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