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 | | cgracom.d |
. . . . . 6
β’ (π β π· β π) |
7 | 6 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β π· β π) |
8 | | cgracom.e |
. . . . . 6
β’ (π β πΈ β π) |
9 | 8 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β πΈ β π) |
10 | | cgracom.f |
. . . . . 6
β’ (π β πΉ β π) |
11 | 10 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β πΉ β π) |
12 | | simpllr 775 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β π₯ β π) |
13 | | cgraid.b |
. . . . . 6
β’ (π β π΅ β π) |
14 | 13 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β π΅ β π) |
15 | | simplr 768 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β π¦ β π) |
16 | | cgraid.i |
. . . . . 6
β’ πΌ = (ItvβπΊ) |
17 | | simprlr 779 |
. . . . . . 7
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) |
18 | 17 | eqcomd 2743 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β (πΈ(distβπΊ)π·) = (π΅(distβπΊ)π₯)) |
19 | 1, 2, 16, 5, 9, 7,
14, 12, 18 | tgcgrcomlr 27464 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β (π·(distβπΊ)πΈ) = (π₯(distβπΊ)π΅)) |
20 | | simprrr 781 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)) |
21 | 20 | eqcomd 2743 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β (πΈ(distβπΊ)πΉ) = (π΅(distβπΊ)π¦)) |
22 | | cgraid.k |
. . . . . . . 8
β’ πΎ = (hlGβπΊ) |
23 | | cgraid.a |
. . . . . . . . 9
β’ (π β π΄ β π) |
24 | 23 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β π΄ β π) |
25 | | cgraid.c |
. . . . . . . . 9
β’ (π β πΆ β π) |
26 | 25 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β πΆ β π) |
27 | | cgracom.1 |
. . . . . . . . 9
β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) |
28 | 27 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) |
29 | | simprll 778 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β π₯(πΎβπ΅)π΄) |
30 | | simprrl 780 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β π¦(πΎβπ΅)πΆ) |
31 | 1, 16, 22, 5, 24, 14, 26, 7, 9, 11, 28, 12, 2, 15, 29, 30, 17, 20 | cgracgr 27802 |
. . . . . . 7
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β (π₯(distβπΊ)π¦) = (π·(distβπΊ)πΉ)) |
32 | 31 | eqcomd 2743 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β (π·(distβπΊ)πΉ) = (π₯(distβπΊ)π¦)) |
33 | 1, 2, 16, 5, 7, 11, 12, 15, 32 | tgcgrcomlr 27464 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β (πΉ(distβπΊ)π·) = (π¦(distβπΊ)π₯)) |
34 | 1, 2, 3, 5, 7, 9, 11, 12, 14, 15, 19, 21, 33 | trgcgr 27500 |
. . . 4
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β β¨βπ·πΈπΉββ©(cgrGβπΊ)β¨βπ₯π΅π¦ββ©) |
35 | 34, 29, 30 | 3jca 1129 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) β (β¨βπ·πΈπΉββ©(cgrGβπΊ)β¨βπ₯π΅π¦ββ© β§ π₯(πΎβπ΅)π΄ β§ π¦(πΎβπ΅)πΆ)) |
36 | 1, 16, 22, 4, 23, 13, 25, 6, 8, 10, 27 | cgrane1 27796 |
. . . . 5
β’ (π β π΄ β π΅) |
37 | 1, 16, 22, 4, 23, 13, 25, 6, 8, 10, 27 | cgrane3 27798 |
. . . . 5
β’ (π β πΈ β π·) |
38 | 1, 16, 22, 13, 8, 6, 4, 23, 2,
36, 37 | hlcgrex 27600 |
. . . 4
β’ (π β βπ₯ β π (π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·))) |
39 | 1, 16, 22, 4, 23, 13, 25, 6, 8, 10, 27 | cgrane2 27797 |
. . . . . 6
β’ (π β π΅ β πΆ) |
40 | 39 | necomd 3000 |
. . . . 5
β’ (π β πΆ β π΅) |
41 | 1, 16, 22, 4, 23, 13, 25, 6, 8, 10, 27 | cgrane4 27799 |
. . . . 5
β’ (π β πΈ β πΉ) |
42 | 1, 16, 22, 13, 8, 10, 4, 25, 2, 40, 41 | hlcgrex 27600 |
. . . 4
β’ (π β βπ¦ β π (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ))) |
43 | | reeanv 3220 |
. . . 4
β’
(βπ₯ β
π βπ¦ β π ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ))) β (βπ₯ β π (π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ βπ¦ β π (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) |
44 | 38, 42, 43 | sylanbrc 584 |
. . 3
β’ (π β βπ₯ β π βπ¦ β π ((π₯(πΎβπ΅)π΄ β§ (π΅(distβπΊ)π₯) = (πΈ(distβπΊ)π·)) β§ (π¦(πΎβπ΅)πΆ β§ (π΅(distβπΊ)π¦) = (πΈ(distβπΊ)πΉ)))) |
45 | 35, 44 | reximddv2 3207 |
. 2
β’ (π β βπ₯ β π βπ¦ β π (β¨βπ·πΈπΉββ©(cgrGβπΊ)β¨βπ₯π΅π¦ββ© β§ π₯(πΎβπ΅)π΄ β§ π¦(πΎβπ΅)πΆ)) |
46 | 1, 16, 22, 4, 6, 8,
10, 23, 13, 25 | iscgra 27793 |
. 2
β’ (π β (β¨βπ·πΈπΉββ©(cgrAβπΊ)β¨βπ΄π΅πΆββ© β βπ₯ β π βπ¦ β π (β¨βπ·πΈπΉββ©(cgrGβπΊ)β¨βπ₯π΅π¦ββ© β§ π₯(πΎβπ΅)π΄ β§ π¦(πΎβπ΅)πΆ))) |
47 | 45, 46 | mpbird 257 |
1
β’ (π β β¨βπ·πΈπΉββ©(cgrAβπΊ)β¨βπ΄π΅πΆββ©) |