Step
*
1
1
1
1
of Lemma
hp-angle-sum-eq3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. ijk ≅a i'j'k'
22. p1 : Point
23. p2 : Point
24. d1 : Point
25. f1 : Point
26. abc ≅a ijp1
27. kjp1 ≅a xyz
28. B(jp2p1)
29. out(j id1)
30. out(j kf1)
31. d1-p2-f1
32. p : Point
33. p' : Point
34. d' : Point
35. f' : Point
36. a'b'c' ≅a i'j'p
37. k'j'p ≅a x'y'z'
38. B(j'p'p)
39. out(j' i'd')
40. out(j' k'f')
41. d'-p'-f'
42. a # bc
43. i # jk
44. A1 : Point
45. d1-j-A1 ∧ jA1 ≅ OX
46. B1 : Point
47. f1-j-B1 ∧ jB1 ≅ OX
48. A2 : Point
49. d'-j'-A2 ∧ j'A2 ≅ OX
50. B2 : Point
51. f'-j'-B2 ∧ j'B2 ≅ OX
52. C1 : Point
53. A1-j-C1 ∧ jC1 ≅ OX
54. D1 : Point
55. B1-j-D1 ∧ jD1 ≅ OX
56. C2 : Point
57. A2-j'-C2 ∧ j'C2 ≅ OX
58. D2 : Point
59. B2-j'-D2 ∧ j'D2 ≅ OX
⊢ xyz ≅a x'y'z'
BY
{ ((Assert d1 # jf1 BY
(InstLemma `out-preserves-lsep` [⌜e⌝;⌜j⌝;⌜i⌝;⌜k⌝;⌜d1⌝;⌜f1⌝]⋅ THEN Auto))
THEN (Assert out(j d1C1) BY
(InstLemma `geo-out-if-between` [⌜e⌝;⌜j⌝;⌜d1⌝;⌜C1⌝;⌜A1⌝]⋅ THEN Auto))
THEN (Assert out(j f1D1) BY
(InstLemma `geo-out-if-between` [⌜e⌝;⌜j⌝;⌜f1⌝;⌜D1⌝;⌜B1⌝]⋅ THEN Auto))) }
1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. ijk ≅a i'j'k'
22. p1 : Point
23. p2 : Point
24. d1 : Point
25. f1 : Point
26. abc ≅a ijp1
27. kjp1 ≅a xyz
28. B(jp2p1)
29. out(j id1)
30. out(j kf1)
31. d1-p2-f1
32. p : Point
33. p' : Point
34. d' : Point
35. f' : Point
36. a'b'c' ≅a i'j'p
37. k'j'p ≅a x'y'z'
38. B(j'p'p)
39. out(j' i'd')
40. out(j' k'f')
41. d'-p'-f'
42. a # bc
43. i # jk
44. A1 : Point
45. d1-j-A1 ∧ jA1 ≅ OX
46. B1 : Point
47. f1-j-B1 ∧ jB1 ≅ OX
48. A2 : Point
49. d'-j'-A2 ∧ j'A2 ≅ OX
50. B2 : Point
51. f'-j'-B2 ∧ j'B2 ≅ OX
52. C1 : Point
53. A1-j-C1 ∧ jC1 ≅ OX
54. D1 : Point
55. B1-j-D1 ∧ jD1 ≅ OX
56. C2 : Point
57. A2-j'-C2 ∧ j'C2 ≅ OX
58. D2 : Point
59. B2-j'-D2 ∧ j'D2 ≅ OX
60. d1 # jf1
61. out(j d1C1)
62. out(j f1D1)
⊢ xyz ≅a x'y'z'
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc \mcong{}\msuba{} a'b'c'
21. ijk \mcong{}\msuba{} i'j'k'
22. p1 : Point
23. p2 : Point
24. d1 : Point
25. f1 : Point
26. abc \mcong{}\msuba{} ijp1
27. kjp1 \mcong{}\msuba{} xyz
28. B(jp2p1)
29. out(j id1)
30. out(j kf1)
31. d1-p2-f1
32. p : Point
33. p' : Point
34. d' : Point
35. f' : Point
36. a'b'c' \mcong{}\msuba{} i'j'p
37. k'j'p \mcong{}\msuba{} x'y'z'
38. B(j'p'p)
39. out(j' i'd')
40. out(j' k'f')
41. d'-p'-f'
42. a \# bc
43. i \# jk
44. A1 : Point
45. d1-j-A1 \mwedge{} jA1 \mcong{} OX
46. B1 : Point
47. f1-j-B1 \mwedge{} jB1 \mcong{} OX
48. A2 : Point
49. d'-j'-A2 \mwedge{} j'A2 \mcong{} OX
50. B2 : Point
51. f'-j'-B2 \mwedge{} j'B2 \mcong{} OX
52. C1 : Point
53. A1-j-C1 \mwedge{} jC1 \mcong{} OX
54. D1 : Point
55. B1-j-D1 \mwedge{} jD1 \mcong{} OX
56. C2 : Point
57. A2-j'-C2 \mwedge{} j'C2 \mcong{} OX
58. D2 : Point
59. B2-j'-D2 \mwedge{} j'D2 \mcong{} OX
\mvdash{} xyz \mcong{}\msuba{} x'y'z'
By
Latex:
((Assert d1 \# jf1 BY
(InstLemma `out-preserves-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}f1\mkleeneclose{}]\mcdot{} THEN Auto))
THEN (Assert out(j d1C1) BY
(InstLemma `geo-out-if-between` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}C1\mkleeneclose{};\mkleeneopen{}A1\mkleeneclose{}]\mcdot{} THEN Auto))
THEN (Assert out(j f1D1) BY
(InstLemma `geo-out-if-between` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}f1\mkleeneclose{};\mkleeneopen{}D1\mkleeneclose{};\mkleeneopen{}B1\mkleeneclose{}]\mcdot{} THEN Auto)))
Home
Index