Nuprl Lemma : symmetry-preserves-congruence
∀e:BasicGeometry. ∀A,P,Q,p,q:Point. (p=A=P ⇒ q=A=Q ⇒ PQ ≅ pq)
Proof
Definitions occuring in Statement :
basic-geometry: BasicGeometry,
geo-midpoint: a=m=b,
geo-congruent: ab ≅ cd,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q
Lemmas referenced :
geo-midpoint-diagonals-congruent
Rules used in proof :
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}e:BasicGeometry. \mforall{}A,P,Q,p,q:Point. (p=A=P {}\mRightarrow{} q=A=Q {}\mRightarrow{} PQ \mcong{} pq)
Date html generated:
2019_10_16-PM-01_28_19
Last ObjectModification:
2019_08_26-PM-09_12_10
Theory : euclidean!plane!geometry
Home
Index