Nuprl Lemma : congruence-preserves-lsep
∀g:EuclideanPlane. ∀a,b,c,A,B,C:Point. (ab ≅ AB ⇒ ac ≅ AC ⇒ bc ≅ BC ⇒ c # ab ⇒ (¬¬C # AB))
Proof
Definitions occuring in Statement :
euclidean-plane: EuclideanPlane,
geo-lsep: a # bc,
geo-congruent: ab ≅ cd,
geo-point: Point,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
not: ¬A,
false: False,
member: t ∈ T,
iff: P ⇐⇒ Q,
and: P ∧ Q,
basic-geometry: BasicGeometry,
uall: ∀[x:A]. B[x],
cand: A c∧ B,
uimplies: b supposing a,
prop: ℙ,
guard: {T},
rev_implies: P ⇐ Q,
subtype_rel: A ⊆r B
Lemmas referenced :
not-lsep-iff-colinear,
geo-congruent-preserves-colinear,
geo-colinear_wf,
geo-congruent_wf,
geo-colinear-symmetry,
geo-congruent-full-symmetry,
geo-lsep_wf,
euclidean-plane-structure-subtype,
euclidean-plane-subtype,
subtype_rel_transitivity,
euclidean-plane_wf,
euclidean-plane-structure_wf,
geo-primitives_wf,
istype-void,
geo-point_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
thin,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
hypothesisEquality,
hypothesis,
productElimination,
independent_functionElimination,
sqequalRule,
isectElimination,
independent_isectElimination,
because_Cache,
isectIsType,
universeIsType,
independent_pairFormation,
voidElimination,
functionIsType,
applyEquality,
instantiate,
inhabitedIsType
Latex:
\mforall{}g:EuclideanPlane. \mforall{}a,b,c,A,B,C:Point. (ab \mcong{} AB {}\mRightarrow{} ac \mcong{} AC {}\mRightarrow{} bc \mcong{} BC {}\mRightarrow{} c \# ab {}\mRightarrow{} (\mneg{}\mneg{}C \# AB))
Date html generated:
2019_10_16-PM-01_43_17
Last ObjectModification:
2018_12_11-PM-06_11_55
Theory : euclidean!plane!geometry
Home
Index