Nuprl Lemma : parallel-preserves-intersection
∀eu:EuclideanParPlane. ∀l,m,n:Line. ((l \/ m ⇒ (l \/ n ∨ m \/ n)) ⇒ (l \/ m ∧ l || n) ⇒ m \/ n)
Proof
Definitions occuring in Statement :
euclidean-parallel-plane: EuclideanParPlane,
geo-Aparallel: l || m,
geo-intersect: L \/ M,
geo-line: Line,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q
Definitions unfolded in proof :
uimplies: b supposing a,
guard: {T},
subtype_rel: A ⊆r B,
euclidean-parallel-plane: EuclideanParPlane,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
false: False,
not: ¬A,
geo-Aparallel: l || m,
or: P ∨ Q,
and: P ∧ Q,
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
geo-primitives_wf,
euclidean-plane-structure_wf,
euclidean-plane_wf,
euclidean-parallel-plane_wf,
subtype_rel_transitivity,
euclidean-planes-subtype,
euclidean-plane-subtype,
euclidean-plane-structure-subtype,
geo-line_wf,
or_wf,
geo-Aparallel_wf,
geoline-subtype1,
geo-intersect_wf
Rules used in proof :
independent_isectElimination,
instantiate,
dependent_functionElimination,
functionEquality,
sqequalRule,
because_Cache,
applyEquality,
hypothesisEquality,
rename,
setElimination,
isectElimination,
extract_by_obid,
introduction,
cut,
productEquality,
voidElimination,
unionElimination,
hypothesis,
independent_functionElimination,
thin,
productElimination,
sqequalHypSubstitution,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}eu:EuclideanParPlane. \mforall{}l,m,n:Line. ((l \mbackslash{}/ m {}\mRightarrow{} (l \mbackslash{}/ n \mvee{} m \mbackslash{}/ n)) {}\mRightarrow{} (l \mbackslash{}/ m \mwedge{} l || n) {}\mRightarrow{} m \mbackslash{}/ n)
Date html generated:
2018_07_29-AM-09_39_19
Last ObjectModification:
2018_06_26-PM-08_50_54
Theory : euclidean!plane!geometry
Home
Index