---

Step * 2 1 1 1 of Lemma not-proj-sep-iff-proj-eq


1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. m : ℝ
5. ||a|| = (|m| * ||b||)
6. m < r0
7. ∀i:ℕn + 1. ((a i) = (m * (b i)))
8. i : ℕn + 1
9. (a i) = (m * (b i))
⊢ ((b i) * ||b|| * m) = -((b i) * ||a||)
BY
{ (RWO "5" 0 THENA Auto) }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. m : ℝ
5. ||a|| = (|m| * ||b||)
6. m < r0
7. ∀i:ℕn + 1. ((a i) = (m * (b i)))
8. i : ℕn + 1
9. (a i) = (m * (b i))
⊢ ((b i) * ||b|| * m) = -((b i) * |m| * ||b||)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbP{}\^{}n
3.  b  :  \mBbbP{}\^{}n
4.  m  :  \mBbbR{}
5.  ||a||  =  (|m|  *  ||b||)
6.  m  <  r0
7.  \mforall{}i:\mBbbN{}n  +  1.  ((a  i)  =  (m  *  (b  i)))
8.  i  :  \mBbbN{}n  +  1
9.  (a  i)  =  (m  *  (b  i))
\mvdash{}  ((b  i)  *  ||b||  *  m)  =  -((b  i)  *  ||a||)


By

---

Latex:
(RWO  "5"  0  THENA  Auto)

---

Home Index