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\in \mathscr{H}\to A{\cdot }_{\mathrm{ih}}A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A{\cdot }_{\mathrm{ih}}A=A{\cdot }_{\mathrm{ih}}A$$
2		hire	$$⊢\left(A\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to \left(A{\cdot }_{\mathrm{ih}}A\in ℝ\leftrightarrow A{\cdot }_{\mathrm{ih}}A=A{\cdot }_{\mathrm{ih}}A\right)$$
3	1 2	mpbiri	$$⊢\left(A\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}A\in ℝ$$
4	3	anidms	$$⊢A\in \mathscr{H}\to A{\cdot }_{\mathrm{ih}}A\in ℝ$$