---

Step * 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)
⊢ (proj-rev(n;p1) i) = (m*proj-rev(n;p2) i)
BY
{ All  (RepUR ``proj-rev real-vec-mul``) }

1
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 )

---

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{}  (proj-rev(n;p1)  i)  =  (m*proj-rev(n;p2)  i)


By

---

Latex:
All    (RepUR  ``proj-rev  real-vec-mul``)

---

Home Index