---

Step * of Lemma p2J_functionality

∀[a1,b1,a2,b2:ℙ^2].  (p2J(a1;b1) = p2J(a2;b2)) supposing (b1 = b2 and a1 = a2 and a1 ≠ b1)
BY
{ (Intros
   THEN Unhide
   THEN Auto
   THEN DupHyp (-3)
   THEN RWO "-3 -2" (-4)
   THEN Auto
   THEN (All (RWO "proj-eq-iff") THENA Auto)
   THEN SqExRepD
   THEN DSetVars) }

1
1. a1 : ℙ^2
2. b1 : ℙ^2
3. a2 : ℙ^2
4. b2 : ℙ^2
5. a2 ≠ b2
6. m1 : ℝ
7. m1 ≠ r0
8. req-vec(2 + 1;a1;m1*a2)
9. m : ℝ
10. m ≠ r0
11. req-vec(2 + 1;b1;m*b2)
12. a1 ≠ b1
⊢ ↓∃m:{m:ℝ| m ≠ r0} . req-vec(2 + 1;p2J(a1;b1);m*p2J(a2;b2))

---

Latex:

---

Latex:
\mforall{}[a1,b1,a2,b2:\mBbbP{}\^{}2].    (p2J(a1;b1)  =  p2J(a2;b2))  supposing  (b1  =  b2  and  a1  =  a2  and  a1  \mneq{}  b1)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Auto
  THEN  DupHyp  (-3)
  THEN  RWO  "-3  -2"  (-4)
  THEN  Auto
  THEN  (All  (RWO  "proj-eq-iff")  THENA  Auto)
  THEN  SqExRepD
  THEN  DSetVars)

---

Home Index