Nuprl Lemma : pgeo-triangle-dual
∀pg:ProjectivePlane. ∀t:pgeo-triangle(pg).
∃t*:pgeo-triangle(pg*)
let a,b,c,s,s' = t in let lab,lbc,lca,s1,s2 = t* in a I lab ∧ b I lab ∧ b I lbc ∧ c I lbc ∧ c I lca ∧ a I lca
Proof
Definitions occuring in Statement :
pgeo-triangle: pgeo-triangle(pg),
projective-plane: ProjectivePlane,
pgeo-dual: pg*,
pgeo-incident: a I b,
spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
pgeo-triangle: pgeo-triangle(pg),
all: ∀x:A. B[x],
cand: A c∧ B,
and: P ∧ Q,
guard: {T},
implies: P ⇒ Q,
pgeo-lsep: l ≠ m,
exists: ∃x:A. B[x],
subtype_rel: A ⊆r B,
uimplies: b supposing a,
prop: ℙ,
pgeo-meet: l ∧ m,
mk-pgeo-prim: mk-pgeo-prim,
pgeo-line: Line,
pgeo-point: Point,
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
top: Top,
mk-pgeo: mk-pgeo(p; ss; por; lor; j; m; p3; l3),
pgeo-dual-prim: pg*,
pgeo-plsep: a ≠ b,
pgeo-dual: pg*,
pgeo-join: p ∨ q,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
pgeo-incident: a I b,
pgeo-psep: a ≠ b,
spreadn: let a,b,c,d,e = u in v[a; b; c; d; e]
Lemmas referenced :
projective-plane_wf,
pgeo-triangle_wf,
pgeo-psep-sym,
plsep-join-implies,
incident-join-first,
projective-plane-structure-complete_subtype,
projective-plane-subtype,
subtype_rel_transitivity,
projective-plane-structure-complete_wf,
projective-plane-structure_wf,
pgeo-plsep-cycle,
pgeo-join-plsep-sym,
pgeo-incident_wf,
projective-plane-structure_subtype,
pgeo-primitives_wf,
pgeo-join_wf,
pgeo-line_wf,
pgeo-plsep_wf,
rec_select_update_lemma,
pgeo-meet-to-point,
projective-plane-subtype-basic,
incident-join-second,
pgeo-peq_inversion,
pgeo-meet_wf,
pgeo-plsep_functionality,
pgeo-leq_weakening,
pgeo-lsep_wf,
pgeo-point_wf
Rules used in proof :
hypothesis,
hypothesisEquality,
isectElimination,
extract_by_obid,
introduction,
cut,
thin,
productElimination,
sqequalHypSubstitution,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
rename,
independent_pairFormation,
independent_functionElimination,
dependent_functionElimination,
dependent_pairFormation,
applyEquality,
instantiate,
independent_isectElimination,
sqequalRule,
because_Cache,
productEquality,
lambdaEquality,
setElimination,
setEquality,
voidEquality,
voidElimination,
isect_memberEquality,
dependent_pairEquality
Latex:
\mforall{}pg:ProjectivePlane. \mforall{}t:pgeo-triangle(pg).
\mexists{}t*:pgeo-triangle(pg*)
let a,b,c,s,s' = t in let lab,lbc,lca,s1,s2 = t* in a I lab
\mwedge{} b I lab
\mwedge{} b I lbc
\mwedge{} c I lbc
\mwedge{} c I lca
\mwedge{} a I lca
Date html generated:
2018_05_22-PM-00_51_29
Last ObjectModification:
2017_12_05-AM-11_36_54
Theory : euclidean!plane!geometry
Home
Index