---

Step * 1 of Lemma r2-compass-compass-simple1


1. a : ℝ^2
2. b : ℝ^2
3. c : {c:ℝ^2| a ≠ c} 
4. ∀d:{d:ℝ^2| ↓∃p,q:ℝ^2. ((ab=ap ∧ (¬¬(∃w:ℝ^2. (c_w_d ∧ cw=cp)))) ∧ cd=cq ∧ (¬¬(∃w:ℝ^2. (a_w_b ∧ aw=aq))))} 
     ∃u:{u:ℝ^2| ab=au ∧ cd=cu} 
      (∃v:ℝ^2 [((ab=av ∧ cd=cv)
              ∧ ((↓∃p,q:ℝ^2
                    ((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d))) ∧ cd=cq ∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b))))
                ⇒ (r2-left(u;a;c) ∧ r2-left(v;c;a))))])
5. d : {d:ℝ^2| ↓∃p,q:ℝ^2. ((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d))) ∧ cd=cq ∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b)))} 
⊢ ∃u:ℝ^2 [(ab=au ∧ cd=cu ∧ r2-left(u;a;c))]
BY
{ InstHyp [⌜d⌝] (-2)⋅ }

1
.....wf..... 
1. a : ℝ^2
2. b : ℝ^2
3. c : {c:ℝ^2| a ≠ c} 
4. ∀d:{d:ℝ^2| ↓∃p,q:ℝ^2. ((ab=ap ∧ (¬¬(∃w:ℝ^2. (c_w_d ∧ cw=cp)))) ∧ cd=cq ∧ (¬¬(∃w:ℝ^2. (a_w_b ∧ aw=aq))))} 
     ∃u:{u:ℝ^2| ab=au ∧ cd=cu} 
      (∃v:ℝ^2 [((ab=av ∧ cd=cv)
              ∧ ((↓∃p,q:ℝ^2
                    ((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d))) ∧ cd=cq ∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b))))
                ⇒ (r2-left(u;a;c) ∧ r2-left(v;c;a))))])
5. d : {d:ℝ^2| ↓∃p,q:ℝ^2. ((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d))) ∧ cd=cq ∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b)))} 
⊢ d ∈ {d:ℝ^2| ↓∃p,q:ℝ^2. ((ab=ap ∧ (¬¬(∃w:ℝ^2. (c_w_d ∧ cw=cp)))) ∧ cd=cq ∧ (¬¬(∃w:ℝ^2. (a_w_b ∧ aw=aq))))} 

2
1. a : ℝ^2
2. b : ℝ^2
3. c : {c:ℝ^2| a ≠ c} 
4. ∀d:{d:ℝ^2| ↓∃p,q:ℝ^2. ((ab=ap ∧ (¬¬(∃w:ℝ^2. (c_w_d ∧ cw=cp)))) ∧ cd=cq ∧ (¬¬(∃w:ℝ^2. (a_w_b ∧ aw=aq))))} 
     ∃u:{u:ℝ^2| ab=au ∧ cd=cu} 
      (∃v:ℝ^2 [((ab=av ∧ cd=cv)
              ∧ ((↓∃p,q:ℝ^2
                    ((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d))) ∧ cd=cq ∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b))))
                ⇒ (r2-left(u;a;c) ∧ r2-left(v;c;a))))])
5. d : {d:ℝ^2| ↓∃p,q:ℝ^2. ((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d))) ∧ cd=cq ∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b)))} 
6. ∃u:{u:ℝ^2| ab=au ∧ cd=cu} 
    (∃v:ℝ^2 [((ab=av ∧ cd=cv)
            ∧ ((↓∃p,q:ℝ^2. ((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d))) ∧ cd=cq ∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b))))
              ⇒ (r2-left(u;a;c) ∧ r2-left(v;c;a))))])
⊢ ∃u:ℝ^2 [(ab=au ∧ cd=cu ∧ r2-left(u;a;c))]

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  c  :  \{c:\mBbbR{}\^{}2|  a  \mneq{}  c\} 
4.  \mforall{}d:\{d:\mBbbR{}\^{}2| 
              \mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2
                  ((ab=ap  \mwedge{}  (\mneg{}\mneg{}(\mexists{}w:\mBbbR{}\^{}2.  (c\_w\_d  \mwedge{}  cw=cp))))  \mwedge{}  cd=cq  \mwedge{}  (\mneg{}\mneg{}(\mexists{}w:\mBbbR{}\^{}2.  (a\_w\_b  \mwedge{}  aw=aq))))\} 
          \mexists{}u:\{u:\mBbbR{}\^{}2|  ab=au  \mwedge{}  cd=cu\} 
            (\mexists{}v:\mBbbR{}\^{}2  [((ab=av  \mwedge{}  cd=cv)
                            \mwedge{}  ((\mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2
                                        ((ab=ap  \mwedge{}  (\mdownarrow{}\mexists{}w:\mBbbR{}\^{}2.  (c\_w\_d  \mwedge{}  cw=cp  \mwedge{}  w  \mneq{}  d)))
                                        \mwedge{}  cd=cq
                                        \mwedge{}  (\mdownarrow{}\mexists{}w:\mBbbR{}\^{}2.  (a\_w\_b  \mwedge{}  aw=aq  \mwedge{}  w  \mneq{}  b))))
                                {}\mRightarrow{}  (r2-left(u;a;c)  \mwedge{}  r2-left(v;c;a))))])
5.  d  :  \{d:\mBbbR{}\^{}2| 
                \mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2
                    ((ab=ap  \mwedge{}  (\mdownarrow{}\mexists{}w:\mBbbR{}\^{}2.  (c\_w\_d  \mwedge{}  cw=cp  \mwedge{}  w  \mneq{}  d)))
                    \mwedge{}  cd=cq
                    \mwedge{}  (\mdownarrow{}\mexists{}w:\mBbbR{}\^{}2.  (a\_w\_b  \mwedge{}  aw=aq  \mwedge{}  w  \mneq{}  b)))\} 
\mvdash{}  \mexists{}u:\mBbbR{}\^{}2  [(ab=au  \mwedge{}  cd=cu  \mwedge{}  r2-left(u;a;c))]


By

---

Latex:
InstHyp  [\mkleeneopen{}d\mkleeneclose{}]  (-2)\mcdot{}

---

Home Index