---

Step * of Lemma eu-seg-extend_functionality

∀e:EuclideanPlane. ∀[s1,s2:ProperSegment]. ∀[t1,t2:Segment].  (s1 + t1 ≡ s2 + t2) supposing (t1 ≡ t2 and s1 ≡ s2)
BY
{ (Auto THEN (Assert e ∈ EuclideanPlane BY Auto) THEN D 1 THEN Unhide THEN Auto THEN D 2 THEN ExRepD) }

1
1. e : EuclideanStructure@i'
2. ∀[a,b:Point].  ab=ba@i'
3. ∀[a,b,p,q,r,s:Point].  (pq=rs) supposing (ab=rs and ab=pq)@i'
4. ∀[a,b,c:Point].  a = b ∈ Point supposing ab=cc@i'
5. ∀[q:Point]. ∀[a:{a:Point| ¬(q = a ∈ Point)} ]. ∀[b,c:Point].  (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc)@i'
6. ∀[a,b,c,d,A,B,C,D:Point].
     (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (¬(a = b ∈ Point)))@i'
7. ∀[a,b:Point].  (¬a-b-a)@i'
8. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
     let x = eu-inner-pasch(e;a;b;c;p;q) in
         p-x-b ∧ q-x-a@i'
9. ∀[a,b,p,q,r:Point].  (Colinear(p;q;r)) supposing (ra=rb and qa=qb and pa=pb and (¬(a = b ∈ Point)))@i'
10. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ].  let x = middle(a;b;c) in ax=bx ∧ ax=cx@i'
11. ∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ]. ∀[q:{q:Point| 
                                                                                            aq=ay
                                                                                            ∧ (¬(q = p ∈ Point))} ].
      let uv = intersect pq (at radius xy) with Oab  in
          afst(uv)=ab
          ∧ asnd(uv)=ab
          ∧ p_fst(uv)_q
          ∧ snd(uv)_p_q
          ∧ ¬((fst(uv)) = (snd(uv)) ∈ Point) supposing ¬(x = b ∈ Point)@i'
12. ∀[a,b,c:Point].  c-b-a supposing a-b-c@i'
13. ∀[a,b,c,d:Point].  (a-b-c) supposing (b-c-d and a-b-d)@i'
14. s1 : ProperSegment
15. s2 : ProperSegment
16. t1 : Segment
17. t2 : Segment
18. s1 ≡ s2
19. t1 ≡ t2
20. e ∈ EuclideanPlane
⊢ s1 + t1 ≡ s2 + t2

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane
    \mforall{}[s1,s2:ProperSegment].  \mforall{}[t1,t2:Segment].    (s1  +  t1  \mequiv{}  s2  +  t2)  supposing  (t1  \mequiv{}  t2  and  s1  \mequiv{}  s2)


By

---

Latex:
(Auto  THEN  (Assert  e  \mmember{}  EuclideanPlane  BY  Auto)  THEN  D  1  THEN  Unhide  THEN  Auto  THEN  D  2  THEN  ExRepD)

---

Home Index