Nuprl Lemma : geo-cong3-to-conga-aux
∀e:BasicGeometry. ∀b,a,a',a0,e0,d,d',d0:Point.
(out(b aa') ⇒ out(e0 dd') ⇒ b_a_a0 ⇒ e0_d_d0 ⇒ ba' ≅ e0d' ⇒ aa0 ≅ e0d ⇒ dd0 ≅ ba ⇒ (ba0 ≅ e0d0 ∧ a'a0 ≅ d'd0))
Proof
Definitions occuring in Statement :
geo-out: out(p ab),
basic-geometry: BasicGeometry,
geo-congruent: ab ≅ cd,
geo-between: a_b_c,
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,
prop: ℙ,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
true: True,
squash: ↓T,
uiff: uiff(P;Q),
geo-out: out(p ab),
basic-geometry: BasicGeometry,
euclidean-plane: EuclideanPlane,
stable: Stable{P},
not: ¬A,
false: False,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
geo-zero-length: 0,
basic-geometry-: BasicGeometry-
Lemmas referenced :
geo-congruent_wf,
geo-between_wf,
geo-out_wf,
geo-point_wf,
euclidean-plane-structure-subtype,
euclidean-plane-subtype,
basic-geometry-subtype,
subtype_rel_transitivity,
basic-geometry_wf,
euclidean-plane_wf,
euclidean-plane-structure_wf,
geo-primitives_wf,
geo-add-length-comm,
geo-length-type_wf,
true_wf,
squash_wf,
geo-add-length_wf,
geo-add-length-between,
geo-congruent-trivial,
geo-length-flip,
geo-congruent-iff-length,
geo-between-symmetry,
geo-five-segment,
stable__geo-congruent,
not_wf,
geo-between-same-side,
Error :basic-geo-primitives_wf,
Error :basic-geo-structure_wf,
geo-between-seg-eq,
iff_weakening_equal,
equal_wf,
geo-mk-seg_wf,
geo-length_wf,
and_wf,
geo-add-length-zero,
geo-add-length-assoc,
geo-add-length-cancel-left,
geo-zero-length_wf,
geo-sum-eq-x,
geo-ab-eq-x,
geo-between-exchange4,
geo-between-exchange3,
geo-between-inner-trans,
subtype_rel_self,
basic-geo-axioms_wf,
geo-left-axioms_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
independent_pairFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
applyEquality,
because_Cache,
hypothesis,
sqequalRule,
instantiate,
independent_isectElimination,
baseClosed,
imageMemberEquality,
natural_numberEquality,
imageElimination,
lambdaEquality,
equalitySymmetry,
equalityTransitivity,
productElimination,
dependent_functionElimination,
setElimination,
rename,
independent_functionElimination,
voidElimination,
universeEquality,
applyLambdaEquality,
dependent_set_memberEquality,
hyp_replacement,
setEquality,
productEquality,
cumulativity,
equalityElimination
Latex:
\mforall{}e:BasicGeometry. \mforall{}b,a,a',a0,e0,d,d',d0:Point.
(out(b aa')
{}\mRightarrow{} out(e0 dd')
{}\mRightarrow{} b\_a\_a0
{}\mRightarrow{} e0\_d\_d0
{}\mRightarrow{} ba' \00D0 e0d'
{}\mRightarrow{} aa0 \00D0 e0d
{}\mRightarrow{} dd0 \00D0 ba
{}\mRightarrow{} (ba0 \00D0 e0d0 \mwedge{} a'a0 \00D0 d'd0))
Date html generated:
2017_10_02-PM-06_37_32
Last ObjectModification:
2017_08_17-PM-08_12_01
Theory : euclidean!plane!geometry
Home
Index