Theorem reipcl

Description: An inner product of an element with itself is real. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	reipcl.v	$$⊢V={\mathrm{Base}}_W$$
	reipcl.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
Assertion	reipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to A\underset{\dot{}}{,}A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		reipcl.v	$$⊢V={\mathrm{Base}}_W$$
2		reipcl.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		eqid	$$⊢\mathrm{norm}\left(W\right)=\mathrm{norm}\left(W\right)$$
4	1 2 3	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to {\mathrm{norm}\left(W\right)\left(A\right)}^2=A\underset{\dot{}}{,}A$$
5		cphngp	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{NrmGrp}$$
6	1 3	nmcl	$$⊢\left(W\in \mathrm{NrmGrp}\wedge A\in V\right)\to \mathrm{norm}\left(W\right)\left(A\right)\in ℝ$$
7	5 6	sylan	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to \mathrm{norm}\left(W\right)\left(A\right)\in ℝ$$
8	7	resqcld	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to {\mathrm{norm}\left(W\right)\left(A\right)}^2\in ℝ$$
9	4 8	eqeltrrd	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to A\underset{\dot{}}{,}A\in ℝ$$