### Nuprl Lemma : eu-seg-extend_functionality

`∀e:EuclideanPlane. ∀[s1,s2:ProperSegment]. ∀[t1,t2:Segment].  (s1 + t1 ≡ s2 + t2) supposing (t1 ≡ t2 and s1 ≡ s2)`

Proof

Definitions occuring in Statement :  eu-seg-extend: `s + t` eu-seg-congruent: `s1 ≡ s2` eu-proper-segment: `ProperSegment` eu-segment: `Segment` euclidean-plane: `EuclideanPlane` uimplies: `b 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]` uimplies: `b supposing a` member: `t ∈ T` euclidean-plane: `EuclideanPlane` subtype_rel: `A ⊆r B` eu-proper-segment: `ProperSegment` sq_stable: `SqStable(P)` implies: `P `` Q` euclidean-axioms: `euclidean-axioms(e)` and: `P ∧ Q` squash: `↓T` prop: `ℙ` not: `¬A` false: `False` eu-seg-extend: `s + t` eu-seg-congruent: `s1 ≡ s2` eu-seg2: `s.2` eu-seg1: `s.1` pi1: `fst(t)` pi2: `snd(t)` eu-seg-proper: `proper(s)` eu-congruent: `ab=cd` record-select: `r.x`
Lemmas referenced :  eu-congruent-symmetry eu-congruent-transitivity eu-three-segment eu-congruent_wf eu-between-eq_wf and_wf eu-extend_wf not_wf eu-seg2_wf eu-seg1_wf eu-point_wf equal_wf euclidean-plane_wf eu-segment_wf eu-seg-congruent_wf eu-proper-segment_wf eu-seg-extend_wf sq_stable_eu-seg-congruent
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut hypothesisEquality sqequalHypSubstitution setElimination thin rename lemma_by_obid dependent_functionElimination isectElimination hypothesis applyEquality lambdaEquality sqequalRule independent_functionElimination introduction productElimination imageMemberEquality baseClosed imageElimination dependent_set_memberEquality because_Cache equalityEquality equalityTransitivity equalitySymmetry independent_isectElimination

Latex:
\mforall{}e:EuclideanPlane
\mforall{}[s1,s2:ProperSegment].  \mforall{}[t1,t2:Segment].    (s1  +  t1  \mequiv{}  s2  +  t2)  supposing  (t1  \mequiv{}  t2  and  s1  \mequiv{}  s2)

Date html generated: 2016_05_18-AM-06_37_10
Last ObjectModification: 2016_01_16-PM-10_31_56

Theory : euclidean!geometry

Home Index