Step
*
1
1
1
1
of Lemma
geo-intersect-unique
1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. z : Point
12. z I l
13. z # m
14. ∀a,b,c,d,p,q:Point.
((¬Colinear(a;b;c)) ⇒ c ≠ d ⇒ Colinear(a;b;p) ⇒ Colinear(a;b;q) ⇒ Colinear(c;d;p) ⇒ Colinear(c;d;q) ⇒ p ≡ q)
15. fst(l) ≠ z
⊢ x ≡ y
BY
{ (InstHyp [⌜fst(m)⌝;⌜fst(snd(m))⌝;⌜z⌝;⌜fst(l)⌝;⌜x⌝;⌜y⌝] (-2)⋅ THEN Auto) }
1
.....antecedent.....
1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. z : Point
12. z I l
13. z # m
14. ∀a,b,c,d,p,q:Point.
((¬Colinear(a;b;c)) ⇒ c ≠ d ⇒ Colinear(a;b;p) ⇒ Colinear(a;b;q) ⇒ Colinear(c;d;p) ⇒ Colinear(c;d;q) ⇒ p ≡ q)
15. fst(l) ≠ z
⊢ ¬Colinear(fst(m);fst(snd(m));z)
2
.....antecedent.....
1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. z : Point
12. z I l
13. z # m
14. ∀a,b,c,d,p,q:Point.
((¬Colinear(a;b;c)) ⇒ c ≠ d ⇒ Colinear(a;b;p) ⇒ Colinear(a;b;q) ⇒ Colinear(c;d;p) ⇒ Colinear(c;d;q) ⇒ p ≡ q)
15. fst(l) ≠ z
⊢ Colinear(fst(m);fst(snd(m));x)
3
.....antecedent.....
1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. z : Point
12. z I l
13. z # m
14. ∀a,b,c,d,p,q:Point.
((¬Colinear(a;b;c)) ⇒ c ≠ d ⇒ Colinear(a;b;p) ⇒ Colinear(a;b;q) ⇒ Colinear(c;d;p) ⇒ Colinear(c;d;q) ⇒ p ≡ q)
15. fst(l) ≠ z
⊢ Colinear(fst(m);fst(snd(m));y)
4
.....antecedent.....
1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. z : Point
12. z I l
13. z # m
14. ∀a,b,c,d,p,q:Point.
((¬Colinear(a;b;c)) ⇒ c ≠ d ⇒ Colinear(a;b;p) ⇒ Colinear(a;b;q) ⇒ Colinear(c;d;p) ⇒ Colinear(c;d;q) ⇒ p ≡ q)
15. fst(l) ≠ z
⊢ Colinear(z;fst(l);x)
5
.....antecedent.....
1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. z : Point
12. z I l
13. z # m
14. ∀a,b,c,d,p,q:Point.
((¬Colinear(a;b;c)) ⇒ c ≠ d ⇒ Colinear(a;b;p) ⇒ Colinear(a;b;q) ⇒ Colinear(c;d;p) ⇒ Colinear(c;d;q) ⇒ p ≡ q)
15. fst(l) ≠ z
⊢ Colinear(z;fst(l);y)
Latex:
Latex:
1. eu : EuclideanParPlane@i'
2. l : Line@i
3. m : Line@i
4. x : Point@i
5. y : Point@i
6. l \mbackslash{}/ m
7. x I l
8. x I m
9. y I l
10. y I m
11. z : Point
12. z I l
13. z \# m
14. \mforall{}a,b,c,d,p,q:Point.
((\mneg{}Colinear(a;b;c))
{}\mRightarrow{} c \mneq{} d
{}\mRightarrow{} Colinear(a;b;p)
{}\mRightarrow{} Colinear(a;b;q)
{}\mRightarrow{} Colinear(c;d;p)
{}\mRightarrow{} Colinear(c;d;q)
{}\mRightarrow{} p \mequiv{} q)
15. fst(l) \mneq{} z
\mvdash{} x \mequiv{} y
By
Latex:
(InstHyp [\mkleeneopen{}fst(m)\mkleeneclose{};\mkleeneopen{}fst(snd(m))\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}fst(l)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}] (-2)\mcdot{} THEN Auto)
Home
Index