Nuprl Lemma : congruence-preserves-between_symmetric-points

e:BasicGeometry. ∀a,b,c,b',c':Point.
  (a_b_c  Colinear(a;c;c')  ab ≅ ab'  ac ≅ ac'  b'-a-b  c ≠ c'  a_b'_c')


Proof




Definitions occuring in Statement :  basic-geometry: BasicGeometry geo-colinear: Colinear(a;b;c) geo-strict-between: a-b-c geo-congruent: ab ≅ cd geo-between: a_b_c geo-sep: a ≠ b geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T subtype_rel: A ⊆B uall: [x:A]. B[x] guard: {T} uimplies: supposing a exists: x:A. B[x] prop: and: P ∧ Q uiff: uiff(P;Q) basic-geometry: BasicGeometry euclidean-plane: EuclideanPlane basic-geometry-: BasicGeometry- squash: T true: True geo-eq: a ≡ b not: ¬A false: False iff: ⇐⇒ Q rev_implies:  Q geo-strict-between: a-b-c
Lemmas referenced :  geo-extend-exists geo-sep-sym geo-strict-between-sep2 euclidean-plane-structure-subtype euclidean-plane-subtype basic-geometry-subtype subtype_rel_transitivity geo-sep_wf basic-geometry_wf euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf geo-strict-between_wf geo-congruent_wf geo-colinear_wf geo-between_wf geo-point_wf geo-congruent-iff-length geo-construction-unicity subtype_rel_self geo-between-sep geo-strict-between-sep3 geo-between-symmetry geo-strict-between-implies-between geo-between-outer-trans geo-between-exchange4 geo-add-length-between geo-add-length_wf squash_wf true_wf geo-length-type_wf geo-three-segment geo-colinear-cases basic-geometry-_wf stable__geo-between geo-eq_wf istype-void geo-between-trivial2 geo-between_functionality geo-eq_weakening geo-between-trivial geo-between-congruent
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin because_Cache hypothesisEquality independent_functionElimination applyEquality hypothesis instantiate isectElimination independent_isectElimination sqequalRule productElimination rename universeIsType inhabitedIsType equalitySymmetry lambdaEquality_alt imageElimination equalityTransitivity natural_numberEquality imageMemberEquality baseClosed setElimination voidElimination functionIsType

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,b',c':Point.
    (a\_b\_c  {}\mRightarrow{}  Colinear(a;c;c')  {}\mRightarrow{}  ab  \mcong{}  ab'  {}\mRightarrow{}  ac  \mcong{}  ac'  {}\mRightarrow{}  b'-a-b  {}\mRightarrow{}  c  \mneq{}  c'  {}\mRightarrow{}  a\_b'\_c')



Date html generated: 2019_10_16-PM-01_17_42
Last ObjectModification: 2019_02_16-AM-06_51_44

Theory : euclidean!plane!geometry


Home Index