---

Step * 2 of Lemma proj-eq-iff


1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. ↓∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;a;m*b)
⊢ a = b
BY
{ ((((D -1 THEN Unhide) THEN Auto) THEN ExRepD) THEN D 0 THEN Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((((D  -1  THEN  Unhide)  THEN  Auto)  THEN  ExRepD)  THEN  D  0  THEN  Auto)

---

Home Index