# Metamath Proof Explorer

## Theorem hial2eq

Description: Two vectors whose inner product is always equal are equal. (Contributed by NM, 16-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion hial2eq ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}↔{A}={B}\right)$

### Proof

Step Hyp Ref Expression
1 hvsubcl ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{-}_{ℎ}{B}\in ℋ$
2 oveq2 ${⊢}{x}={A}{-}_{ℎ}{B}\to {A}{\cdot }_{\mathrm{ih}}{x}={A}{\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)$
3 oveq2 ${⊢}{x}={A}{-}_{ℎ}{B}\to {B}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)$
4 2 3 eqeq12d ${⊢}{x}={A}{-}_{ℎ}{B}\to \left({A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}↔{A}{\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)={B}{\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)$
5 4 rspcv ${⊢}{A}{-}_{ℎ}{B}\in ℋ\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}\to {A}{\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)={B}{\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)$
6 1 5 syl ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}\to {A}{\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)={B}{\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)\right)$
7 hi2eq ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)={B}{\cdot }_{\mathrm{ih}}\left({A}{-}_{ℎ}{B}\right)↔{A}={B}\right)$
8 6 7 sylibd ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}\to {A}={B}\right)$
9 oveq1 ${⊢}{A}={B}\to {A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}$
10 9 ralrimivw ${⊢}{A}={B}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}$
11 8 10 impbid1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}↔{A}={B}\right)$