Nuprl Lemma : geo-line-eq-equiv
∀g:EuclideanPlane. EquivRel(Line;l,m.l ≡ m)
Proof
Definitions occuring in Statement : 
geo-line-eq: l ≡ m
, 
geo-line: Line
, 
euclidean-plane: EuclideanPlane
, 
equiv_rel: EquivRel(T;x,y.E[x; y])
, 
all: ∀x:A. B[x]
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
equiv_rel: EquivRel(T;x,y.E[x; y])
, 
and: P ∧ Q
, 
refl: Refl(T;x,y.E[x; y])
, 
member: t ∈ T
, 
implies: P 
⇒ Q
, 
subtype_rel: A ⊆r B
, 
uall: ∀[x:A]. B[x]
, 
guard: {T}
, 
uimplies: b supposing a
, 
cand: A c∧ B
, 
sym: Sym(T;x,y.E[x; y])
, 
prop: ℙ
, 
trans: Trans(T;x,y.E[x; y])
Lemmas referenced : 
geo-line-eq_weakening, 
geo-line_wf, 
euclidean-plane-structure-subtype, 
euclidean-plane-subtype, 
subtype_rel_transitivity, 
euclidean-plane_wf, 
euclidean-plane-structure_wf, 
geo-primitives_wf, 
geo-line-eq_inversion, 
geo-line-eq_wf, 
geo-line-eq_transitivity
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
lambdaFormation, 
independent_pairFormation, 
cut, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
dependent_functionElimination, 
thin, 
hypothesisEquality, 
because_Cache, 
independent_functionElimination, 
hypothesis, 
applyEquality, 
instantiate, 
isectElimination, 
independent_isectElimination, 
sqequalRule
Latex:
\mforall{}g:EuclideanPlane.  EquivRel(Line;l,m.l  \mequiv{}  m)
Date html generated:
2018_05_22-PM-01_02_34
Last ObjectModification:
2018_05_10-PM-04_28_36
Theory : euclidean!plane!geometry
Home
Index