Nuprl Lemma : geo-playfair-axiom
∀e:EuclideanParPlane. ∀p:Point. ∀l,m,n:Line. ((p I m ∧ m || l) ⇒ (p I n ∧ n || l) ⇒ m ≡ n)
Proof
Definitions occuring in Statement :
euclidean-parallel-plane: EuclideanParPlane,
geo-Aparallel: l || m,
geo-incident: p I L,
geo-line-eq: l ≡ m,
geo-line: Line,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
Playfair-axiom: Playfair-axiom(e),
all: ∀x:A. B[x],
euclidean-parallel-plane: EuclideanParPlane,
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
sq_stable: SqStable(P),
squash: ↓T
Lemmas referenced :
sq_stable__from_stable,
Playfair-axiom_wf,
stable__Playfair-axiom,
euclidean-parallel-plane_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
sqequalHypSubstitution,
setElimination,
thin,
rename,
cut,
introduction,
extract_by_obid,
isectElimination,
dependent_functionElimination,
hypothesisEquality,
hypothesis,
independent_functionElimination,
imageMemberEquality,
baseClosed,
imageElimination
Latex:
\mforall{}e:EuclideanParPlane. \mforall{}p:Point. \mforall{}l,m,n:Line. ((p I m \mwedge{} m || l) {}\mRightarrow{} (p I n \mwedge{} n || l) {}\mRightarrow{} m \mequiv{} n)
Date html generated:
2018_05_22-PM-01_09_28
Last ObjectModification:
2018_05_11-PM-10_49_49
Theory : euclidean!plane!geometry
Home
Index