Nuprl Lemma : geo-congruent-functionality-lemma
∀g:EuclideanPlane
((∀a,b,c:Point. (a ≡ b ⇒ ac ≅ bc))
⇒ (∀a1,a2,b1,b2,c1,c2,d1,d2:Point. (a1 ≡ a2 ⇒ b1 ≡ b2 ⇒ c1 ≡ c2 ⇒ d1 ≡ d2 ⇒ a1b1 ≅ c1d1 ⇒ a2b2 ≅ c2d2)))
Proof
Definitions occuring in Statement :
euclidean-plane: EuclideanPlane,
geo-eq: a ≡ b,
geo-congruent: ab ≅ cd,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
guard: {T},
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
and: P ∧ Q,
subtype_rel: A ⊆r B,
prop: ℙ
Latex:
\mforall{}g:EuclideanPlane
((\mforall{}a,b,c:Point. (a \mequiv{} b {}\mRightarrow{} ac \mcong{} bc))
{}\mRightarrow{} (\mforall{}a1,a2,b1,b2,c1,c2,d1,d2:Point.
(a1 \mequiv{} a2 {}\mRightarrow{} b1 \mequiv{} b2 {}\mRightarrow{} c1 \mequiv{} c2 {}\mRightarrow{} d1 \mequiv{} d2 {}\mRightarrow{} a1b1 \mcong{} c1d1 {}\mRightarrow{} a2b2 \mcong{} c2d2)))
Date html generated:
2020_05_20-AM-09_45_37
Last ObjectModification:
2020_01_27-PM-03_42_20
Theory : euclidean!plane!geometry
Home
Index