This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )