---

Step * of Lemma Euclid-drop-perp-0-ext

No Annotations
∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a # b} . ∀c:Point.
  ∃x:Point. (∃p:Point [(Colinear(p;x;c) ∧ ab  ⊥p px ∧ x # ab ∧ x # c)])
BY
{ Extract of Obid: Euclid-drop-perp-0
  not unfolding  sympoint geo-M geo-SS geo-SCO geo-SCS geo-CC
  finishing with (RepUR ``let`` 0 THEN Auto)
  normalizes to:
  
  λe,a,b,c. if M(a;b;c)
           then let a' = SymmetricPoint(a;c) in
                 let x = SCO(b;a;c;a') in
                 let y = SCS(b;a;c;a') in
                 let u = CC(x;y;y;x) in
                 let v = CC(y;x;x;y) in
                 if M(u;v;c) then <u, geo-SS(e;y;x;v;u)> else <v, geo-SS(e;x;y;u;v)> fi 
           else let b' = SymmetricPoint(b;c) in
                 let x = SCO(a;b;c;b') in
                 let y = SCS(a;b;c;b') in
                 let u = CC(x;y;y;x) in
                 let v = CC(y;x;x;y) in
                 if M(u;v;c) then <u, geo-SS(e;y;x;v;u)> else <v, geo-SS(e;x;y;u;v)> fi 
           fi  }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .  \mforall{}c:Point.
    \mexists{}x:Point.  (\mexists{}p:Point  [(Colinear(p;x;c)  \mwedge{}  ab    \mbot{}p  px  \mwedge{}  x  \#  ab  \mwedge{}  x  \#  c)])


By

---

Latex:
Extract  of  Obid:  Euclid-drop-perp-0
not  unfolding    sympoint  geo-M  geo-SS  geo-SCO  geo-SCS  geo-CC
finishing  with  (RepUR  ``let``  0  THEN  Auto)
normalizes  to:

\mlambda{}e,a,b,c.  if  M(a;b;c)
                  then  let  a'  =  SymmetricPoint(a;c)  in
                              let  x  =  SCO(b;a;c;a')  in
                              let  y  =  SCS(b;a;c;a')  in
                              let  u  =  CC(x;y;y;x)  in
                              let  v  =  CC(y;x;x;y)  in
                              if  M(u;v;c)  then  <u,  geo-SS(e;y;x;v;u)>  else  <v,  geo-SS(e;x;y;u;v)>  fi 
                  else  let  b'  =  SymmetricPoint(b;c)  in
                              let  x  =  SCO(a;b;c;b')  in
                              let  y  =  SCS(a;b;c;b')  in
                              let  u  =  CC(x;y;y;x)  in
                              let  v  =  CC(y;x;x;y)  in
                              if  M(u;v;c)  then  <u,  geo-SS(e;y;x;v;u)>  else  <v,  geo-SS(e;x;y;u;v)>  fi 
                  fi 

---

Home Index