Nuprl Lemma : geo-intersect-points-iff2

∀e:EuclideanPlane. ∀p1,p2,l1,l2:Point.
  (p1p2 \/ l1l2
  ⇐⇒ p1 # p2
      ∧ l1 # l2
      ∧ (∃a,b,c,d,v:Point
          (a-v-b
          ∧ c-v-d
          ∧ Colinear(a;p1;p2)
          ∧ Colinear(b;p1;p2)
          ∧ Colinear(c;l1;l2)
          ∧ Colinear(d;l1;l2)
          ∧ a leftof cd
          ∧ b leftof dc
          ∧ c leftof ba
          ∧ d leftof ab)))


Proof



Definitions occuring in Statement :  geo-intersect-points: ab \/ cd,  euclidean-plane: EuclideanPlane,  geo-colinear: Colinear(a;b;c),  geo-strict-between: a-b-c,  geo-left: a leftof bc,  geo-sep: a # b,  geo-point: Point,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  iff: P ⇐⇒ Q,  and: P ∧ Q
Definitions unfolded in proof :  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  and: P ∧ Q,  implies: P ⇒ Q,  exists: ∃x:A. B[x],  member: t ∈ T,  cand: A c∧ B,  uall: ∀[x:A]. B[x],  subtype_rel: A ⊆r B,  prop: ℙ,  rev_implies: P ⇐ Q,  guard: {T},  uimplies: b supposing a,  geo-strict-between: a-b-c,  or: P ∨ Q
Latex:
\mforall{}e:EuclideanPlane.  \mforall{}p1,p2,l1,l2:Point.
    (p1p2  \mbackslash{}/  l1l2
    \mLeftarrow{}{}\mRightarrow{}  p1  \#  p2
            \mwedge{}  l1  \#  l2
            \mwedge{}  (\mexists{}a,b,c,d,v:Point
                    (a-v-b
                    \mwedge{}  c-v-d
                    \mwedge{}  Colinear(a;p1;p2)
                    \mwedge{}  Colinear(b;p1;p2)
                    \mwedge{}  Colinear(c;l1;l2)
                    \mwedge{}  Colinear(d;l1;l2)
                    \mwedge{}  a  leftof  cd
                    \mwedge{}  b  leftof  dc
                    \mwedge{}  c  leftof  ba
                    \mwedge{}  d  leftof  ab)))


Date html generated: 2020_05_20-AM-10_04_45
Last ObjectModification: 2019_12_31-PM-09_38_41

Theory : euclidean!plane!geometry


Home Index