---

Step * 2 1 of Lemma proj-eq-iff


1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. m : {m:ℝ| m ≠ r0} 
5. req-vec(n + 1;a;m*b)
6. i : ℕn + 1
7. j : ℕn + 1
⊢ ((a i) * (b j)) = ((b i) * (a j))
BY
{ (RepUR ``req-vec real-vec-mul`` 5 THEN RWO  "5" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbP{}\^{}n
3.  b  :  \mBbbP{}\^{}n
4.  m  :  \{m:\mBbbR{}|  m  \mneq{}  r0\} 
5.  req-vec(n  +  1;a;m*b)
6.  i  :  \mBbbN{}n  +  1
7.  j  :  \mBbbN{}n  +  1
\mvdash{}  ((a  i)  *  (b  j))  =  ((b  i)  *  (a  j))


By

---

Latex:
(RepUR  ``req-vec  real-vec-mul``  5  THEN  RWO    "5"  0  THEN  Auto)

---

Home Index