pjssge0ii

Description: Theorem 4.5(iv)->(v) of Beran p. 112. (Contributed by NM, 13-Aug-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjidm.1	$⊢ H \in C_{ℋ}$
	pjidm.2	$⊢ A \in ℋ$
	pjsslem.1	$⊢ G \in C_{ℋ}$
Assertion	pjssge0ii	$⊢ {proj}_{ℎ} (G) (A) -_{ℎ} {proj}_{ℎ} (H) (A) = {proj}_{ℎ} (G \cap ⊥ (H)) (A) \to 0 \leq ({proj}_{ℎ} (G) (A) -_{ℎ} {proj}_{ℎ} (H) (A)) \cdot_{ih} A$

Step	Hyp	Ref	Expression
1		pjidm.1	$⊢ H \in C_{ℋ}$
2		pjidm.2	$⊢ A \in ℋ$
3		pjsslem.1	$⊢ G \in C_{ℋ}$
4	1	choccli	$⊢ ⊥ (H) \in C_{ℋ}$
5	3 4	chincli	$⊢ G \cap ⊥ (H) \in C_{ℋ}$
6	5 2	pjhclii	$⊢ {proj}_{ℎ} (G \cap ⊥ (H)) (A) \in ℋ$
7	6	normcli	$⊢ {norm}_{ℎ} ({proj}_{ℎ} (G \cap ⊥ (H)) (A)) \in ℝ$
8	7	sqge0i	$⊢ 0 \leq {{norm}_{ℎ} ({proj}_{ℎ} (G \cap ⊥ (H)) (A))}^{2}$
9		oveq1	$⊢ {proj}_{ℎ} (G) (A) -_{ℎ} {proj}_{ℎ} (H) (A) = {proj}_{ℎ} (G \cap ⊥ (H)) (A) \to ({proj}_{ℎ} (G) (A) -_{ℎ} {proj}_{ℎ} (H) (A)) \cdot_{ih} A = {proj}_{ℎ} (G \cap ⊥ (H)) (A) \cdot_{ih} A$
10	5 2	pjinormii	$⊢ {proj}_{ℎ} (G \cap ⊥ (H)) (A) \cdot_{ih} A = {{norm}_{ℎ} ({proj}_{ℎ} (G \cap ⊥ (H)) (A))}^{2}$
11	9 10	eqtrdi	$⊢ {proj}_{ℎ} (G) (A) -_{ℎ} {proj}_{ℎ} (H) (A) = {proj}_{ℎ} (G \cap ⊥ (H)) (A) \to ({proj}_{ℎ} (G) (A) -_{ℎ} {proj}_{ℎ} (H) (A)) \cdot_{ih} A = {{norm}_{ℎ} ({proj}_{ℎ} (G \cap ⊥ (H)) (A))}^{2}$
12	8 11	breqtrrid	$⊢ {proj}_{ℎ} (G) (A) -_{ℎ} {proj}_{ℎ} (H) (A) = {proj}_{ℎ} (G \cap ⊥ (H)) (A) \to 0 \leq ({proj}_{ℎ} (G) (A) -_{ℎ} {proj}_{ℎ} (H) (A)) \cdot_{ih} A$

Metamath Proof Explorer