Nuprl Lemma : eu-eq_dist-axiomsC-five-segment
∀e:EuclideanPlane. ∀x,y,z,x',y',z',u,u':Point.
(Dcong(e;x;y;x';y')
⇒ Dcong(e;y;z;y';z')
⇒ Dcong(e;x;u;x';u')
⇒ Dcong(e;y;u;y';u')
⇒ (Dbet(e;x;y;z) ∧ Dsep(e;x;y) ∧ Dsep(e;y;z))
⇒ (Dbet(e;x';y';z') ∧ Dsep(e;x';y') ∧ Dsep(e;y';z'))
⇒ Dcong(e;z;u;z';u'))
Proof
Definitions occuring in Statement :
dist-cong: Dcong(g;a;b;c;d),
dist-bet: Dbet(g;a;b;c),
dist-sep: Dsep(g;a;b),
euclidean-plane: EuclideanPlane,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
guard: {T},
cand: A c∧ B,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
prop: ℙ,
iff: P ⇐⇒ Q,
uimplies: b supposing a,
rev_implies: P ⇐ Q
Lemmas referenced :
lsep-all-sym,
Euclid-Prop20_cycle,
geo-lsep_wf,
Dcong-iff-cong,
dist-bet_wf,
dist-sep_wf,
dist-cong_wf,
geo-point_wf,
euclidean-plane-structure-subtype,
euclidean-plane-subtype,
subtype_rel_transitivity,
euclidean-plane_wf,
euclidean-plane-structure_wf,
geo-primitives_wf,
Dbet-to-between,
geo-five-segment,
Dsep-iff-sep
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
sqequalHypSubstitution,
productElimination,
thin,
cut,
introduction,
extract_by_obid,
dependent_functionElimination,
hypothesisEquality,
independent_functionElimination,
hypothesis,
because_Cache,
universeIsType,
isectElimination,
applyEquality,
sqequalRule,
productIsType,
inhabitedIsType,
instantiate,
independent_isectElimination
Latex:
\mforall{}e:EuclideanPlane. \mforall{}x,y,z,x',y',z',u,u':Point.
(Dcong(e;x;y;x';y')
{}\mRightarrow{} Dcong(e;y;z;y';z')
{}\mRightarrow{} Dcong(e;x;u;x';u')
{}\mRightarrow{} Dcong(e;y;u;y';u')
{}\mRightarrow{} (Dbet(e;x;y;z) \mwedge{} Dsep(e;x;y) \mwedge{} Dsep(e;y;z))
{}\mRightarrow{} (Dbet(e;x';y';z') \mwedge{} Dsep(e;x';y') \mwedge{} Dsep(e;y';z'))
{}\mRightarrow{} Dcong(e;z;u;z';u'))
Date html generated:
2019_10_16-PM-02_59_00
Last ObjectModification:
2019_06_05-PM-04_11_15
Theory : euclidean!plane!geometry
Home
Index