---

Step * 1 of Lemma proj-sep-implies


1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. i : ℕn + 1
5. u(a) i ≠ u(b) i
6. ∃i:ℕn + 1. u(a) i ≠ r(-1)*u(b) i
⊢ a i ≠ (||a||/||b||)*b i
BY
{ (Thin (-1) 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) ≠ (r1/||b||) * (b i)
⊢ a i ≠ (||a||/||b||) * (b i)

---

Latex:

---

Latex:

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


By

---

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

---

Home Index