# Metamath Proof Explorer

## Theorem hial2eq2

Description: Two vectors whose inner product is always equal are equal. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 ax-his1 ${⊢}\left({A}\in ℋ\wedge {x}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{x}=\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{A}}$
2 ax-his1 ${⊢}\left({B}\in ℋ\wedge {x}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{x}=\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{B}}$
3 1 2 eqeqan12d ${⊢}\left(\left({A}\in ℋ\wedge {x}\in ℋ\right)\wedge \left({B}\in ℋ\wedge {x}\in ℋ\right)\right)\to \left({A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}↔\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{A}}=\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{B}}\right)$
4 hicl ${⊢}\left({x}\in ℋ\wedge {A}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
5 4 ancoms ${⊢}\left({A}\in ℋ\wedge {x}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
6 hicl ${⊢}\left({x}\in ℋ\wedge {B}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
7 6 ancoms ${⊢}\left({B}\in ℋ\wedge {x}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{B}\in ℂ$
8 cj11 ${⊢}\left({x}{\cdot }_{\mathrm{ih}}{A}\in ℂ\wedge {x}{\cdot }_{\mathrm{ih}}{B}\in ℂ\right)\to \left(\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{A}}=\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{B}}↔{x}{\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{B}\right)$
9 5 7 8 syl2an ${⊢}\left(\left({A}\in ℋ\wedge {x}\in ℋ\right)\wedge \left({B}\in ℋ\wedge {x}\in ℋ\right)\right)\to \left(\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{A}}=\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{B}}↔{x}{\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{B}\right)$
10 3 9 bitr2d ${⊢}\left(\left({A}\in ℋ\wedge {x}\in ℋ\right)\wedge \left({B}\in ℋ\wedge {x}\in ℋ\right)\right)\to \left({x}{\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{B}↔{A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}\right)$
11 10 anandirs ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge {x}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{B}↔{A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}\right)$
12 11 ralbidva ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{B}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{\mathrm{ih}}{x}={B}{\cdot }_{\mathrm{ih}}{x}\right)$
13 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)$
14 12 13 bitrd ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{A}={x}{\cdot }_{\mathrm{ih}}{B}↔{A}={B}\right)$