---

Step * 2 of Lemma proj-sep-implies


1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. ∃i:ℕn + 1. u(a) i ≠ u(b) i
5. i : ℕn + 1
6. u(a) i ≠ r(-1)*u(b) i
⊢ a i ≠ (-(||a||)/||b||)*b i
BY
{ (Thin (-3) THEN RepUR ``punit real-vec-mul`` -1 THEN RepUR ``real-vec-mul`` 0) }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. i : ℕn + 1
5. (r1/||a||) * (a i) ≠ r(-1) * (r1/||b||) * (b i)
⊢ a i ≠ (-(||a||)/||b||) * (b i)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbP{}\^{}n
3.  b  :  \mBbbP{}\^{}n
4.  \mexists{}i:\mBbbN{}n  +  1.  u(a)  i  \mneq{}  u(b)  i
5.  i  :  \mBbbN{}n  +  1
6.  u(a)  i  \mneq{}  r(-1)*u(b)  i
\mvdash{}  a  i  \mneq{}  (-(||a||)/||b||)*b  i


By

---

Latex:
(Thin  (-3)  THEN  RepUR  ``punit  real-vec-mul``  -1  THEN  RepUR  ``real-vec-mul``  0)

---

Home Index