---

Step * 1 1 of Lemma p2J_functionality


1. a1 : ℙ^2
2. b1 : ℙ^2
3. a2 : ℙ^2
4. b2 : ℙ^2
5. a2 ≠ b2
6. m1 : ℝ
7. m1 ≠ r0
8. req-vec(3;a1;m1*a2)
9. m : ℝ
10. m ≠ r0
11. req-vec(3;b1;m*b2)
12. a1 ≠ b1
13. m1 * m ≠ r0
⊢ req-vec(3;p2J(a1;b1);m1 * m*p2J(a2;b2))
BY
{ (All (RepUR ``req-vec real-vec-mul``)
   THEN Auto
   THEN IntSegCases (-1)
   THEN RepUR ``p2J`` 0
   THEN RWO "8 11" 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a1  :  \mBbbP{}\^{}2
2.  b1  :  \mBbbP{}\^{}2
3.  a2  :  \mBbbP{}\^{}2
4.  b2  :  \mBbbP{}\^{}2
5.  a2  \mneq{}  b2
6.  m1  :  \mBbbR{}
7.  m1  \mneq{}  r0
8.  req-vec(3;a1;m1*a2)
9.  m  :  \mBbbR{}
10.  m  \mneq{}  r0
11.  req-vec(3;b1;m*b2)
12.  a1  \mneq{}  b1
13.  m1  *  m  \mneq{}  r0
\mvdash{}  req-vec(3;p2J(a1;b1);m1  *  m*p2J(a2;b2))


By

---

Latex:
(All  (RepUR  ``req-vec  real-vec-mul``)
  THEN  Auto
  THEN  IntSegCases  (-1)
  THEN  RepUR  ``p2J``  0
  THEN  RWO  "8  11"  0
  THEN  Auto)\mcdot{}

---

Home Index