Step
*
1
of Lemma
hp-angle-sum-subst2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. abc + def ≅ xyz
15. abc ≅a ijk
⊢ ijk + def ≅ xyz
BY
{ (Unfold `hp-angle-sum` 0 THEN Unfold `hp-angle-sum` -2) }
1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. ∃p,p',d',f':Point. (((abc ≅a xyp ∧ zyp ≅a def) ∧ y_p'_p) ∧ (out(y xd') ∧ out(y zf')) ∧ d'_p'_f' ∧ d' ≠ f')
15. abc ≅a ijk
⊢ ∃p,p',d',f':Point. (((ijk ≅a xyp ∧ zyp ≅a def) ∧ y_p'_p) ∧ (out(y xd') ∧ out(y zf')) ∧ d'_p'_f' ∧ d' ≠ f')
Latex:
Latex:
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. abc + def \mcong{} xyz
15. abc \mcong{}\msuba{} ijk
\mvdash{} ijk + def \mcong{} xyz
By
Latex:
(Unfold `hp-angle-sum` 0 THEN Unfold `hp-angle-sum` -2)
Home
Index