Step
*
1
1
1
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
60. d1 # jf1
61. out(j d1C1)
62. out(j f1D1)
63. d' # j'f'
64. out(j' d'C2)
65. out(j' f'D2)
66. ∃x':Point. (((C1-x'-D1 ∧ out(j p2x')) ∧ d1jp2 ≅a C1jx') ∧ f1jp2 ≅a D1jx')
⊢ xyz ≅a x'y'z'
BY
{ (ExRepD
THEN ((gProperProlong ⌜p⌝⌜j'⌝`J1'⌜O⌝⌜X⌝⋅ THENA EAuto 1) THEN ExRepD)
THEN ((gProperProlong ⌜J1⌝⌜j'⌝`x2'⌜j⌝⌜x1⌝⋅ THENA EAuto 1) THEN ExRepD)
THEN (Assert out(j' px2) BY
(InstLemma `geo-out-if-between` [⌜e⌝;⌜j'⌝;⌜p⌝;⌜x2⌝;⌜J1⌝]⋅ 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
46. jA1 ≅ OX
47. B1 : Point
48. f1-j-B1
49. jB1 ≅ OX
50. A2 : Point
51. d'-j'-A2
52. j'A2 ≅ OX
53. B2 : Point
54. f'-j'-B2
55. j'B2 ≅ OX
56. C1 : Point
57. A1-j-C1
58. jC1 ≅ OX
59. D1 : Point
60. B1-j-D1
61. jD1 ≅ OX
62. C2 : Point
63. A2-j'-C2
64. j'C2 ≅ OX
65. D2 : Point
66. B2-j'-D2
67. j'D2 ≅ OX
68. d1 # jf1
69. out(j d1C1)
70. out(j f1D1)
71. d' # j'f'
72. out(j' d'C2)
73. out(j' f'D2)
74. x1 : Point
75. C1-x1-D1
76. out(j p2x1)
77. d1jp2 ≅a C1jx1
78. f1jp2 ≅a D1jx1
79. J1 : Point
80. p-j'-J1
81. j'J1 ≅ OX
82. x2 : Point
83. J1-j'-x2
84. j'x2 ≅ jx1
85. out(j' px2)
⊢ 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
60. d1 \# jf1
61. out(j d1C1)
62. out(j f1D1)
63. d' \# j'f'
64. out(j' d'C2)
65. out(j' f'D2)
66. \mexists{}x':Point. (((C1-x'-D1 \mwedge{} out(j p2x')) \mwedge{} d1jp2 \mcong{}\msuba{} C1jx') \mwedge{} f1jp2 \mcong{}\msuba{} D1jx')
\mvdash{} xyz \mcong{}\msuba{} x'y'z'
By
Latex:
(ExRepD
THEN ((gProperProlong \mkleeneopen{}p\mkleeneclose{}\mkleeneopen{}j'\mkleeneclose{}`J1'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{} THENA EAuto 1) THEN ExRepD)
THEN ((gProperProlong \mkleeneopen{}J1\mkleeneclose{}\mkleeneopen{}j'\mkleeneclose{}`x2'\mkleeneopen{}j\mkleeneclose{}\mkleeneopen{}x1\mkleeneclose{}\mcdot{} THENA EAuto 1) THEN ExRepD)
THEN (Assert out(j' px2) BY
(InstLemma `geo-out-if-between` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}J1\mkleeneclose{}]\mcdot{} THEN Auto)))
Home
Index