---

Step * 1 of Lemma proj-eq-equiv


1. n : ℕ
2. Sym(ℙ^n;a,b.↓∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;a;m*b))
3. a : ℙ^n
4. b : ℙ^n
5. c : ℙ^n
6. m1 : {m:ℝ| m ≠ r0} 
7. req-vec(n + 1;a;m1*b)
8. m : {m:ℝ| m ≠ r0} 
9. req-vec(n + 1;b;m*c)
⊢ ∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;a;m*c)
BY
{ (RWO "-3" 0 THENA Auto) }

1
1. n : ℕ
2. Sym(ℙ^n;a,b.↓∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;a;m*b))
3. a : ℙ^n
4. b : ℙ^n
5. c : ℙ^n
6. m1 : {m:ℝ| m ≠ r0} 
7. req-vec(n + 1;a;m1*b)
8. m : {m:ℝ| m ≠ r0} 
9. req-vec(n + 1;b;m*c)
⊢ ∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;m1*b;m*c)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  Sym(\mBbbP{}\^{}n;a,b.\mdownarrow{}\mexists{}m:\{m:\mBbbR{}|  m  \mneq{}  r0\}  .  req-vec(n  +  1;a;m*b))
3.  a  :  \mBbbP{}\^{}n
4.  b  :  \mBbbP{}\^{}n
5.  c  :  \mBbbP{}\^{}n
6.  m1  :  \{m:\mBbbR{}|  m  \mneq{}  r0\} 
7.  req-vec(n  +  1;a;m1*b)
8.  m  :  \{m:\mBbbR{}|  m  \mneq{}  r0\} 
9.  req-vec(n  +  1;b;m*c)
\mvdash{}  \mexists{}m:\{m:\mBbbR{}|  m  \mneq{}  r0\}  .  req-vec(n  +  1;a;m*c)


By

---

Latex:
(RWO  "-3"  0  THENA  Auto)

---

Home Index