pjige0i

Description: The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	pjadjt.1	$⊢ H \in C_{ℋ}$
	Assertion	pjige0i	$⊢ A \in ℋ \to 0 \leq {proj}_{ℎ} (H) (A) \cdot_{ih} A$

Step	Hyp	Ref	Expression
1		pjadjt.1	$⊢ H \in C_{ℋ}$
2	1	pjhcli	$⊢ A \in ℋ \to {proj}_{ℎ} (H) (A) \in ℋ$
3		normcl	$⊢ {proj}_{ℎ} (H) (A) \in ℋ \to {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) \in ℝ$
4	2 3	syl	$⊢ A \in ℋ \to {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) \in ℝ$
5	4	sqge0d	$⊢ A \in ℋ \to 0 \leq {{norm}_{ℎ} ({proj}_{ℎ} (H) (A))}^{2}$
6	1	pjinormi	$⊢ A \in ℋ \to {proj}_{ℎ} (H) (A) \cdot_{ih} A = {{norm}_{ℎ} ({proj}_{ℎ} (H) (A))}^{2}$
7	5 6	breqtrrd	$⊢ A \in ℋ \to 0 \leq {proj}_{ℎ} (H) (A) \cdot_{ih} A$

Metamath Proof Explorer