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

### Proof

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