Nuprl Lemma : geo-add-length_functionality_wrt_cong
∀e:BasicGeometry. ∀x,y,x',y':Length. ((x = x' ∈ Length) ⇒ (y = y' ∈ Length) ⇒ (x + y = x' + y' ∈ Length))
Proof
Definitions occuring in Statement :
geo-add-length: p + q,
geo-length-type: Length,
basic-geometry: BasicGeometry,
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
squash: ↓T,
uall: ∀[x:A]. B[x],
true: True
Lemmas referenced :
geo-add-length_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
applyEquality,
thin,
lambdaEquality_alt,
sqequalHypSubstitution,
imageElimination,
introduction,
extract_by_obid,
isectElimination,
because_Cache,
hypothesis,
equalitySymmetry,
natural_numberEquality,
sqequalRule,
imageMemberEquality,
hypothesisEquality,
baseClosed,
equalityIstype,
inhabitedIsType
Latex:
\mforall{}e:BasicGeometry. \mforall{}x,y,x',y':Length. ((x = x') {}\mRightarrow{} (y = y') {}\mRightarrow{} (x + y = x' + y'))
Date html generated:
2019_10_16-PM-01_18_53
Last ObjectModification:
2019_03_04-PM-04_54_53
Theory : euclidean!plane!geometry
Home
Index