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 e. ~H /\ B e. ~H ) -> ( ( A .ih B ) e. RR <-> ( A .ih B ) = ( B .ih A ) ) )

Proof

Step Hyp Ref Expression
1 hicl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) e. CC )
2 cjreb 
 |-  ( ( A .ih B ) e. CC -> ( ( A .ih B ) e. RR <-> ( * ` ( A .ih B ) ) = ( A .ih B ) ) )
3 1 2 syl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) e. RR <-> ( * ` ( 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 e. ~H /\ B e. ~H ) -> ( ( A .ih B ) e. RR <-> ( A .ih B ) = ( * ` ( A .ih B ) ) ) )
6 ax-his1 
 |-  ( ( B e. ~H /\ A e. ~H ) -> ( B .ih A ) = ( * ` ( A .ih B ) ) )
7 6 ancoms 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( B .ih A ) = ( * ` ( A .ih B ) ) )
8 7 eqeq2d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = ( B .ih A ) <-> ( A .ih B ) = ( * ` ( A .ih B ) ) ) )
9 5 8 bitr4d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) e. RR <-> ( A .ih B ) = ( B .ih A ) ) )