---

Step * 1 of Lemma proj-eq-iff


1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. a = b
⊢ ↓∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;a;m*b)
BY
{ ((DVar `b' THEN ExRepD) THEN Unfold `proj-eq` -1) }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℝ^n + 1
4. k : ℕn + 1
5. b k ≠ r0
6. ∀i,j:ℕn + 1.  (((a i) * (b j)) = ((b i) * (a j)))
⊢ ↓∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;a;m*b)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbP{}\^{}n
3.  b  :  \mBbbP{}\^{}n
4.  a  =  b
\mvdash{}  \mdownarrow{}\mexists{}m:\{m:\mBbbR{}|  m  \mneq{}  r0\}  .  req-vec(n  +  1;a;m*b)


By

---

Latex:
((DVar  `b'  THEN  ExRepD)  THEN  Unfold  `proj-eq`  -1)

---

Home Index