Nuprl Lemma : cong-angle-out-aux-weak

g:HeytingGeometry. ∀a,b,c,d,e,f,a',c',d',f':Point.
  (abc ≅a def  out(b a'a)  out(b c'c)  out(e d'd)  out(e f'f)  ba' ≅ ed'  bc' ≅ ef'  a'c' ≅ d'f')


Proof




Definitions occuring in Statement :  heyting-geometry: HeytingGeometry geo-out: out(p ab) geo-cong-angle: abc ≅a xyz geo-congruent: ab ≅ cd geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q geo-cong-angle: abc ≅a xyz and: P ∧ Q exists: x:A. B[x] member: t ∈ T subtype_rel: A ⊆B uall: [x:A]. B[x] guard: {T} uimplies: supposing a heyting-geometry: HeytingGeometry prop: geo-out: out(p ab) geo-colinear-set: geo-colinear-set(e; L) l_all: (∀x∈L.P[x]) top: Top int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A less_than: a < b squash: T true: True select: L[n] cons: [a b] subtract: m cand: c∧ B iff: ⇐⇒ Q rev_implies:  Q or: P ∨ Q append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] uiff: uiff(P;Q)
Lemmas referenced :  geo-between-out euclidean-plane-subtype-basic heyting-geometry-subtype subtype_rel_transitivity heyting-geometry_wf euclidean-plane_wf basic-geometry_wf geo-sep-sym geo-between-sep geo-out_transitivity geo-out_inversion geo-congruent_wf euclidean-plane-structure-subtype euclidean-plane-subtype euclidean-plane-structure_wf geo-primitives_wf geo-out_wf geo-cong-angle_wf geo-point_wf geo-out-cong-cong geo-colinear-five-segment geo-colinear-is-colinear-set geo-out-colinear length_of_cons_lemma istype-void length_of_nil_lemma istype-false istype-le istype-less_than oriented-colinear-append euclidean-plane-subtype-oriented oriented-plane_wf cons_wf nil_wf cons_member l_member_wf geo-sep_wf geo-between-implies-colinear list_ind_cons_lemma list_ind_nil_lemma geo-congruent-iff-length geo-length-flip
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalHypSubstitution productElimination thin cut introduction extract_by_obid dependent_functionElimination hypothesisEquality applyEquality hypothesis instantiate isectElimination independent_isectElimination sqequalRule independent_functionElimination because_Cache universeIsType inhabitedIsType isect_memberEquality_alt voidElimination dependent_set_memberEquality_alt natural_numberEquality independent_pairFormation imageMemberEquality baseClosed productIsType dependent_pairFormation_alt inlFormation_alt inrFormation_alt equalityIsType1 equalityTransitivity equalitySymmetry

Latex:
\mforall{}g:HeytingGeometry.  \mforall{}a,b,c,d,e,f,a',c',d',f':Point.
    (abc  \mcong{}\msuba{}  def
    {}\mRightarrow{}  out(b  a'a)
    {}\mRightarrow{}  out(b  c'c)
    {}\mRightarrow{}  out(e  d'd)
    {}\mRightarrow{}  out(e  f'f)
    {}\mRightarrow{}  ba'  \mcong{}  ed'
    {}\mRightarrow{}  bc'  \mcong{}  ef'
    {}\mRightarrow{}  a'c'  \mcong{}  d'f')



Date html generated: 2019_10_16-PM-02_08_01
Last ObjectModification: 2018_11_07-PM-01_09_08

Theory : euclidean!plane!geometry


Home Index