Step
*
1
1
1
1
1
1
of Lemma
hp-angle-sum-subst3
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 : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x # yz
26. d' ≠ y
27. y ≠ f'
28. i ≠ j
29. j ≠ k
30. a' : Point
31. c' : Point
32. x' : Point
33. z' : Point
34. y_d'_a'
35. y_f'_c'
36. j_i_x'
37. j_k_z'
38. ya' ≅ jx'
39. yc' ≅ jz'
40. a'c' ≅ x'z'
41. d' # yf'
42. x1 : Point
43. a'-x1-c'
44. out(y p'x1)
45. d'yp' ≅a a'yx1
46. f'yp' ≅a c'yx1
47. b' : Point
48. x'-b'-z'
49. a'x1 ≅ x'b'
50. x1c' ≅ b'z'
51. x1y ≅ b'j
52. a'yx1 ≅a x'jb'
53. ya'x1 ≅a jx'b'
54. yx1a' ≅a jb'x'
55. c'yx1 ≅a z'jb'
56. yc'x1 ≅a jz'b'
57. yx1c' ≅a jb'z'
58. c ≠ b
⊢ abc ≅a a'yx1
BY
{ (InstLemma `out-preserves-angle-cong_1` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜x⌝;⌜y⌝;⌜p⌝;⌜a⌝;⌜c⌝;⌜a'⌝;⌜x1⌝]⋅ THEN Auto) }
1
.....antecedent.....
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 : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x # yz
26. d' ≠ y
27. y ≠ f'
28. i ≠ j
29. j ≠ k
30. a' : Point
31. c' : Point
32. x' : Point
33. z' : Point
34. y_d'_a'
35. y_f'_c'
36. j_i_x'
37. j_k_z'
38. ya' ≅ jx'
39. yc' ≅ jz'
40. a'c' ≅ x'z'
41. d' # yf'
42. x1 : Point
43. a'-x1-c'
44. out(y p'x1)
45. d'yp' ≅a a'yx1
46. f'yp' ≅a c'yx1
47. b' : Point
48. x'-b'-z'
49. a'x1 ≅ x'b'
50. x1c' ≅ b'z'
51. x1y ≅ b'j
52. a'yx1 ≅a x'jb'
53. ya'x1 ≅a jx'b'
54. yx1a' ≅a jb'x'
55. c'yx1 ≅a z'jb'
56. yc'x1 ≅a jz'b'
57. yx1c' ≅a jb'z'
58. c ≠ b
⊢ out(b cc)
2
.....antecedent.....
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 : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x # yz
26. d' ≠ y
27. y ≠ f'
28. i ≠ j
29. j ≠ k
30. a' : Point
31. c' : Point
32. x' : Point
33. z' : Point
34. y_d'_a'
35. y_f'_c'
36. j_i_x'
37. j_k_z'
38. ya' ≅ jx'
39. yc' ≅ jz'
40. a'c' ≅ x'z'
41. d' # yf'
42. x1 : Point
43. a'-x1-c'
44. out(y p'x1)
45. d'yp' ≅a a'yx1
46. f'yp' ≅a c'yx1
47. b' : Point
48. x'-b'-z'
49. a'x1 ≅ x'b'
50. x1c' ≅ b'z'
51. x1y ≅ b'j
52. a'yx1 ≅a x'jb'
53. ya'x1 ≅a jx'b'
54. yx1a' ≅a jb'x'
55. c'yx1 ≅a z'jb'
56. yc'x1 ≅a jz'b'
57. yx1c' ≅a jb'z'
58. c ≠ b
⊢ out(b aa)
3
.....antecedent.....
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 : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x # yz
26. d' ≠ y
27. y ≠ f'
28. i ≠ j
29. j ≠ k
30. a' : Point
31. c' : Point
32. x' : Point
33. z' : Point
34. y_d'_a'
35. y_f'_c'
36. j_i_x'
37. j_k_z'
38. ya' ≅ jx'
39. yc' ≅ jz'
40. a'c' ≅ x'z'
41. d' # yf'
42. x1 : Point
43. a'-x1-c'
44. out(y p'x1)
45. d'yp' ≅a a'yx1
46. f'yp' ≅a c'yx1
47. b' : Point
48. x'-b'-z'
49. a'x1 ≅ x'b'
50. x1c' ≅ b'z'
51. x1y ≅ b'j
52. a'yx1 ≅a x'jb'
53. ya'x1 ≅a jx'b'
54. yx1a' ≅a jb'x'
55. c'yx1 ≅a z'jb'
56. yc'x1 ≅a jz'b'
57. yx1c' ≅a jb'z'
58. c ≠ b
⊢ out(y px1)
4
.....antecedent.....
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 : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x # yz
26. d' ≠ y
27. y ≠ f'
28. i ≠ j
29. j ≠ k
30. a' : Point
31. c' : Point
32. x' : Point
33. z' : Point
34. y_d'_a'
35. y_f'_c'
36. j_i_x'
37. j_k_z'
38. ya' ≅ jx'
39. yc' ≅ jz'
40. a'c' ≅ x'z'
41. d' # yf'
42. x1 : Point
43. a'-x1-c'
44. out(y p'x1)
45. d'yp' ≅a a'yx1
46. f'yp' ≅a c'yx1
47. b' : Point
48. x'-b'-z'
49. a'x1 ≅ x'b'
50. x1c' ≅ b'z'
51. x1y ≅ b'j
52. a'yx1 ≅a x'jb'
53. ya'x1 ≅a jx'b'
54. yx1a' ≅a jb'x'
55. c'yx1 ≅a z'jb'
56. yc'x1 ≅a jz'b'
57. yx1c' ≅a jb'z'
58. c ≠ b
⊢ out(y xa')
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. p : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc \mcong{}\msuba{} xyp
19. zyp \mcong{}\msuba{} def
20. y\_p'\_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz \mcong{}\msuba{} ijk
25. x \# yz
26. d' \mneq{} y
27. y \mneq{} f'
28. i \mneq{} j
29. j \mneq{} k
30. a' : Point
31. c' : Point
32. x' : Point
33. z' : Point
34. y\_d'\_a'
35. y\_f'\_c'
36. j\_i\_x'
37. j\_k\_z'
38. ya' \mcong{} jx'
39. yc' \mcong{} jz'
40. a'c' \mcong{} x'z'
41. d' \# yf'
42. x1 : Point
43. a'-x1-c'
44. out(y p'x1)
45. d'yp' \mcong{}\msuba{} a'yx1
46. f'yp' \mcong{}\msuba{} c'yx1
47. b' : Point
48. x'-b'-z'
49. a'x1 \mcong{} x'b'
50. x1c' \mcong{} b'z'
51. x1y \mcong{} b'j
52. a'yx1 \mcong{}\msuba{} x'jb'
53. ya'x1 \mcong{}\msuba{} jx'b'
54. yx1a' \mcong{}\msuba{} jb'x'
55. c'yx1 \mcong{}\msuba{} z'jb'
56. yc'x1 \mcong{}\msuba{} jz'b'
57. yx1c' \mcong{}\msuba{} jb'z'
58. c \mneq{} b
\mvdash{} abc \mcong{}\msuba{} a'yx1
By
Latex:
(InstLemma `out-preserves-angle-cong\_1` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index