Nuprl Lemma : Euclid-Prop2-lemma-ext
∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀v:Point. (∃x:Point [ax ≅ bv])
Proof
Definitions occuring in Statement :
euclidean-plane: EuclideanPlane,
geo-congruent: ab ≅ cd,
geo-sep: a ≠ b,
geo-point: Point,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
set: {x:A| B[x]}
Definitions unfolded in proof :
member: t ∈ T,
eqtri: Δ(a;b),
prop2-lemma: lemma2(a;b;c),
let: let,
Euclid-Prop2-lemma,
sq_stable__and,
sq_stable__geo-congruent,
sq_stable__geo-left,
Euclid-Prop1-left-ext,
extend-using-SC
Lemmas referenced :
Euclid-Prop2-lemma,
sq_stable__and,
sq_stable__geo-congruent,
sq_stable__geo-left,
Euclid-Prop1-left-ext,
extend-using-SC
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a:Point. \mforall{}b:\{b:Point| a \mneq{} b\} . \mforall{}v:Point. (\mexists{}x:Point [ax \mcong{} bv])
Date html generated:
2019_10_16-PM-01_15_58
Last ObjectModification:
2019_09_27-PM-04_45_54
Theory : euclidean!plane!geometry
Home
Index