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	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·_ih 𝐴 ) = ( 𝑥 ·_ih 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-his1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝐴 ·_ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·_ih 𝐴 ) ) )
2		ax-his1	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝐵 ·_ih 𝑥 ) = ( ∗ ‘ ( 𝑥 ·_ih 𝐵 ) ) )
3	1 2	eqeqan12d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( 𝐴 ·_ih 𝑥 ) = ( 𝐵 ·_ih 𝑥 ) ↔ ( ∗ ‘ ( 𝑥 ·_ih 𝐴 ) ) = ( ∗ ‘ ( 𝑥 ·_ih 𝐵 ) ) ) )
4		hicl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝑥 ·_ih 𝐴 ) ∈ ℂ )
5	4	ancoms	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·_ih 𝐴 ) ∈ ℂ )
6		hicl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑥 ·_ih 𝐵 ) ∈ ℂ )
7	6	ancoms	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·_ih 𝐵 ) ∈ ℂ )
8		cj11	⊢ ( ( ( 𝑥 ·_ih 𝐴 ) ∈ ℂ ∧ ( 𝑥 ·_ih 𝐵 ) ∈ ℂ ) → ( ( ∗ ‘ ( 𝑥 ·_ih 𝐴 ) ) = ( ∗ ‘ ( 𝑥 ·_ih 𝐵 ) ) ↔ ( 𝑥 ·_ih 𝐴 ) = ( 𝑥 ·_ih 𝐵 ) ) )
9	5 7 8	syl2an	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( ∗ ‘ ( 𝑥 ·_ih 𝐴 ) ) = ( ∗ ‘ ( 𝑥 ·_ih 𝐵 ) ) ↔ ( 𝑥 ·_ih 𝐴 ) = ( 𝑥 ·_ih 𝐵 ) ) )
10	3 9	bitr2d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) ∧ ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( ( 𝑥 ·_ih 𝐴 ) = ( 𝑥 ·_ih 𝐵 ) ↔ ( 𝐴 ·_ih 𝑥 ) = ( 𝐵 ·_ih 𝑥 ) ) )
11	10	anandirs	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·_ih 𝐴 ) = ( 𝑥 ·_ih 𝐵 ) ↔ ( 𝐴 ·_ih 𝑥 ) = ( 𝐵 ·_ih 𝑥 ) ) )
12	11	ralbidva	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·_ih 𝐴 ) = ( 𝑥 ·_ih 𝐵 ) ↔ ∀ 𝑥 ∈ ℋ ( 𝐴 ·_ih 𝑥 ) = ( 𝐵 ·_ih 𝑥 ) ) )
13		hial2eq	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝐴 ·_ih 𝑥 ) = ( 𝐵 ·_ih 𝑥 ) ↔ 𝐴 = 𝐵 ) )
14	12 13	bitrd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·_ih 𝐴 ) = ( 𝑥 ·_ih 𝐵 ) ↔ 𝐴 = 𝐵 ) )