# 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}\in ℋ\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}=0↔{A}={0}_{ℎ}\right)$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{x}={A}\to {A}{\cdot }_{\mathrm{ih}}{x}={A}{\cdot }_{\mathrm{ih}}{A}$
2 1 eqeq1d ${⊢}{x}={A}\to \left({A}{\cdot }_{\mathrm{ih}}{x}=0↔{A}{\cdot }_{\mathrm{ih}}{A}=0\right)$
3 2 rspcv ${⊢}{A}\in ℋ\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}=0\to {A}{\cdot }_{\mathrm{ih}}{A}=0\right)$
4 his6 ${⊢}{A}\in ℋ\to \left({A}{\cdot }_{\mathrm{ih}}{A}=0↔{A}={0}_{ℎ}\right)$
5 3 4 sylibd ${⊢}{A}\in ℋ\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}=0\to {A}={0}_{ℎ}\right)$
6 oveq1 ${⊢}{A}={0}_{ℎ}\to {A}{\cdot }_{\mathrm{ih}}{x}={0}_{ℎ}{\cdot }_{\mathrm{ih}}{x}$
7 hi01 ${⊢}{x}\in ℋ\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{x}=0$
8 6 7 sylan9eq ${⊢}\left({A}={0}_{ℎ}\wedge {x}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{x}=0$
9 8 ex ${⊢}{A}={0}_{ℎ}\to \left({x}\in ℋ\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)$
10 9 a1i ${⊢}{A}\in ℋ\to \left({A}={0}_{ℎ}\to \left({x}\in ℋ\to {A}{\cdot }_{\mathrm{ih}}{x}=0\right)\right)$
11 10 ralrimdv ${⊢}{A}\in ℋ\to \left({A}={0}_{ℎ}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}=0\right)$
12 5 11 impbid ${⊢}{A}\in ℋ\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}=0↔{A}={0}_{ℎ}\right)$