ipge0

Description: The inner product in a subcomplex pre-Hilbert space is positive definite. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	reipcl.v	$⊢ V = {Base}_{W}$
	reipcl.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
Assertion	ipge0	$⊢ (W \in CPreHil \land A \in V) \to 0 \leq A \underset{˙}{,} A$

Step	Hyp	Ref	Expression
1		reipcl.v	$⊢ V = {Base}_{W}$
2		reipcl.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		cphngp	$⊢ W \in CPreHil \to W \in NrmGrp$
4		eqid	$⊢ norm (W) = norm (W)$
5	1 4	nmcl	$⊢ (W \in NrmGrp \land A \in V) \to norm (W) (A) \in ℝ$
6	3 5	sylan	$⊢ (W \in CPreHil \land A \in V) \to norm (W) (A) \in ℝ$
7	6	sqge0d	$⊢ (W \in CPreHil \land A \in V) \to 0 \leq {norm (W) (A)}^{2}$
8	1 2 4	nmsq	$⊢ (W \in CPreHil \land A \in V) \to {norm (W) (A)}^{2} = A \underset{˙}{,} A$
9	7 8	breqtrd	$⊢ (W \in CPreHil \land A \in V) \to 0 \leq A \underset{˙}{,} A$

Metamath Proof Explorer