---

Step * 1 of Lemma pgeo-minimum-order


1. pg : ProjectivePlane
2. n : ℕ
3. l : Line
4. p,q:{p:Point| p I l} //p ≡ q ~ ℕn + 1
⊢ n ≥ 2 
BY
{ (((RepeatFor 2 (D -1) THEN Thin (-1))
    THEN (Assert ∀p,q:Point.  (p ≠ q ⇒ (¬(p = q ∈ (p,q:{p:Point| p I l} //p ≡ q)))) BY
                (Intros THEN (D 0 THENA Auto) THEN (EqTypeHD (-1)⋅ THENA Auto) THEN D -1 THEN Auto))
    THEN (Assert ∀x,y:p,q:{p:Point| p I l} //p ≡ q.  ((¬(x = y ∈ (p,q:{p:Point| p I l} //p ≡ q))) ⇒ (¬((f x) = (f y) ∈ \000Cℤ))) BY
                (Intros
                 THEN (D 0 THENA Auto)
                 THEN (D 5 With ⌜x⌝  THENA Auto)
                 THEN (D -1 With ⌜y⌝  THENA Auto)
                 THEN D -1
                 THEN Auto)))
   THEN (InstLemma `pgeo-three-points-axiom` [⌜pg⌝;⌜l⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN RepeatFor 3 ((FHyp 6 [-3] THENA Auto))
   THEN (Assert {p:Point| p I l}  ⊆r (p,q:{p:Point| p I l} //p ≡ q) BY
               Auto)) }

1
1. pg : ProjectivePlane
2. n : ℕ
3. l : Line
4. f : (p,q:{p:Point| p I l} //p ≡ q) ⟶ ℕn + 1
5. Inj(p,q:{p:Point| p I l} //p ≡ q;ℕn + 1;f)
6. ∀p,q:Point.  (p ≠ q ⇒ (¬(p = q ∈ (p,q:{p:Point| p I l} //p ≡ q))))
7. ∀x,y:p,q:{p:Point| p I l} //p ≡ q.  ((¬(x = y ∈ (p,q:{p:Point| p I l} //p ≡ q))) ⇒ (¬((f x) = (f y) ∈ ℤ)))
8. a : Point
9. b : Point
10. c : Point
11. a I l
12. b I l
13. c I l
14. a ≠ b
15. b ≠ c
16. c ≠ a
17. ¬(a = b ∈ (p,q:{p:Point| p I l} //p ≡ q))
18. ¬(b = c ∈ (p,q:{p:Point| p I l} //p ≡ q))
19. ¬(c = a ∈ (p,q:{p:Point| p I l} //p ≡ q))
20. {p:Point| p I l}  ⊆r (p,q:{p:Point| p I l} //p ≡ q)
⊢ n ≥ 2 

---

Latex:

---

Latex:

1.  pg  :  ProjectivePlane
2.  n  :  \mBbbN{}
3.  l  :  Line
4.  p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q  \msim{}  \mBbbN{}n  +  1
\mvdash{}  n  \mgeq{}  2 


By

---

Latex:
(((RepeatFor  2  (D  -1)  THEN  Thin  (-1))
    THEN  (Assert  \mforall{}p,q:Point.    (p  \mneq{}  q  {}\mRightarrow{}  (\mneg{}(p  =  q)))  BY
                            (Intros  THEN  (D  0  THENA  Auto)  THEN  (EqTypeHD  (-1)\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  Auto))
    THEN  (Assert  \mforall{}x,y:p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q.    ((\mneg{}(x  =  y))  {}\mRightarrow{}  (\mneg{}((f  x)  =  (f  y))))  BY
                            (Intros
                              THEN  (D  0  THENA  Auto)
                              THEN  (D  5  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
                              THEN  (D  -1  With  \mkleeneopen{}y\mkleeneclose{}    THENA  Auto)
                              THEN  D  -1
                              THEN  Auto)))
  THEN  (InstLemma  `pgeo-three-points-axiom`  [\mkleeneopen{}pg\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  RepeatFor  3  ((FHyp  6  [-3]  THENA  Auto))
  THEN  (Assert  \{p:Point|  p  I  l\}    \msubseteq{}r  (p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q)  BY
                          Auto))

---

Home Index