Theorem hlipgt0

Description: The inner product of a Hilbert space vector by itself is positive. (Contributed by NM, 8-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hlipgt0.1	|- X = ( BaseSet ` U )
	hlipgt0.5	|- Z = ( 0vec ` U )
	hlipgt0.7	|- P = ( .iOLD ` U )
Assertion	hlipgt0	|- ( ( U e. CHilOLD /\ A e. X /\ A =/= Z ) -> 0 < ( A P A ) )

Proof

Step	Hyp	Ref	Expression
1		hlipgt0.1	|- X = ( BaseSet ` U )
2		hlipgt0.5	|- Z = ( 0vec ` U )
3		hlipgt0.7	|- P = ( .iOLD ` U )
4		hlnv	|- ( U e. CHilOLD -> U e. NrmCVec )
5		eqid	|- ( normCV ` U ) = ( normCV ` U )
6	1 5	nvcl	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( normCV ` U ) ` A ) e. RR )
7	6	3adant3	|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( ( normCV ` U ) ` A ) e. RR )
8	1 2 5	nvz	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( normCV ` U ) ` A ) = 0 <-> A = Z ) )
9	8	biimpd	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( normCV ` U ) ` A ) = 0 -> A = Z ) )
10	9	necon3d	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A =/= Z -> ( ( normCV ` U ) ` A ) =/= 0 ) )
11	10	3impia	|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( ( normCV ` U ) ` A ) =/= 0 )
12	7 11	sqgt0d	|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> 0 < ( ( ( normCV ` U ) ` A ) ^ 2 ) )
13	1 5 3	ipidsq	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A P A ) = ( ( ( normCV ` U ) ` A ) ^ 2 ) )
14	13	3adant3	|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> ( A P A ) = ( ( ( normCV ` U ) ` A ) ^ 2 ) )
15	12 14	breqtrrd	|- ( ( U e. NrmCVec /\ A e. X /\ A =/= Z ) -> 0 < ( A P A ) )
16	4 15	syl3an1	|- ( ( U e. CHilOLD /\ A e. X /\ A =/= Z ) -> 0 < ( A P A ) )