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 )