---

Step * 1 of Lemma geo-add-length-cancel-left

.....antecedent..... 
1. e : BasicGeometry
2. x : Base
3. x1 : Base
4. x = x1 ∈ (x,y:{p:Point| B(OXp)} //x ≡ y)
5. x ∈ {p:Point| B(OXp)} 
6. x1 ∈ {p:Point| B(OXp)} 
7. x ≡ x1
8. y : Base
9. y1 : Base
10. y = y1 ∈ (x,y:{p:Point| B(OXp)} //x ≡ y)
11. y ∈ {p:Point| B(OXp)} 
12. y1 ∈ {p:Point| B(OXp)} 
13. y ≡ y1
14. z : Base
15. z1 : Base
16. z = z1 ∈ (x,y:{p:Point| B(OXp)} //x ≡ y)
17. z ∈ {p:Point| B(OXp)} 
18. z1 ∈ {p:Point| B(OXp)} 
19. z ≡ z1
20. z + x = z + y ∈ (x,y:{p:Point| B(OXp)} //x ≡ y)
21. z + x ∈ {p:Point| B(OXp)} 
22. z + y ∈ {p:Point| B(OXp)} 
23. extend Oz by Xx ≡ extend Oz by Xy
⊢ x ≡ y
BY
{ (ThinVar `y1'
   THEN ThinVar `z1'
   THEN ThinVar `x1'
   THEN MoveToConcl (-1)
   THEN RenameTo `a' `x'
   THEN (GenConcl ⌜a = x ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto)
   THEN (RenameTo `b' `y' THEN (GenConcl ⌜b = y ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto))
   THEN RenameTo `c' `z'
   THEN (GenConcl ⌜c = z ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. e : BasicGeometry
2. x : {p:Point| B(OXp)} 
3. y : {p:Point| B(OXp)} 
4. z : {p:Point| B(OXp)} 
⊢ extend Oz by Xx ≡ extend Oz by Xy ⇒ x ≡ y

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  BasicGeometry
2.  x  :  Base
3.  x1  :  Base
4.  x  =  x1
5.  x  \mmember{}  \{p:Point|  B(OXp)\} 
6.  x1  \mmember{}  \{p:Point|  B(OXp)\} 
7.  x  \mequiv{}  x1
8.  y  :  Base
9.  y1  :  Base
10.  y  =  y1
11.  y  \mmember{}  \{p:Point|  B(OXp)\} 
12.  y1  \mmember{}  \{p:Point|  B(OXp)\} 
13.  y  \mequiv{}  y1
14.  z  :  Base
15.  z1  :  Base
16.  z  =  z1
17.  z  \mmember{}  \{p:Point|  B(OXp)\} 
18.  z1  \mmember{}  \{p:Point|  B(OXp)\} 
19.  z  \mequiv{}  z1
20.  z  +  x  =  z  +  y
21.  z  +  x  \mmember{}  \{p:Point|  B(OXp)\} 
22.  z  +  y  \mmember{}  \{p:Point|  B(OXp)\} 
23.  extend  Oz  by  Xx  \mequiv{}  extend  Oz  by  Xy
\mvdash{}  x  \mequiv{}  y


By

---

Latex:
(ThinVar  `y1'
  THEN  ThinVar  `z1'
  THEN  ThinVar  `x1'
  THEN  MoveToConcl  (-1)
  THEN  RenameTo  `a'  `x'
  THEN  (GenConcl  \mkleeneopen{}a  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RenameTo  `b'  `y'  THEN  (GenConcl  \mkleeneopen{}b  =  y\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  RenameTo  `c'  `z'
  THEN  (GenConcl  \mkleeneopen{}c  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index