Metamath Proof Explorer

Theorem hire

Description: A necessary and sufficient condition for an inner product to be real. (Contributed by NM, 2-Jul-2005) (New usage is discouraged.)

Ref Expression
Assertion hire ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ∈ ℝ ↔ A ⋅ ih B = B ⋅ ih A

Proof

Step Hyp Ref Expression
1 hicl ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ∈ ℂ
2 cjreb ⊢ A ⋅ ih B ∈ ℂ → A ⋅ ih B ∈ ℝ ↔ A ⋅ ih B ‾ = A ⋅ ih B
3 1 2 syl ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ∈ ℝ ↔ A ⋅ ih B ‾ = A ⋅ ih B
4 eqcom ⊢ A ⋅ ih B ‾ = A ⋅ ih B ↔ A ⋅ ih B = A ⋅ ih B ‾
5 3 4 bitrdi ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ∈ ℝ ↔ A ⋅ ih B = A ⋅ ih B ‾
6 ax-his1 ⊢ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A = A ⋅ ih B ‾
7 6 ancoms ⊢ A ∈ ℋ ∧ B ∈ ℋ → B ⋅ ih A = A ⋅ ih B ‾
8 7 eqeq2d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = B ⋅ ih A ↔ A ⋅ ih B = A ⋅ ih B ‾
9 5 8 bitr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B ∈ ℝ ↔ A ⋅ ih B = B ⋅ ih A