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 ⊢A∈ℋ∧B∈ℋ→∀x∈ℋx⋅ihA=x⋅ihB↔A=B

Proof

Step Hyp Ref Expression
1 ax-his1 ⊢A∈ℋ∧x∈ℋ→A⋅ihx=x⋅ihA‾
2 ax-his1 ⊢B∈ℋ∧x∈ℋ→B⋅ihx=x⋅ihB‾
3 1 2 eqeqan12d ⊢A∈ℋ∧x∈ℋ∧B∈ℋ∧x∈ℋ→A⋅ihx=B⋅ihx↔x⋅ihA‾=x⋅ihB‾
4 hicl ⊢x∈ℋ∧A∈ℋ→x⋅ihA∈ℂ
5 4 ancoms ⊢A∈ℋ∧x∈ℋ→x⋅ihA∈ℂ
6 hicl ⊢x∈ℋ∧B∈ℋ→x⋅ihB∈ℂ
7 6 ancoms ⊢B∈ℋ∧x∈ℋ→x⋅ihB∈ℂ
8 cj11 ⊢x⋅ihA∈ℂ∧x⋅ihB∈ℂ→x⋅ihA‾=x⋅ihB‾↔x⋅ihA=x⋅ihB
9 5 7 8 syl2an ⊢A∈ℋ∧x∈ℋ∧B∈ℋ∧x∈ℋ→x⋅ihA‾=x⋅ihB‾↔x⋅ihA=x⋅ihB
10 3 9 bitr2d ⊢A∈ℋ∧x∈ℋ∧B∈ℋ∧x∈ℋ→x⋅ihA=x⋅ihB↔A⋅ihx=B⋅ihx
11 10 anandirs ⊢A∈ℋ∧B∈ℋ∧x∈ℋ→x⋅ihA=x⋅ihB↔A⋅ihx=B⋅ihx
12 11 ralbidva ⊢A∈ℋ∧B∈ℋ→∀x∈ℋx⋅ihA=x⋅ihB↔∀x∈ℋA⋅ihx=B⋅ihx
13 hial2eq ⊢A∈ℋ∧B∈ℋ→∀x∈ℋA⋅ihx=B⋅ihx↔A=B
14 12 13 bitrd ⊢A∈ℋ∧B∈ℋ→∀x∈ℋx⋅ihA=x⋅ihB↔A=B