---

Step * 1 1 of Lemma proj-rev_functionality


1. n : ℕ
2. p1 : ℙ^n
3. p2 : ℙ^n
4. m : {m:ℝ| m ≠ r0} 
5. ∀i:ℕn + 1. ((p1 i) = (m * (p2 i)))
6. i : ℕn + 1
7. (p1 i) = (m * (p2 i))
⊢ if i <z n then p1 i else -(p1 i) fi  = (m * if i <z n then p2 i else -(p2 i) fi )
BY
{ (AutoSplit THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  p1  :  \mBbbP{}\^{}n
3.  p2  :  \mBbbP{}\^{}n
4.  m  :  \{m:\mBbbR{}|  m  \mneq{}  r0\} 
5.  \mforall{}i:\mBbbN{}n  +  1.  ((p1  i)  =  (m  *  (p2  i)))
6.  i  :  \mBbbN{}n  +  1
7.  (p1  i)  =  (m  *  (p2  i))
\mvdash{}  if  i  <z  n  then  p1  i  else  -(p1  i)  fi    =  (m  *  if  i  <z  n  then  p2  i  else  -(p2  i)  fi  )


By

---

Latex:
(AutoSplit  THEN  RWO  "-1"  0  THEN  Auto)

---

Home Index