---

Step * 1 of Lemma pgeo-minimum-order-proof2


1. pg : ProjectivePlane
2. n : ℕ
3. l : Line
4. p,q:{p:Point| p I l} //p ≡ q ~ ℕn + 1
⊢ n ≥ 2 
BY
{ (SupposeNot
   THEN (InstLemma `pgeo-three-points-axiom` [⌜pg⌝;⌜l⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert {p:Point| p I l}  ⊆r (p,q:{p:Point| p I l} //p ≡ q) BY
               Auto)
   THEN (Assert (a ∈ {p:Point| p I l} ) ∧ (b ∈ {p:Point| p I l} ) ∧ (c ∈ {p:Point| p I l} ) BY
               Auto)
   THEN (InstLemma `cardinality-le-no_repeats-length`  [⌜p,q:{p:Point| p I l} //p ≡ q⌝;⌜2⌝;⌜[a; b; c]⌝]⋅ THENA Auto)) }

1
1. pg : ProjectivePlane
2. n : ℕ
3. l : Line
4. p,q:{p:Point| p I l} //p ≡ q ~ ℕn + 1
5. ¬(n ≥ 2 )
6. a : Point
7. b : Point
8. c : Point
9. a I l
10. b I l
11. c I l
12. a ≠ b
13. b ≠ c
14. c ≠ a
15. {p:Point| p I l}  ⊆r (p,q:{p:Point| p I l} //p ≡ q)
16. a ∈ {p:Point| p I l} 
17. b ∈ {p:Point| p I l} 
18. c ∈ {p:Point| p I l} 
⊢ |p,q:{p:Point| p I l} //p ≡ q| ≤ 2

2
1. pg : ProjectivePlane
2. n : ℕ
3. l : Line
4. p,q:{p:Point| p I l} //p ≡ q ~ ℕn + 1
5. ¬(n ≥ 2 )
6. a : Point
7. b : Point
8. c : Point
9. a I l
10. b I l
11. c I l
12. a ≠ b
13. b ≠ c
14. c ≠ a
15. {p:Point| p I l}  ⊆r (p,q:{p:Point| p I l} //p ≡ q)
16. a ∈ {p:Point| p I l} 
17. b ∈ {p:Point| p I l} 
18. c ∈ {p:Point| p I l} 
19. no_repeats(p,q:{p:Point| p I l} //p ≡ q;[c])
⊢ ¬(b ∈ [c])

3
1. pg : ProjectivePlane
2. n : ℕ
3. l : Line
4. p,q:{p:Point| p I l} //p ≡ q ~ ℕn + 1
5. ¬(n ≥ 2 )
6. a : Point
7. b : Point
8. c : Point
9. a I l
10. b I l
11. c I l
12. a ≠ b
13. b ≠ c
14. c ≠ a
15. {p:Point| p I l}  ⊆r (p,q:{p:Point| p I l} //p ≡ q)
16. a ∈ {p:Point| p I l} 
17. b ∈ {p:Point| p I l} 
18. c ∈ {p:Point| p I l} 
19. no_repeats(p,q:{p:Point| p I l} //p ≡ q;[b; c])
⊢ ¬(a ∈ [b; c])

4
1. pg : ProjectivePlane
2. n : ℕ
3. l : Line
4. p,q:{p:Point| p I l} //p ≡ q ~ ℕn + 1
5. ¬(n ≥ 2 )
6. a : Point
7. b : Point
8. c : Point
9. a I l
10. b I l
11. c I l
12. a ≠ b
13. b ≠ c
14. c ≠ a
15. {p:Point| p I l}  ⊆r (p,q:{p:Point| p I l} //p ≡ q)
16. (a ∈ {p:Point| p I l} ) ∧ (b ∈ {p:Point| p I l} ) ∧ (c ∈ {p:Point| p I l} )
17. ||[a; b; c]|| ≤ 2
⊢ 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:
(SupposeNot
  THEN  (InstLemma  `pgeo-three-points-axiom`  [\mkleeneopen{}pg\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  \{p:Point|  p  I  l\}    \msubseteq{}r  (p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q)  BY
                          Auto)
  THEN  (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)
  THEN  (InstLemma  `cardinality-le-no\_repeats-length`
                [\mkleeneopen{}p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}[a;  b;  c]\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index