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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	hlipgt0.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
	hlipgt0.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
Assertion	hlipgt0	⊢ ( ( 𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍 ) → 0 < ( 𝐴 𝑃 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		hlipgt0.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		hlipgt0.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3		hlipgt0.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
4		hlnv	⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec )
5		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
6	1 5	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℝ )
7	6	3adant3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ∈ ℝ )
8	1 2 5	nvz	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) = 0 ↔ 𝐴 = 𝑍 ) )
9	8	biimpd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) = 0 → 𝐴 = 𝑍 ) )
10	9	necon3d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ 𝑍 → ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ≠ 0 ) )
11	10	3impia	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ≠ 0 )
12	7 11	sqgt0d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍 ) → 0 < ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ↑ 2 ) )
13	1 5 3	ipidsq	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐴 ) = ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ↑ 2 ) )
14	13	3adant3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍 ) → ( 𝐴 𝑃 𝐴 ) = ( ( ( normCV ‘ 𝑈 ) ‘ 𝐴 ) ↑ 2 ) )
15	12 14	breqtrrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍 ) → 0 < ( 𝐴 𝑃 𝐴 ) )
16	4 15	syl3an1	⊢ ( ( 𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍 ) → 0 < ( 𝐴 𝑃 𝐴 ) )