Nuprl Lemma : pgeo-peq_weakening

g:ProjectivePlane. ∀l,m:Point.  ((l m ∈ Point)  l ≡ m)


Proof




Definitions occuring in Statement :  projective-plane: ProjectivePlane pgeo-peq: a ≡ b pgeo-point: Point all: x:A. B[x] implies:  Q equal: t ∈ T
Definitions unfolded in proof :  uimplies: supposing a guard: {T} subtype_rel: A ⊆B uall: [x:A]. B[x] prop: member: t ∈ T false: False pgeo-incident: b and: P ∧ Q exists: x:A. B[x] pgeo-psep: a ≠ b not: ¬A pgeo-peq: a ≡ b implies:  Q all: x:A. B[x]
Lemmas referenced :  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-point_wf equal_wf pgeo-peq_wf pgeo-psep_wf
Rules used in proof :  independent_isectElimination instantiate applyLambdaEquality equalitySymmetry hyp_replacement sqequalRule because_Cache applyEquality hypothesisEquality isectElimination extract_by_obid introduction voidElimination independent_functionElimination productElimination sqequalHypSubstitution thin hypothesis cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}l,m:Point.    ((l  =  m)  {}\mRightarrow{}  l  \mequiv{}  m)



Date html generated: 2018_05_22-PM-00_45_48
Last ObjectModification: 2017_11_27-PM-03_52_46

Theory : euclidean!plane!geometry


Home Index