---

Step * 1 1 of Lemma eu-seg-extend_functionality


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
21. ¬(s1.1 = s1.2 ∈ Point)
22. ¬(s2.1 = s2.2 ∈ Point)
23. v : Point@i
24. (extend s1.1s1.2 by t1.1t1.2) = v ∈ Point@i
25. v1 : Point@i
26. (extend s2.1s2.2 by t2.1t2.2) = v1 ∈ Point@i
⊢ (s1.1_s1.2_v ∧ s1.2v=t1.1t1.2) ⇒ (s2.1_s2.2_v1 ∧ s2.2v1=t2.1t2.2) ⇒ s1.1v=s2.1v1
BY
{ Auto }

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
21. ¬(s1.1 = s1.2 ∈ Point)
22. ¬(s2.1 = s2.2 ∈ Point)
23. v : Point@i
24. (extend s1.1s1.2 by t1.1t1.2) = v ∈ Point@i
25. v1 : Point@i
26. (extend s2.1s2.2 by t2.1t2.2) = v1 ∈ Point@i
27. s1.1_s1.2_v@i
28. s1.2v=t1.1t1.2@i
29. s2.1_s2.2_v1@i
30. s2.2v1=t2.1t2.2@i
⊢ s1.1v=s2.1v1

---

Latex:

---

Latex:

1.  e  :  EuclideanStructure@i'
2.  \mforall{}[a,b:Point].    ab=ba@i'
3.  \mforall{}[a,b,p,q,r,s:Point].    (pq=rs)  supposing  (ab=rs  and  ab=pq)@i'
4.  \mforall{}[a,b,c:Point].    a  =  b  supposing  ab=cc@i'
5.  \mforall{}[q:Point].  \mforall{}[a:\{a:Point|  \mneg{}(q  =  a)\}  ].  \mforall{}[b,c:Point].
          (q\_a\_(extend  qa  by  bc)  \mwedge{}  a(extend  qa  by  bc)=bc)@i'
6.  \mforall{}[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  (\mneg{}(a  =  b)))@i'
7.  \mforall{}[a,b:Point].    (\mneg{}a-b-a)@i'
8.  \mforall{}[a,b:Point].  \mforall{}[c:\{c:Point|  \mneg{}Colinear(a;b;c)\}  ].  \mforall{}[p:\{p:Point|  a-p-c\}  ].  \mforall{}[q:\{q:Point|  b\_q\_c\}  ].
          let  x  =  eu-inner-pasch(e;a;b;c;p;q)  in
                  p-x-b  \mwedge{}  q-x-a@i'
9.  \mforall{}[a,b,p,q,r:Point].    (Colinear(p;q;r))  supposing  (ra=rb  and  qa=qb  and  pa=pb  and  (\mneg{}(a  =  b)))@i'
10.  \mforall{}[a,b:Point].  \mforall{}[c:\{c:Point|  \mneg{}Colinear(a;b;c)\}  ].    let  x  =  middle(a;b;c)  in  ax=bx  \mwedge{}  ax=cx@i'
11.  \mforall{}[a,b:Point].  \mforall{}[x:\{x:Point|  a\_x\_b\}  ].  \mforall{}[y:\{y:Point|  a\_b\_y\}  ].  \mforall{}[p:\{p:Point|  ap=ax\}  ].
        \mforall{}[q:\{q:Point|  aq=ay  \mwedge{}  (\mneg{}(q  =  p))\}  ].
            let  uv  =  intersect  pq  (at  radius  xy)  with  Oab    in
                    afst(uv)=ab
                    \mwedge{}  asnd(uv)=ab
                    \mwedge{}  p\_fst(uv)\_q
                    \mwedge{}  snd(uv)\_p\_q
                    \mwedge{}  \mneg{}((fst(uv))  =  (snd(uv)))  supposing  \mneg{}(x  =  b)@i'
12.  \mforall{}[a,b,c:Point].    c-b-a  supposing  a-b-c@i'
13.  \mforall{}[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  \mequiv{}  s2
19.  t1  \mequiv{}  t2
20.  e  \mmember{}  EuclideanPlane
21.  \mneg{}(s1.1  =  s1.2)
22.  \mneg{}(s2.1  =  s2.2)
23.  v  :  Point@i
24.  (extend  s1.1s1.2  by  t1.1t1.2)  =  v@i
25.  v1  :  Point@i
26.  (extend  s2.1s2.2  by  t2.1t2.2)  =  v1@i
\mvdash{}  (s1.1\_s1.2\_v  \mwedge{}  s1.2v=t1.1t1.2)  {}\mRightarrow{}  (s2.1\_s2.2\_v1  \mwedge{}  s2.2v1=t2.1t2.2)  {}\mRightarrow{}  s1.1v=s2.1v1


By

---

Latex:
Auto

---

Home Index