Nuprl Lemma : geo-Aparallel_transitivity
∀e:EuclideanParPlane. ∀l,m,n:LINE. (l || m ⇒ m || n ⇒ l || n)
Proof
Definitions occuring in Statement :
euclidean-parallel-plane: EuclideanParPlane,
geo-Aparallel: l || m,
geoline: LINE,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
geo-Aparallel: l || m,
not: ¬A,
geoline: LINE,
member: t ∈ T,
quotient: x,y:A//B[x; y],
and: P ∧ Q,
false: False,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
prop: ℙ,
guard: {T},
uimplies: b supposing a,
sq_type: SQType(T),
true: True
Lemmas referenced :
geo-Aparallel-trans-lines,
equal-wf-base,
geo-line_wf,
geo-line-eq_wf,
euclidean-plane-structure-subtype,
subtype_rel_transitivity,
euclidean-parallel-plane_wf,
euclidean-plane-structure_wf,
geo-primitives_wf,
subtype_base_sq,
int_subtype_base,
geo-intersect_wf,
geo-Aparallel_wf,
euclidean-planes-subtype,
geoline_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalHypSubstitution,
pointwiseFunctionalityForEquality,
intEquality,
sqequalRule,
pertypeElimination,
productElimination,
thin,
introduction,
extract_by_obid,
dependent_functionElimination,
hypothesisEquality,
equalityTransitivity,
hypothesis,
equalitySymmetry,
independent_functionElimination,
voidElimination,
productEquality,
isectElimination,
applyEquality,
because_Cache,
instantiate,
independent_isectElimination,
cumulativity,
natural_numberEquality,
promote_hyp
Latex:
\mforall{}e:EuclideanParPlane. \mforall{}l,m,n:LINE. (l || m {}\mRightarrow{} m || n {}\mRightarrow{} l || n)
Date html generated:
2018_05_22-PM-01_10_54
Last ObjectModification:
2018_05_11-AM-09_50_21
Theory : euclidean!plane!geometry
Home
Index