Step
*
1
3
of Lemma
pgeo-triangle-dual
1. pg : ProjectivePlane
2. a : Point
3. b : Point
4. c : Point
5. s : b ≠ c
6. t4 : a ≠ b ∨ c
7. s2 : a ≠ b
8. s3 : c ≠ a
9. s4 : b ∨ c ≠ c ∨ a
10. s5 : a ∨ b ≠ b ∨ c ∨ c ∨ a
⊢ ∃t*:pgeo-triangle(pg*). let a,b,c,s,s' = <a, b, c, s, t4> in let lab,lbc,lca,s1,s2 = t* in a I lab ∧ b I lab ∧ b I lbc\000C ∧ c I lbc ∧ c I lca ∧ a I lca
BY
{ At ⌜ℙ⌝ (InstConcl [⌜<a ∨ b, b ∨ c, c ∨ a, s4, s5>⌝])⋅ }
1
.....wf.....
1. pg : ProjectivePlane
2. a : Point
3. b : Point
4. c : Point
5. s : b ≠ c
6. t4 : a ≠ b ∨ c
7. s2 : a ≠ b
8. s3 : c ≠ a
9. s4 : b ∨ c ≠ c ∨ a
10. s5 : a ∨ b ≠ b ∨ c ∨ c ∨ a
⊢ <a ∨ b, b ∨ c, c ∨ a, s4, s5> ∈ pgeo-triangle(pg*)
2
1. pg : ProjectivePlane
2. a : Point
3. b : Point
4. c : Point
5. s : b ≠ c
6. t4 : a ≠ b ∨ c
7. s2 : a ≠ b
8. s3 : c ≠ a
9. s4 : b ∨ c ≠ c ∨ a
10. s5 : a ∨ b ≠ b ∨ c ∨ c ∨ a
⊢ let a@0,b@0,c@0,s@0,s' = <a, b, c, s, t4> in let lab,lbc,lca,s1,s2 = <a ∨ b, b ∨ c, c ∨ a, s4, s5> in a@0 I lab ∧ b@0 \000CI lab ∧ b@0 I lbc ∧ c@0 I lbc ∧ c@0 I lca ∧ a@0 I lca
3
.....wf.....
1. pg : ProjectivePlane
2. a : Point
3. b : Point
4. c : Point
5. s : b ≠ c
6. t4 : a ≠ b ∨ c
7. s2 : a ≠ b
8. s3 : c ≠ a
9. s4 : b ∨ c ≠ c ∨ a
10. s5 : a ∨ b ≠ b ∨ c ∨ c ∨ a
11. t* : pgeo-triangle(pg*)
⊢ let a,b,c,s,s' = <a, b, c, s, t4> in let lab,lbc,lca,s1,s2 = t* in a I lab ∧ b I lab ∧ b I lbc ∧ c I lbc ∧ c I lca ∧ a\000C I lca ∈ ℙ
Latex:
Latex:
1. pg : ProjectivePlane
2. a : Point
3. b : Point
4. c : Point
5. s : b \mneq{} c
6. t4 : a \mneq{} b \mvee{} c
7. s2 : a \mneq{} b
8. s3 : c \mneq{} a
9. s4 : b \mvee{} c \mneq{} c \mvee{} a
10. s5 : a \mvee{} b \mneq{} b \mvee{} c \mvee{} c \mvee{} a
\mvdash{} \mexists{}t*:pgeo-triangle(pg*)
let a,b,c,s,s' = <a, b, c, s, t4> in let lab,lbc,lca,s1,s2 = t* in a I lab
\mwedge{} b I lab
\mwedge{} b I lbc
\mwedge{} c I lbc
\mwedge{} c I lca
\mwedge{} a I lca
By
Latex:
At \mkleeneopen{}\mBbbP{}\mkleeneclose{} (InstConcl [\mkleeneopen{}<a \mvee{} b, b \mvee{} c, c \mvee{} a, s4, s5>\mkleeneclose{}])\mcdot{}
Home
Index