Metamath Proof Explorer


Theorem hiidrcl

Description: Real closure of inner product with self. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion hiidrcl
|- ( A e. ~H -> ( A .ih A ) e. RR )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( A .ih A ) = ( A .ih A )
2 hire
 |-  ( ( A e. ~H /\ A e. ~H ) -> ( ( A .ih A ) e. RR <-> ( A .ih A ) = ( A .ih A ) ) )
3 1 2 mpbiri
 |-  ( ( A e. ~H /\ A e. ~H ) -> ( A .ih A ) e. RR )
4 3 anidms
 |-  ( A e. ~H -> ( A .ih A ) e. RR )