Metamath Proof Explorer

Theorem hi2eq

Description: Lemma used to prove equality of vectors. (Contributed by NM, 16-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion hi2eq ⊢A∈ℋ∧B∈ℋ→A⋅ihA-ℎB=B⋅ihA-ℎB↔A=B

Proof

Step Hyp Ref Expression
1 hvsubcl ⊢A∈ℋ∧B∈ℋ→A-ℎB∈ℋ
2 his2sub ⊢A∈ℋ∧B∈ℋ∧A-ℎB∈ℋ→A-ℎB⋅ihA-ℎB=A⋅ihA-ℎB−B⋅ihA-ℎB
3 1 2 mpd3an3 ⊢A∈ℋ∧B∈ℋ→A-ℎB⋅ihA-ℎB=A⋅ihA-ℎB−B⋅ihA-ℎB
4 3 eqeq1d ⊢A∈ℋ∧B∈ℋ→A-ℎB⋅ihA-ℎB=0↔A⋅ihA-ℎB−B⋅ihA-ℎB=0
5 his6 ⊢A-ℎB∈ℋ→A-ℎB⋅ihA-ℎB=0↔A-ℎB=0ℎ
6 1 5 syl ⊢A∈ℋ∧B∈ℋ→A-ℎB⋅ihA-ℎB=0↔A-ℎB=0ℎ
7 4 6 bitr3d ⊢A∈ℋ∧B∈ℋ→A⋅ihA-ℎB−B⋅ihA-ℎB=0↔A-ℎB=0ℎ
8 hicl ⊢A∈ℋ∧A-ℎB∈ℋ→A⋅ihA-ℎB∈ℂ
9 1 8 syldan ⊢A∈ℋ∧B∈ℋ→A⋅ihA-ℎB∈ℂ
10 simpr ⊢A∈ℋ∧B∈ℋ→B∈ℋ
11 hicl ⊢B∈ℋ∧A-ℎB∈ℋ→B⋅ihA-ℎB∈ℂ
12 10 1 11 syl2anc ⊢A∈ℋ∧B∈ℋ→B⋅ihA-ℎB∈ℂ
13 9 12 subeq0ad ⊢A∈ℋ∧B∈ℋ→A⋅ihA-ℎB−B⋅ihA-ℎB=0↔A⋅ihA-ℎB=B⋅ihA-ℎB
14 hvsubeq0 ⊢A∈ℋ∧B∈ℋ→A-ℎB=0ℎ↔A=B
15 7 13 14 3bitr3d ⊢A∈ℋ∧B∈ℋ→A⋅ihA-ℎB=B⋅ihA-ℎB↔A=B