---

Step * of Lemma geo-midpoint-diagonals-congruent

No Annotations
∀e:BasicGeometry. ∀A,P,Q,p,q:Point.  (p=A=P ⇒ q=A=Q ⇒ PQ ≅ pq)
BY
{ (Unfold `geo-midpoint` 0
   THEN Auto
   THEN (gSeparatedCases' ⌜A⌝ ⌜P⌝⋅ THENA Auto)
   THEN (gSeparatedCases' ⌜A⌝ ⌜Q⌝⋅ THENA Auto)) }

1
1. e : BasicGeometry
2. A : Point
3. P : Point
4. Q : Point
5. p : Point
6. q : Point
7. B(pAP)
8. pA ≅ AP
9. B(qAQ)
10. qA ≅ AQ
11. A # P
12. A # Q
⊢ PQ ≅ pq

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}A,P,Q,p,q:Point.    (p=A=P  {}\mRightarrow{}  q=A=Q  {}\mRightarrow{}  PQ  \mcong{}  pq)


By

---

Latex:
(Unfold  `geo-midpoint`  0
  THEN  Auto
  THEN  (gSeparatedCases'  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}P\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gSeparatedCases'  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}Q\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index