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 = 0 vec U
hlipgt0.7 P = 𝑖OLD U
Assertion hlipgt0 U CHil OLD A X A Z 0 < A P A

Proof

Step Hyp Ref Expression
1 hlipgt0.1 X = BaseSet U
2 hlipgt0.5 Z = 0 vec U
3 hlipgt0.7 P = 𝑖OLD U
4 hlnv U CHil OLD U NrmCVec
5 eqid norm CV U = norm CV U
6 1 5 nvcl U NrmCVec A X norm CV U A
7 6 3adant3 U NrmCVec A X A Z norm CV U A
8 1 2 5 nvz U NrmCVec A X norm CV U A = 0 A = Z
9 8 biimpd U NrmCVec A X norm CV U A = 0 A = Z
10 9 necon3d U NrmCVec A X A Z norm CV U A 0
11 10 3impia U NrmCVec A X A Z norm CV U A 0
12 7 11 sqgt0d U NrmCVec A X A Z 0 < norm CV U A 2
13 1 5 3 ipidsq U NrmCVec A X A P A = norm CV U A 2
14 13 3adant3 U NrmCVec A X A Z A P A = norm CV U A 2
15 12 14 breqtrrd U NrmCVec A X A Z 0 < A P A
16 4 15 syl3an1 U CHil OLD A X A Z 0 < A P A