---

Step * 1 1 1 2 1 of Lemma not-proj-sep-iff-proj-eq


1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. ∀i:ℕn + 1. ((u(a) i) = (u(b) i))
5. i : ℕn + 1
6. (u(a) i) = (u(b) i)
⊢ (a i) = ((||a||/||b||)*b i)
BY
{ (RepUR ``punit real-vec-mul`` -1 THEN RepUR ``real-vec-mul`` 0) }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. ∀i:ℕn + 1. ((u(a) i) = (u(b) i))
5. i : ℕn + 1
6. ((r1/||a||) * (a i)) = ((r1/||b||) * (b i))
⊢ (a i) = ((||a||/||b||) * (b i))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbP{}\^{}n
3.  b  :  \mBbbP{}\^{}n
4.  \mforall{}i:\mBbbN{}n  +  1.  ((u(a)  i)  =  (u(b)  i))
5.  i  :  \mBbbN{}n  +  1
6.  (u(a)  i)  =  (u(b)  i)
\mvdash{}  (a  i)  =  ((||a||/||b||)*b  i)


By

---

Latex:
(RepUR  ``punit  real-vec-mul``  -1  THEN  RepUR  ``real-vec-mul``  0)

---

Home Index