Metamath Proof Explorer

Theorem abshicom

Description: Commuted inner products have the same absolute values. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

Ref Expression
Assertion abshicom ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = B ⋅ ih A

Proof

Step Hyp Ref Expression
1 ax-his1 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = B ⋅ ih A ‾
2 1 fveq2d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = B ⋅ ih A ‾
3 hicl ⊢ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A ∈ ℂ
4 3 ancoms ⊢ A ∈ ℋ ∧ B ∈ ℋ → B ⋅ ih A ∈ ℂ
5 4 abscjd ⊢ A ∈ ℋ ∧ B ∈ ℋ → B ⋅ ih A ‾ = B ⋅ ih A
6 2 5 eqtrd ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = B ⋅ ih A