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

Proof

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