Nuprl Lemma : angle-bisector-unique
∀e:EuclideanPlane. ∀a,b,c,a',c',x,y:Point.
(a # bc ⇒ out(b aa') ⇒ out(b cc') ⇒ a-x-c ⇒ a'-y-c' ⇒ abx ≅a cbx ⇒ a'by ≅a c'by ⇒ {out(b xy) ∧ abx ≅a a'by})
Proof
Definitions occuring in Statement :
geo-out: out(p ab),
geo-cong-angle: abc ≅a xyz,
euclidean-plane: EuclideanPlane,
geo-strict-between: a-b-c,
geo-lsep: a # bc,
geo-point: Point,
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
geo-out: out(p ab),
geo-midpoint: a=m=b,
iff: P ⇐⇒ Q,
basic-geometry-: BasicGeometry-,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
prop: ℙ,
uall: ∀[x:A]. B[x],
euclidean-plane: EuclideanPlane,
exists: ∃x:A. B[x],
basic-geometry: BasicGeometry,
cand: A c∧ B,
and: P ∧ Q,
guard: {T},
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
out-cong-angle,
out-preserves-angle-cong_1,
geo-out_transitivity,
geo-cong-angle_functionality,
geo-out_functionality,
geo-strict-between_functionality,
geo-midpoint_functionality,
at-most-one-midpoint,
geo-cong-angle-transitivity,
geo-sas2,
geo-congruent-right-comm,
geo-cong-angle-symm2,
euclidean-plane-axioms,
geo-congruent-refl,
geo-congruent-symmetry,
geo-eq_weakening,
geo-out_weakening,
geo-between-symmetry,
geo-strict-between-implies-between,
geo-out-iff-between1,
geo-strict-between-sep3,
geo-point_wf,
geo-lsep_wf,
geo-out_wf,
geo-primitives_wf,
euclidean-plane-structure_wf,
euclidean-plane_wf,
subtype_rel_transitivity,
euclidean-plane-subtype,
euclidean-plane-structure-subtype,
geo-strict-between_wf,
geo-cong-angle_wf,
geo-sep-O-X,
lsep-implies-sep,
geo-sep-sym,
geo-X_wf,
geo-O_wf,
geo-proper-extend-exists,
geo-out_inversion,
lsep-all-sym,
lsep-symmetry,
out-preserves-lsep,
geo-out-interior-point-exists
Rules used in proof :
promote_hyp,
productIsType,
independent_pairFormation,
dependent_pairFormation_alt,
inhabitedIsType,
independent_isectElimination,
instantiate,
applyEquality,
isectElimination,
universeIsType,
rename,
setElimination,
sqequalRule,
productElimination,
hypothesis,
because_Cache,
independent_functionElimination,
hypothesisEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a,b,c,a',c',x,y:Point.
(a \# bc
{}\mRightarrow{} out(b aa')
{}\mRightarrow{} out(b cc')
{}\mRightarrow{} a-x-c
{}\mRightarrow{} a'-y-c'
{}\mRightarrow{} abx \mcong{}\msuba{} cbx
{}\mRightarrow{} a'by \mcong{}\msuba{} c'by
{}\mRightarrow{} \{out(b xy) \mwedge{} abx \mcong{}\msuba{} a'by\})
Date html generated:
2019_10_29-AM-09_20_43
Last ObjectModification:
2019_10_18-PM-04_37_29
Theory : euclidean!plane!geometry
Home
Index