Nuprl Lemma : geo-construction-unicity-from-first

e:BasicGeometry-. ∀[Q,A,X,Y:Point].  (X ≡ Y) supposing (QY ≅ QX and Q_A_X and Q_A_Y and Q ≠ A)


Proof




Definitions occuring in Statement :  basic-geometry-: BasicGeometry- geo-eq: a ≡ b geo-congruent: ab ≅ cd geo-between: a_b_c geo-sep: a ≠ b geo-point: Point uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x]
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a geo-eq: a ≡ b not: ¬A implies:  Q false: False subtype_rel: A ⊆B guard: {T} prop: basic-geometry-: BasicGeometry- and: P ∧ Q
Lemmas referenced :  geo-congruent_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-between_wf geo-sep_wf geo-point_wf geo-congruent-refl geo-five-segment geo-congruence-identity-sym geo-between-symmetry geo-inner-three-segment geo-congruent-full-symmetry
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt isect_memberFormation_alt introduction cut sqequalRule sqequalHypSubstitution lambdaEquality_alt dependent_functionElimination thin hypothesisEquality because_Cache functionIsTypeImplies inhabitedIsType universeIsType extract_by_obid isectElimination applyEquality hypothesis instantiate independent_isectElimination isect_memberEquality_alt isectIsTypeImplies voidElimination productElimination

Latex:
\mforall{}e:BasicGeometry-.  \mforall{}[Q,A,X,Y:Point].    (X  \mequiv{}  Y)  supposing  (QY  \mcong{}  QX  and  Q\_A\_X  and  Q\_A\_Y  and  Q  \mneq{}  A)



Date html generated: 2019_10_16-PM-01_16_11
Last ObjectModification: 2019_01_03-PM-02_02_06

Theory : euclidean!plane!geometry


Home Index