Nuprl Lemma : line-sep-from-point-triangle_wf

g:ProjectivePlane. ∀l:Line. ∀a,b,c:Point.  (l ≠ (a;b;c) ∈ ℙ)


Proof




Definitions occuring in Statement :  line-sep-from-point-triangle: l ≠ (a;b;c) projective-plane: ProjectivePlane pgeo-line: Line pgeo-point: Point prop: all: x:A. B[x] member: t ∈ T
Definitions unfolded in proof :  so_apply: x[s] and: P ∧ Q prop: so_lambda: λ2x.t[x] uimplies: supposing a guard: {T} subtype_rel: A ⊆B uall: [x:A]. B[x] line-sep-from-point-triangle: l ≠ (a;b;c) member: t ∈ T all: x:A. B[x]
Lemmas referenced :  point-triangle_wf pgeo-plsep_wf pgeo-point_wf pgeo-primitives_wf projective-plane-structure_wf projective-plane-structure-complete_wf projective-plane_wf subtype_rel_transitivity projective-plane-subtype projective-plane-structure-complete_subtype projective-plane-structure_subtype pgeo-line_wf all_wf
Rules used in proof :  dependent_functionElimination productEquality because_Cache lambdaEquality independent_isectElimination instantiate hypothesis applyEquality hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction sqequalRule cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}l:Line.  \mforall{}a,b,c:Point.    (l  \mneq{}  P\mDelta{}(a;b;c)  \mmember{}  \mBbbP{})



Date html generated: 2018_05_22-PM-00_50_23
Last ObjectModification: 2017_12_01-PM-03_12_06

Theory : euclidean!plane!geometry


Home Index