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⋅ihB∈ℝ↔A⋅ihB=B⋅ihA

Proof

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