---

Step * 1 1 of Lemma pgeo-minimum-order


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 
BY
{ (Assert (a ∈ {p:Point| p I l} ) ∧ (b ∈ {p:Point| p I l} ) ∧ (c ∈ {p:Point| p I l} ) 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)
21. (a ∈ {p:Point| p I l} ) ∧ (b ∈ {p:Point| p I l} ) ∧ (c ∈ {p:Point| p I l} )
⊢ n ≥ 2 

---

Latex:

---

Latex:

1.  pg  :  ProjectivePlane
2.  n  :  \mBbbN{}
3.  l  :  Line
4.  f  :  (p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q)  {}\mrightarrow{}  \mBbbN{}n  +  1
5.  Inj(p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q;\mBbbN{}n  +  1;f)
6.  \mforall{}p,q:Point.    (p  \mneq{}  q  {}\mRightarrow{}  (\mneg{}(p  =  q)))
7.  \mforall{}x,y:p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q.    ((\mneg{}(x  =  y))  {}\mRightarrow{}  (\mneg{}((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  \mneq{}  b
15.  b  \mneq{}  c
16.  c  \mneq{}  a
17.  \mneg{}(a  =  b)
18.  \mneg{}(b  =  c)
19.  \mneg{}(c  =  a)
20.  \{p:Point|  p  I  l\}    \msubseteq{}r  (p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q)
\mvdash{}  n  \mgeq{}  2 


By

---

Latex:
(Assert  (a  \mmember{}  \{p:Point|  p  I  l\}  )  \mwedge{}  (b  \mmember{}  \{p:Point|  p  I  l\}  )  \mwedge{}  (c  \mmember{}  \{p:Point|  p  I  l\}  )  BY
              Auto)

---

Home Index