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 = \cdot_{𝑖OLD} (U)$
Assertion	hlipgt0	$⊢ (U \in {CHil}_{OLD} \land A \in X \land A \neq Z) \to 0 < A P A$

Step	Hyp	Ref	Expression
1		hlipgt0.1	$⊢ X = BaseSet (U)$
2		hlipgt0.5	$⊢ Z = 0_{vec} (U)$
3		hlipgt0.7	$⊢ P = \cdot_{𝑖OLD} (U)$
4		hlnv	$⊢ U \in {CHil}_{OLD} \to U \in NrmCVec$
5		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
6	1 5	nvcl	$⊢ (U \in NrmCVec \land A \in X) \to {norm}_{CV} (U) (A) \in ℝ$
7	6	3adant3	$⊢ (U \in NrmCVec \land A \in X \land A \neq Z) \to {norm}_{CV} (U) (A) \in ℝ$
8	1 2 5	nvz	$⊢ (U \in NrmCVec \land A \in X) \to ({norm}_{CV} (U) (A) = 0 \leftrightarrow A = Z)$
9	8	biimpd	$⊢ (U \in NrmCVec \land A \in X) \to ({norm}_{CV} (U) (A) = 0 \to A = Z)$
10	9	necon3d	$⊢ (U \in NrmCVec \land A \in X) \to (A \neq Z \to {norm}_{CV} (U) (A) \neq 0)$
11	10	3impia	$⊢ (U \in NrmCVec \land A \in X \land A \neq Z) \to {norm}_{CV} (U) (A) \neq 0$
12	7 11	sqgt0d	$⊢ (U \in NrmCVec \land A \in X \land A \neq Z) \to 0 < {{norm}_{CV} (U) (A)}^{2}$
13	1 5 3	ipidsq	$⊢ (U \in NrmCVec \land A \in X) \to A P A = {{norm}_{CV} (U) (A)}^{2}$
14	13	3adant3	$⊢ (U \in NrmCVec \land A \in X \land A \neq Z) \to A P A = {{norm}_{CV} (U) (A)}^{2}$
15	12 14	breqtrrd	$⊢ (U \in NrmCVec \land A \in X \land A \neq Z) \to 0 < A P A$
16	4 15	syl3an1	$⊢ (U \in {CHil}_{OLD} \land A \in X \land A \neq Z) \to 0 < A P A$

Metamath Proof Explorer