---

Step * of Lemma proj-eq-equiv

∀[n:ℕ]. EquivRel(ℙ^n;a,b.a = b)
BY
{ (Auto
   THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto))
   THEN Try ((D 0 THEN Complete (Auto)))
   THEN Try ((ParallelLast THEN RWO "-1" 0 THEN Auto))
   THEN (All (RWO "proj-eq-iff") THENA Auto)
   THEN SqExRepD
   THEN D 0) }

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;a;m*c)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  EquivRel(\mBbbP{}\^{}n;a,b.a  =  b)


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto))
  THEN  Try  ((D  0  THEN  Complete  (Auto)))
  THEN  Try  ((ParallelLast  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  (All  (RWO  "proj-eq-iff")  THENA  Auto)
  THEN  SqExRepD
  THEN  D  0)

---

Home Index