---

Step * 1 1 1 2 1 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. ((r1/||a||) * (a i)) = ((r1/||b||) * (b i))
⊢ (a i) = ((||a||/||b||) * (b i))
BY
{ (nRMul ⌜||a||⌝ (-1)⋅ THENA Auto) }

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))
7. (((r1/||a||) * (a i)) * ||a||) = (((r1/||b||) * (b i)) * ||a||)
⊢ (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.  ((r1/||a||)  *  (a  i))  =  ((r1/||b||)  *  (b  i))
\mvdash{}  (a  i)  =  ((||a||/||b||)  *  (b  i))


By

---

Latex:
(nRMul  \mkleeneopen{}||a||\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)

---

Home Index