Nuprl Lemma : geo-simple-colinear-cases
∀[e:BasicGeometry-]. ∀[a,b,c:Point].
∀X:ℙ. (Stable{X} ⇒ Colinear(a;b;c) ⇒ (a_b_c ⇒ X) ⇒ (b_c_a ⇒ X) ⇒ (c_a_b ⇒ X) ⇒ X)
Proof
Definitions occuring in Statement :
basic-geometry-: BasicGeometry-,
geo-colinear: Colinear(a;b;c),
geo-between: a_b_c,
geo-point: Point,
stable: Stable{P},
uall: ∀[x:A]. B[x],
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
guard: {T},
subtype_rel: A ⊆r B,
prop: ℙ,
member: t ∈ T,
uimplies: b supposing a,
stable: Stable{P},
implies: P ⇒ Q,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
false: False,
cand: A c∧ B,
and: P ∧ Q,
not: ¬A
Lemmas referenced :
geo-point_wf,
stable_wf,
geo-colinear_wf,
geo-primitives_wf,
euclidean-plane-structure_wf,
euclidean-plane_wf,
basic-geometry-_wf,
subtype_rel_transitivity,
basic-geometry--subtype,
euclidean-plane-subtype,
euclidean-plane-structure-subtype,
geo-between_wf,
not_wf,
geo-colinear-implies
Rules used in proof :
universeEquality,
because_Cache,
sqequalRule,
instantiate,
applyEquality,
hypothesisEquality,
isectElimination,
extract_by_obid,
introduction,
functionEquality,
thin,
independent_isectElimination,
hypothesis,
cut,
sqequalHypSubstitution,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
independent_pairFormation,
voidElimination,
independent_functionElimination,
dependent_functionElimination
Latex:
\mforall{}[e:BasicGeometry-]. \mforall{}[a,b,c:Point].
\mforall{}X:\mBbbP{}. (Stable\{X\} {}\mRightarrow{} Colinear(a;b;c) {}\mRightarrow{} (a\_b\_c {}\mRightarrow{} X) {}\mRightarrow{} (b\_c\_a {}\mRightarrow{} X) {}\mRightarrow{} (c\_a\_b {}\mRightarrow{} X) {}\mRightarrow{} X)
Date html generated:
2017_10_02-PM-04_43_38
Last ObjectModification:
2017_08_07-PM-00_24_15
Theory : euclidean!plane!geometry
Home
Index