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 = ( Base ` W )
	reipcl.h	|- ., = ( .i ` W )
Assertion	reipcl	|- ( ( W e. CPreHil /\ A e. V ) -> ( A ., A ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		reipcl.v	|- V = ( Base ` W )
2		reipcl.h	|- ., = ( .i ` W )
3		eqid	|- ( norm ` W ) = ( norm ` W )
4	1 2 3	nmsq	|- ( ( W e. CPreHil /\ A e. V ) -> ( ( ( norm ` W ) ` A ) ^ 2 ) = ( A ., A ) )
5		cphngp	|- ( W e. CPreHil -> W e. NrmGrp )
6	1 3	nmcl	|- ( ( W e. NrmGrp /\ A e. V ) -> ( ( norm ` W ) ` A ) e. RR )
7	5 6	sylan	|- ( ( W e. CPreHil /\ A e. V ) -> ( ( norm ` W ) ` A ) e. RR )
8	7	resqcld	|- ( ( W e. CPreHil /\ A e. V ) -> ( ( ( norm ` W ) ` A ) ^ 2 ) e. RR )
9	4 8	eqeltrrd	|- ( ( W e. CPreHil /\ A e. V ) -> ( A ., A ) e. RR )