### Nuprl Lemma : eu-extend-equal-iff-congruent

e:EuclideanPlane
∀[a,b,c,d,c',d':Point].  uiff((extend ab by cd) (extend ab by c'd') ∈ Point;cd=c'd') supposing ¬(a b ∈ Point)

Proof

Definitions occuring in Statement :  euclidean-plane: EuclideanPlane eu-extend: (extend ab by cd) eu-congruent: ab=cd eu-point: Point uiff: uiff(P;Q) uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] not: ¬A equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T not: ¬A implies:  Q false: False euclidean-plane: EuclideanPlane prop: sq_stable: SqStable(P) and: P ∧ Q uiff: uiff(P;Q) squash: T cand: c∧ B
Lemmas referenced :  eu-point_wf sq_stable__uiff equal_wf eu-extend_wf not_wf eu-congruent_wf sq_stable__equal sq_stable__eu-congruent eu-extend-property eu-between-eq_wf euclidean-plane_wf eu-congruent-symmetry and_wf eu-congruent-transitivity eu-congruent-refl eu-five-segment eu-congruence-identity eu-three-segment
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination equalityEquality extract_by_obid isectElimination setElimination rename hypothesis because_Cache dependent_set_memberEquality independent_functionElimination productElimination independent_pairFormation axiomEquality productEquality equalityTransitivity equalitySymmetry imageMemberEquality baseClosed imageElimination independent_isectElimination applyEquality setEquality hyp_replacement Error :applyLambdaEquality

Latex:
\mforall{}e:EuclideanPlane
\mforall{}[a,b,c,d,c',d':Point].    uiff((extend  ab  by  cd)  =  (extend  ab  by  c'd');cd=c'd')  supposing  \mneg{}(a  =  b)

Date html generated: 2016_10_26-AM-07_41_10
Last ObjectModification: 2016_07_12-AM-08_07_21

Theory : euclidean!geometry

Home Index