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

Proof

Step Hyp Ref Expression
1 hvsubcl ⊢A∈ℋ∧B∈ℋ→A-ℎB∈ℋ
2 oveq2 ⊢x=A-ℎB→A⋅ihx=A⋅ihA-ℎB
3 oveq2 ⊢x=A-ℎB→B⋅ihx=B⋅ihA-ℎB
4 2 3 eqeq12d ⊢x=A-ℎB→A⋅ihx=B⋅ihx↔A⋅ihA-ℎB=B⋅ihA-ℎB
5 4 rspcv ⊢A-ℎB∈ℋ→∀x∈ℋA⋅ihx=B⋅ihx→A⋅ihA-ℎB=B⋅ihA-ℎB
6 1 5 syl ⊢A∈ℋ∧B∈ℋ→∀x∈ℋA⋅ihx=B⋅ihx→A⋅ihA-ℎB=B⋅ihA-ℎB
7 hi2eq ⊢A∈ℋ∧B∈ℋ→A⋅ihA-ℎB=B⋅ihA-ℎB↔A=B
8 6 7 sylibd ⊢A∈ℋ∧B∈ℋ→∀x∈ℋA⋅ihx=B⋅ihx→A=B
9 oveq1 ⊢A=B→A⋅ihx=B⋅ihx
10 9 ralrimivw ⊢A=B→∀x∈ℋA⋅ihx=B⋅ihx
11 8 10 impbid1 ⊢A∈ℋ∧B∈ℋ→∀x∈ℋA⋅ihx=B⋅ihx↔A=B