### Nuprl Lemma : eu-conga-to-cong3

`∀E:EuclideanPlane. ∀a,b,c,d,e,f:Point.`
`  (abc = def `` (∃a',c',d',f':Point. (out(b a'a) ∧ out(b cc') ∧ out(e d'd) ∧ out(e ff') ∧ Cong3(a'bc',d'ef'))))`

Proof

Definitions occuring in Statement :  eu-out: `out(p ab)` eu-cong-tri: `Cong3(abc,a'b'c')` eu-cong-angle: `abc = xyz` euclidean-plane: `EuclideanPlane` eu-point: `Point` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` eu-cong-angle: `abc = xyz` and: `P ∧ Q` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cand: `A c∧ B` eu-out: `out(p ab)` not: `¬A` uimplies: `b supposing a` false: `False` eu-cong-tri: `Cong3(abc,a'b'c')` uiff: `uiff(P;Q)`
Lemmas referenced :  eu-cong-angle_wf eu-point_wf euclidean-plane_wf eu-out_wf eu-cong-tri_wf exists_wf eu-between-eq_wf eu-between-eq-same equal_wf not_wf eu-congruent_wf false_wf eu-congruence-identity eu-congruent-iff-length eu-length-flip
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename productElimination dependent_pairFormation productEquality sqequalRule lambdaEquality because_Cache equalitySymmetry hyp_replacement Error :applyLambdaEquality,  independent_isectElimination independent_functionElimination voidElimination independent_pairFormation dependent_functionElimination equalityTransitivity equalityEquality universeEquality

Latex:
\mforall{}E:EuclideanPlane.  \mforall{}a,b,c,d,e,f:Point.
(abc  =  def
{}\mRightarrow{}  (\mexists{}a',c',d',f':Point.  (out(b  a'a)  \mwedge{}  out(b  cc')  \mwedge{}  out(e  d'd)  \mwedge{}  out(e  ff')  \mwedge{}  Cong3(a'bc',d'ef'))))

Date html generated: 2016_10_26-AM-07_44_48
Last ObjectModification: 2016_07_12-AM-08_13_00

Theory : euclidean!geometry

Home Index