Nuprl Lemma : geo-same-line-symmetry

[e:BasicGeometry]. ∀[a:Point]. ∀[b:{b:Point| a ≠ b} ]. ∀[c:Point]. ∀[d:{d:Point| c ≠ d} ].
  (line(a;b)=line(c;d)  line(c;d)=line(a;b))


Proof




Definitions occuring in Statement :  geo-same-line: line(a;b)=line(c;d) basic-geometry: BasicGeometry geo-sep: a ≠ b geo-point: Point uall: [x:A]. B[x] implies:  Q set: {x:A| B[x]} 
Definitions unfolded in proof :  so_apply: x[s] so_lambda: λ2x.t[x] uimplies: supposing a guard: {T} subtype_rel: A ⊆B false: False not: ¬A geo-colinear: Colinear(a;b;c) and: P ∧ Q geo-same-line: line(a;b)=line(c;d) prop: squash: T sq_stable: SqStable(P) implies:  Q member: t ∈ T uall: [x:A]. B[x] all: x:A. B[x] basic-geometry: BasicGeometry subtract: m cons: [a b] select: L[n] true: True less_than: a < b less_than': less_than'(a;b) le: A ≤ B lelt: i ≤ j < k int_seg: {i..j-} l_all: (∀x∈L.P[x]) geo-colinear-set: geo-colinear-set(e; L) so_apply: x[s1;s2;s3] top: Top so_lambda: so_lambda(x,y,z.t[x; y; z]) append: as bs or: P ∨ Q rev_implies:  Q iff: ⇐⇒ Q exists: x:A. B[x] cand: c∧ B
Lemmas referenced :  geo-sep_wf geo-point_wf set_wf Error :basic-geo-primitives_wf,  Error :basic-geo-structure_wf,  basic-geometry_wf subtype_rel_transitivity basic-geometry-subtype geo-between_wf not_wf geo-same-line_wf squash_wf sq_stable__colinear geo-colinear_wf sq_stable__and lelt_wf false_wf length_of_nil_lemma length_of_cons_lemma list_ind_nil_lemma list_ind_cons_lemma geo-colinear-is-colinear-set exists_wf equal_wf l_member_wf cons_member nil_wf cons_wf geo-colinear-append
Rules used in proof :  voidElimination isect_memberEquality independent_isectElimination instantiate applyEquality productEquality because_Cache independent_pairEquality productElimination dependent_functionElimination lambdaEquality isectElimination extract_by_obid imageElimination hypothesis baseClosed hypothesisEquality imageMemberEquality sqequalRule independent_functionElimination sqequalHypSubstitution rename thin setElimination lambdaFormation cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution natural_numberEquality dependent_set_memberEquality voidEquality inrFormation inlFormation independent_pairFormation dependent_pairFormation

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[a:Point].  \mforall{}[b:\{b:Point|  a  \mneq{}  b\}  ].  \mforall{}[c:Point].  \mforall{}[d:\{d:Point|  c  \mneq{}  d\}  ].
    (line(a;b)=line(c;d)  {}\mRightarrow{}  line(c;d)=line(a;b))



Date html generated: 2017_10_02-PM-06_22_46
Last ObjectModification: 2017_08_05-PM-04_17_00

Theory : euclidean!plane!geometry


Home Index