Step
*
1
of Lemma
common-P_point-parallel-P_lines
1. e : EuclideanParPlane@i'
2. p : Point@i
3. l : Line@i
4. n : Line@i
5. P4 : p I n@i
6. P5 : p # l@i
7. l1 : Line@i
8. L1 : p:Point × n:{n:Line| p I n} × p # l1@i
9. l || n
10. ∀l,m,n:Line. (l \/ m ⇒ (l \/ n ∨ m \/ n))
11. l1 \/ n
⊢ (l \/ l1 ∨ n \/ l1) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l1)
BY
{ ((InstHyp [⌜l1⌝;⌜n⌝;⌜l⌝] (10)⋅ THEN Auto) THEN D -1 THEN Auto) }
1
1. e : EuclideanParPlane@i'
2. p : Point@i
3. l : Line@i
4. n : Line@i
5. P4 : p I n@i
6. P5 : p # l@i
7. l1 : Line@i
8. L1 : p:Point × n:{n:Line| p I n} × p # l1@i
9. l || n
10. ∀l,m,n:Line. (l \/ m ⇒ (l \/ n ∨ m \/ n))
11. l1 \/ n
12. l1 \/ l
⊢ l \/ l1 ∨ n \/ l1
2
1. e : EuclideanParPlane@i'
2. p : Point@i
3. l : Line@i
4. n : Line@i
5. P4 : p I n@i
6. P5 : p # l@i
7. l1 : Line@i
8. L1 : p:Point × n:{n:Line| p I n} × p # l1@i
9. l || n
10. ∀l,m,n:Line. (l \/ m ⇒ (l \/ n ∨ m \/ n))
11. l1 \/ n
12. n \/ l
⊢ l \/ l1 ∨ n \/ l1
3
1. e : EuclideanParPlane@i'
2. p : Point@i
3. l : Line@i
4. n : Line@i
5. P4 : p I n@i
6. P5 : p # l@i
7. l1 : Line@i
8. L1 : p:Point × n:{n:Line| p I n} × p # l1@i
9. l || n
10. ∀l,m,n:Line. (l \/ m ⇒ (l \/ n ∨ m \/ n))
11. l1 \/ n
12. l1 \/ l ∨ n \/ l
13. l \/ l1 ∨ n \/ l1
14. x : Point@i
15. [%7] : x I l ∧ x I n@i
⊢ x # l1
Latex:
Latex:
1. e : EuclideanParPlane@i'
2. p : Point@i
3. l : Line@i
4. n : Line@i
5. P4 : p I n@i
6. P5 : p \# l@i
7. l1 : Line@i
8. L1 : p:Point \mtimes{} n:\{n:Line| p I n\} \mtimes{} p \# l1@i
9. l || n
10. \mforall{}l,m,n:Line. (l \mbackslash{}/ m {}\mRightarrow{} (l \mbackslash{}/ n \mvee{} m \mbackslash{}/ n))
11. l1 \mbackslash{}/ n
\mvdash{} (l \mbackslash{}/ l1 \mvee{} n \mbackslash{}/ l1) \mwedge{} (\mforall{}x:\{x:Point| x I l \mwedge{} x I n\} . x \# l1)
By
Latex:
((InstHyp [\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}] (10)\mcdot{} THEN Auto) THEN D -1 THEN Auto)
Home
Index