---

Step * of Lemma hp-angle-sum-functionality

∀e:EuclideanPlane. ∀a,b,c,x,y,z,i,j,k,a',b',c',x',y',z',i',j',k':Point.
  (a ≡ a'
  ⇒ b ≡ b'
  ⇒ c ≡ c'
  ⇒ x ≡ x'
  ⇒ y ≡ y'
  ⇒ z ≡ z'
  ⇒ i ≡ i'
  ⇒ j ≡ j'
  ⇒ k ≡ k'
  ⇒ (abc + xyz ≅ ijk ⇐⇒ a'b'c' + x'y'z' ≅ i'j'k'))
BY
{ (Auto
   THEN (Unfold `hp-angle-sum` -1 THEN ExRepD)
   THEN (Unfold `hp-angle-sum` 0 THEN GenRepD)
   THEN (EliminatePoint (20) THENA Auto)
   THEN (EliminatePoint (21) THENA Auto)
   THEN (EliminatePoint (22) THENA Auto)
   THEN (EliminatePoint (23) THENA Auto)
   THEN (EliminatePoint (24) THENA Auto)
   THEN (EliminatePoint (25) THENA Auto)
   THEN (EliminatePoint (26) THENA Auto)
   THEN (EliminatePoint (27) THENA Auto)
   THEN (EliminatePoint (28) THENA Auto)
   THEN InstConcl [⌜p⌝;⌜p'⌝;⌜d'⌝;⌜f'⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z,i,j,k,a',b',c',x',y',z',i',j',k':Point.
    (a  \mequiv{}  a'
    {}\mRightarrow{}  b  \mequiv{}  b'
    {}\mRightarrow{}  c  \mequiv{}  c'
    {}\mRightarrow{}  x  \mequiv{}  x'
    {}\mRightarrow{}  y  \mequiv{}  y'
    {}\mRightarrow{}  z  \mequiv{}  z'
    {}\mRightarrow{}  i  \mequiv{}  i'
    {}\mRightarrow{}  j  \mequiv{}  j'
    {}\mRightarrow{}  k  \mequiv{}  k'
    {}\mRightarrow{}  (abc  +  xyz  \mcong{}  ijk  \mLeftarrow{}{}\mRightarrow{}  a'b'c'  +  x'y'z'  \mcong{}  i'j'k'))


By

---

Latex:
(Auto
  THEN  (Unfold  `hp-angle-sum`  -1  THEN  ExRepD)
  THEN  (Unfold  `hp-angle-sum`  0  THEN  GenRepD)
  THEN  (EliminatePoint  (20)  THENA  Auto)
  THEN  (EliminatePoint  (21)  THENA  Auto)
  THEN  (EliminatePoint  (22)  THENA  Auto)
  THEN  (EliminatePoint  (23)  THENA  Auto)
  THEN  (EliminatePoint  (24)  THENA  Auto)
  THEN  (EliminatePoint  (25)  THENA  Auto)
  THEN  (EliminatePoint  (26)  THENA  Auto)
  THEN  (EliminatePoint  (27)  THENA  Auto)
  THEN  (EliminatePoint  (28)  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index