Theorem ipge0

Description: The inner product in a subcomplex pre-Hilbert space is positive definite. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	reipcl.v	|- V = ( Base ` W )
	reipcl.h	|- ., = ( .i ` W )
Assertion	ipge0	|- ( ( W e. CPreHil /\ A e. V ) -> 0 <_ ( A ., A ) )

Proof

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