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

Metamath Proof Explorer

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 ) )