Nuprl Lemma : mk-pgeo_wf
∀[self:ProjGeomPrimitives]. ∀[ss:∀l:Line. ∀a:Point. SqStable(a ≠ l)]. ∀[por:∀a:Point. ∀l:{l:Line| a ≠ l} . ∀m:Line.
(a ≠ m ∨ m ≠ l)].
∀[lor:∀l:Line. ∀a:{a:Point| l ≠ a} . ∀b:Point. (b ≠ l ∨ b ≠ a)].
∀[j:∀a,b:Point. (a ≠ b ⇒ (∃l:Line. (a I l ∧ b I l)))]. ∀[m:∀l,m:Line. (l ≠ m ⇒ (∃a:Point. (a I l ∧ a I m)))].
∀[p3:∀l:Line. ∃a,b,c:Point. (a I l ∧ b I l ∧ c I l ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a)]. ∀[l3:∀a:Point
∃l,m,n:Line
(a I l
∧ a I m
∧ a I n
∧ l ≠ m
∧ m ≠ n
∧ n ≠ l)].
(mk-pgeo(self; ss; por; lor; j; m; p3; l3) ∈ ProjectivePlaneStructure)
Proof
Definitions occuring in Statement :
mk-pgeo: mk-pgeo(p; ss; por; lor; j; m; p3; l3),
projective-plane-structure: ProjectivePlaneStructure,
pgeo-lpsep: a ≠ b,
pgeo-lsep: l ≠ m,
pgeo-psep: a ≠ b,
pgeo-incident: a I b,
pgeo-plsep: a ≠ b,
pgeo-primitives: ProjGeomPrimitives,
pgeo-line: Line,
pgeo-point: Point,
sq_stable: SqStable(P),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]}
Definitions unfolded in proof :
so_apply: x[s],
so_lambda: λ2x.t[x],
pgeo-lpsep: a ≠ b,
pgeo-psep: a ≠ b,
pgeo-incident: a I b,
pgeo-lsep: l ≠ m,
rev_implies: P ⇐ Q,
prop: ℙ,
not: ¬A,
iff: P ⇐⇒ Q,
pgeo-line: Line,
pgeo-point: Point,
pgeo-plsep: a ≠ b,
bfalse: ff,
eq_atom: x =a y,
top: Top,
record-select: r.x,
guard: {T},
sq_type: SQType(T),
ifthenelse: if b then t else f fi ,
uimplies: b supposing a,
and: P ∧ Q,
uiff: uiff(P;Q),
subtype_rel: A ⊆r B,
btrue: tt,
it: ⋅,
unit: Unit,
bool: 𝔹,
implies: P ⇒ Q,
all: ∀x:A. B[x],
record-update: r[x := v],
record+: record+,
projective-plane-structure: ProjectivePlaneStructure,
mk-pgeo: mk-pgeo(p; ss; por; lor; j; m; p3; l3),
member: t ∈ T,
uall: ∀[x:A]. B[x],
record: record(x.T[x]),
pgeo-primitives: ProjGeomPrimitives
Lemmas referenced :
pgeo-primitives_wf,
sq_stable_wf,
pgeo-plsep_wf,
or_wf,
pgeo-lpsep_wf,
pgeo-psep_wf,
pgeo-lsep_wf,
pgeo-incident_wf,
pgeo-line_wf,
exists_wf,
pgeo-point_wf,
all_wf,
equal_wf,
assert_of_bnot,
eqff_to_assert,
iff_weakening_uiff,
not_wf,
bnot_wf,
iff_transitivity,
rec_select_update_lemma,
subtype_base_sq,
assert_of_eq_atom,
eqtt_to_assert,
atom_subtype_base,
assert_wf,
bool_wf,
equal-wf-base,
uiff_transitivity,
eq_atom_wf,
subtype_rel_self
Rules used in proof :
rename,
setElimination,
setEquality,
functionEquality,
productEquality,
lambdaEquality,
axiomEquality,
impliesFunctionality,
independent_pairFormation,
voidEquality,
voidElimination,
isect_memberEquality,
equalitySymmetry,
equalityTransitivity,
dependent_functionElimination,
cumulativity,
instantiate,
independent_isectElimination,
productElimination,
independent_functionElimination,
atomEquality,
applyEquality,
baseClosed,
closedConclusion,
baseApply,
equalityElimination,
unionElimination,
lambdaFormation,
hypothesis,
tokenEquality,
hypothesisEquality,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
thin,
functionExtensionality,
because_Cache,
dependentIntersection_memberEquality,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
universeEquality,
dependentIntersectionEqElimination,
dependentIntersectionElimination
Latex:
\mforall{}[self:ProjGeomPrimitives]. \mforall{}[ss:\mforall{}l:Line. \mforall{}a:Point. SqStable(a \mneq{} l)]. \mforall{}[por:\mforall{}a:Point. \mforall{}l:\{l:Line|
a \mneq{} l\} .
\mforall{}m:Line.
(a \mneq{} m \mvee{} m \mneq{} l)].
\mforall{}[lor:\mforall{}l:Line. \mforall{}a:\{a:Point| l \mneq{} a\} . \mforall{}b:Point. (b \mneq{} l \mvee{} b \mneq{} a)]. \mforall{}[j:\mforall{}a,b:Point.
(a \mneq{} b
{}\mRightarrow{} (\mexists{}l:Line
(a I l \mwedge{} b I l)))].
\mforall{}[m:\mforall{}l,m:Line. (l \mneq{} m {}\mRightarrow{} (\mexists{}a:Point. (a I l \mwedge{} a I m)))]. \mforall{}[p3:\mforall{}l:Line
\mexists{}a,b,c:Point
(a I l
\mwedge{} b I l
\mwedge{} c I l
\mwedge{} a \mneq{} b
\mwedge{} b \mneq{} c
\mwedge{} c \mneq{} a)]. \mforall{}[l3:\mforall{}a:Point
\mexists{}l,m,n:Line
(a I l
\mwedge{} a I m
\mwedge{} a I n
\mwedge{} l \mneq{} m
\mwedge{} m \mneq{} n
\mwedge{} n \mneq{} l)].
(mk-pgeo(self; ss; por; lor; j; m; p3; l3) \mmember{} ProjectivePlaneStructure)
Date html generated:
2018_05_22-PM-00_27_54
Last ObjectModification:
2017_11_26-PM-02_00_22
Theory : euclidean!plane!geometry
Home
Index