Step | Hyp | Ref
| Expression |
1 | | cgraid.p |
. . . . 5
β’ π = (BaseβπΊ) |
2 | | eqid 2737 |
. . . . 5
β’
(distβπΊ) =
(distβπΊ) |
3 | | eqid 2737 |
. . . . 5
β’
(cgrGβπΊ) =
(cgrGβπΊ) |
4 | | cgraid.g |
. . . . . 6
β’ (π β πΊ β TarskiG) |
5 | 4 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β πΊ β TarskiG) |
6 | | cgraid.a |
. . . . . 6
β’ (π β π΄ β π) |
7 | 6 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β π΄ β π) |
8 | | cgraid.b |
. . . . . 6
β’ (π β π΅ β π) |
9 | 8 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β π΅ β π) |
10 | | cgraid.c |
. . . . . 6
β’ (π β πΆ β π) |
11 | 10 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β πΆ β π) |
12 | | simpllr 775 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β π₯ β π) |
13 | | simplr 768 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β π¦ β π) |
14 | | cgraid.i |
. . . . . . 7
β’ πΌ = (ItvβπΊ) |
15 | | simprlr 779 |
. . . . . . 7
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) |
16 | 1, 2, 14, 5, 9, 12, 9, 7, 15 | tgcgrcomlr 27464 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π₯(distβπΊ)π΅) = (π΄(distβπΊ)π΅)) |
17 | 16 | eqcomd 2743 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π΄(distβπΊ)π΅) = (π₯(distβπΊ)π΅)) |
18 | | simprrr 781 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)) |
19 | 18 | eqcomd 2743 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π΅(distβπΊ)πΆ) = (π΅(distβπΊ)π¦)) |
20 | | eqid 2737 |
. . . . . . . 8
β’
(LineGβπΊ) =
(LineGβπΊ) |
21 | | cgraid.k |
. . . . . . . . . . 11
β’ πΎ = (hlGβπΊ) |
22 | | simprll 778 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β π₯(πΎβπ΅)πΆ) |
23 | 1, 14, 21, 12, 11, 9, 5, 20, 22 | hlln 27591 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β π₯ β (πΆ(LineGβπΊ)π΅)) |
24 | 23 | orcd 872 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π₯ β (πΆ(LineGβπΊ)π΅) β¨ πΆ = π΅)) |
25 | 1, 20, 14, 5, 11, 9, 12, 24 | colrot1 27543 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (πΆ β (π΅(LineGβπΊ)π₯) β¨ π΅ = π₯)) |
26 | | eqid 2737 |
. . . . . . . . . 10
β’
(β€GβπΊ) =
(β€GβπΊ) |
27 | 1, 14, 21, 12, 11, 9, 5 | ishlg 27586 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π₯(πΎβπ΅)πΆ β (π₯ β π΅ β§ πΆ β π΅ β§ (π₯ β (π΅πΌπΆ) β¨ πΆ β (π΅πΌπ₯))))) |
28 | 22, 27 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π₯ β π΅ β§ πΆ β π΅ β§ (π₯ β (π΅πΌπΆ) β¨ πΆ β (π΅πΌπ₯)))) |
29 | 28 | simp3d 1145 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π₯ β (π΅πΌπΆ) β¨ πΆ β (π΅πΌπ₯))) |
30 | 29 | orcomd 870 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (πΆ β (π΅πΌπ₯) β¨ π₯ β (π΅πΌπΆ))) |
31 | | simprrl 780 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β π¦(πΎβπ΅)π΄) |
32 | 1, 14, 21, 13, 7, 9, 5 | ishlg 27586 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π¦(πΎβπ΅)π΄ β (π¦ β π΅ β§ π΄ β π΅ β§ (π¦ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπ¦))))) |
33 | 31, 32 | mpbid 231 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π¦ β π΅ β§ π΄ β π΅ β§ (π¦ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπ¦)))) |
34 | 33 | simp3d 1145 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π¦ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπ¦))) |
35 | 1, 2, 14, 26, 5, 9, 11, 12, 9, 9, 13, 7,
30, 34, 19, 15 | tgcgrsub2 27579 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (πΆ(distβπΊ)π₯) = (π¦(distβπΊ)π΄)) |
36 | 1, 2, 3, 5, 9, 11,
12, 9, 13, 7, 19, 35, 16 | trgcgr 27500 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β β¨βπ΅πΆπ₯ββ©(cgrGβπΊ)β¨βπ΅π¦π΄ββ©) |
37 | 1, 2, 14, 5, 11, 13 | axtgcgrrflx 27446 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (πΆ(distβπΊ)π¦) = (π¦(distβπΊ)πΆ)) |
38 | | cgraid.2 |
. . . . . . . . 9
β’ (π β π΅ β πΆ) |
39 | 38 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β π΅ β πΆ) |
40 | 1, 20, 14, 5, 9, 11, 12, 3, 9, 13, 2, 13, 7, 11, 25, 36, 18, 37, 39 | tgfscgr 27552 |
. . . . . . 7
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π₯(distβπΊ)π¦) = (π΄(distβπΊ)πΆ)) |
41 | 1, 2, 14, 5, 12, 13, 7, 11, 40 | tgcgrcomlr 27464 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (π¦(distβπΊ)π₯) = (πΆ(distβπΊ)π΄)) |
42 | 41 | eqcomd 2743 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (πΆ(distβπΊ)π΄) = (π¦(distβπΊ)π₯)) |
43 | 1, 2, 3, 5, 7, 9, 11, 12, 9, 13, 17, 19, 42 | trgcgr 27500 |
. . . 4
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯π΅π¦ββ©) |
44 | 43, 22, 31 | 3jca 1129 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯π΅π¦ββ© β§ π₯(πΎβπ΅)πΆ β§ π¦(πΎβπ΅)π΄)) |
45 | 38 | necomd 3000 |
. . . . 5
β’ (π β πΆ β π΅) |
46 | | cgraid.1 |
. . . . . 6
β’ (π β π΄ β π΅) |
47 | 46 | necomd 3000 |
. . . . 5
β’ (π β π΅ β π΄) |
48 | 1, 14, 21, 8, 8, 6,
4, 10, 2, 45, 47 | hlcgrex 27600 |
. . . 4
β’ (π β βπ₯ β π (π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄))) |
49 | 1, 14, 21, 8, 8, 10, 4, 6, 2,
46, 38 | hlcgrex 27600 |
. . . 4
β’ (π β βπ¦ β π (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ))) |
50 | | reeanv 3220 |
. . . 4
β’
(βπ₯ β
π βπ¦ β π ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ))) β (βπ₯ β π (π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ βπ¦ β π (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) |
51 | 48, 49, 50 | sylanbrc 584 |
. . 3
β’ (π β βπ₯ β π βπ¦ β π ((π₯(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) |
52 | 44, 51 | reximddv2 3207 |
. 2
β’ (π β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯π΅π¦ββ© β§ π₯(πΎβπ΅)πΆ β§ π¦(πΎβπ΅)π΄)) |
53 | 1, 14, 21, 4, 6, 8,
10, 10, 8, 6 | iscgra 27793 |
. 2
β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπΆπ΅π΄ββ© β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯π΅π¦ββ© β§ π₯(πΎβπ΅)πΆ β§ π¦(πΎβπ΅)π΄))) |
54 | 52, 53 | mpbird 257 |
1
β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπΆπ΅π΄ββ©) |