---

Step * 1 of Lemma geo-add-length-assoc


1. e : BasicGeometry
2. x : {p:Point| B(OXp)} 
3. y : {p:Point| B(OXp)} 
4. z : {p:Point| B(OXp)} 
5. x1 : {p:Point| B(OXp)} 
6. y1 : {p:Point| B(OXp)} 
7. z1 : {p:Point| B(OXp)} 
8. x ≡ x1
9. y ≡ y1
10. z ≡ z1
⊢ x + y + z = x1 + y1 + z1 ∈ Length
BY
{ (Unfold `geo-add-length` 0
   THEN GeneralizeGeoExtend ⌜extend Oy by Xz⌝ `a'⋅
   THEN GeneralizeGeoExtend ⌜extend Ox1 by Xy1⌝ `b'⋅
   THEN GeneralizeGeoExtend ⌜extend Ox by Xa⌝ `c'⋅
   THEN DSetVars
   THEN ExRepD
   THEN (Assert B(OXb) BY
               Auto)
   THEN (Assert B(OXc) BY
               Auto)) }

1
1. e : BasicGeometry
2. x : Point
3. B(OXx)
4. y : Point
5. B(OXy)
6. z : Point
7. B(OXz)
8. x1 : Point
9. B(OXx1)
10. y1 : Point
11. B(OXy1)
12. z1 : Point
13. B(OXz1)
14. x ≡ x1
15. y ≡ y1
16. z ≡ z1
17. a : Point
18. B(Oya)
19. ya ≅ Xz
20. ya ≅ Xz
21. B(Oya)
22. b : Point
23. B(Ox1b)
24. x1b ≅ Xy1
25. x1b ≅ Xy1
26. B(Ox1b)
27. c : Point
28. B(Oxc)
29. xc ≅ Xa
30. xc ≅ Xa
31. B(Oxc)
32. B(OXb)
33. B(OXc)
⊢ c = extend Ob by Xz1 ∈ Length

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  \{p:Point|  B(OXp)\} 
3.  y  :  \{p:Point|  B(OXp)\} 
4.  z  :  \{p:Point|  B(OXp)\} 
5.  x1  :  \{p:Point|  B(OXp)\} 
6.  y1  :  \{p:Point|  B(OXp)\} 
7.  z1  :  \{p:Point|  B(OXp)\} 
8.  x  \mequiv{}  x1
9.  y  \mequiv{}  y1
10.  z  \mequiv{}  z1
\mvdash{}  x  +  y  +  z  =  x1  +  y1  +  z1


By

---

Latex:
(Unfold  `geo-add-length`  0
  THEN  GeneralizeGeoExtend  \mkleeneopen{}extend  Oy  by  Xz\mkleeneclose{}  `a'\mcdot{}
  THEN  GeneralizeGeoExtend  \mkleeneopen{}extend  Ox1  by  Xy1\mkleeneclose{}  `b'\mcdot{}
  THEN  GeneralizeGeoExtend  \mkleeneopen{}extend  Ox  by  Xa\mkleeneclose{}  `c'\mcdot{}
  THEN  DSetVars
  THEN  ExRepD
  THEN  (Assert  B(OXb)  BY
                          Auto)
  THEN  (Assert  B(OXc)  BY
                          Auto))

---

Home Index