---

Step * 2 of Lemma geo-congruent-iff-length


1. e : BasicGeometry
2. ∀[s,t:geo-segment(e)].  uiff(geo-seg1(s)geo-seg2(s) ≅ geo-seg1(t)geo-seg2(t);|s| ≡ |t|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. |ab| = |cd| ∈ Length
8. uiff(ab ≅ cd;|ab| ≡ |cd|)
⊢ |ab| ≡ |cd|
BY
{ (EqTypeHD (-2) THENA Auto) }

1
1. e : BasicGeometry
2. ∀[s,t:geo-segment(e)].  uiff(geo-seg1(s)geo-seg2(s) ≅ geo-seg1(t)geo-seg2(t);|s| ≡ |t|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. |ab| = |cd| ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
8. [%5] : (|ab| ∈ {p:Point| O_X_p} ) ∧ (|cd| ∈ {p:Point| O_X_p} ) ∧ |ab| ≡ |cd|
9. uiff(ab ≅ cd;|ab| ≡ |cd|)
⊢ |ab| ≡ |cd|

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  \mforall{}[s,t:geo-segment(e)].    uiff(geo-seg1(s)geo-seg2(s)  \00D0  geo-seg1(t)geo-seg2(t);|s|  \mequiv{}  |t|)
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  d  :  Point
7.  |ab|  =  |cd|
8.  uiff(ab  \00D0  cd;|ab|  \mequiv{}  |cd|)
\mvdash{}  |ab|  \mequiv{}  |cd|


By

---

Latex:
(EqTypeHD  (-2)  THENA  Auto)

---

Home Index