# Metamath Proof Explorer

## Theorem his6

Description: Zero inner product with self means vector is zero. Lemma 3.1(S6) of Beran p. 95. (Contributed by NM, 27-Jul-1999) (New usage is discouraged.)

Ref Expression
Assertion his6 ${⊢}{A}\in ℋ\to \left({A}{\cdot }_{\mathrm{ih}}{A}=0↔{A}={0}_{ℎ}\right)$

### Proof

Step Hyp Ref Expression
1 ax-his4 ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0<{A}{\cdot }_{\mathrm{ih}}{A}$
2 1 gt0ne0d ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {A}{\cdot }_{\mathrm{ih}}{A}\ne 0$
3 2 ex ${⊢}{A}\in ℋ\to \left({A}\ne {0}_{ℎ}\to {A}{\cdot }_{\mathrm{ih}}{A}\ne 0\right)$
4 3 necon4d ${⊢}{A}\in ℋ\to \left({A}{\cdot }_{\mathrm{ih}}{A}=0\to {A}={0}_{ℎ}\right)$
5 hi01 ${⊢}{A}\in ℋ\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}=0$
6 oveq1 ${⊢}{A}={0}_{ℎ}\to {A}{\cdot }_{\mathrm{ih}}{A}={0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}$
7 6 eqeq1d ${⊢}{A}={0}_{ℎ}\to \left({A}{\cdot }_{\mathrm{ih}}{A}=0↔{0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}=0\right)$
8 5 7 syl5ibrcom ${⊢}{A}\in ℋ\to \left({A}={0}_{ℎ}\to {A}{\cdot }_{\mathrm{ih}}{A}=0\right)$
9 4 8 impbid ${⊢}{A}\in ℋ\to \left({A}{\cdot }_{\mathrm{ih}}{A}=0↔{A}={0}_{ℎ}\right)$