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 | | cgratr.i |
. . . . . 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 | 5 | ad3antrrr 729 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β πΊ β TarskiG) |
23 | 7 | ad3antrrr 729 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π΄ β π) |
24 | 9 | ad3antrrr 729 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π΅ β π) |
25 | 11 | ad3antrrr 729 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β πΆ β π) |
26 | | simpllr 775 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π’ β π) |
27 | | cgracom.e |
. . . . . . . . 9
β’ (π β πΈ β π) |
28 | 27 | ad6antr 735 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β πΈ β π) |
29 | | simplr 768 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π£ β π) |
30 | | simpr1 1195 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ©) |
31 | 1, 2, 16, 3, 22, 23, 24, 25, 26, 28, 29, 30 | cgr3simp3 27506 |
. . . . . . 7
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (πΆ(distβπΊ)π΄) = (π£(distβπΊ)π’)) |
32 | 12 | ad3antrrr 729 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π₯ β π) |
33 | 15 | ad3antrrr 729 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π¦ β π) |
34 | | cgraid.k |
. . . . . . . . 9
β’ πΎ = (hlGβπΊ) |
35 | | cgracom.d |
. . . . . . . . . 10
β’ (π β π· β π) |
36 | 35 | ad6antr 735 |
. . . . . . . . 9
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π· β π) |
37 | | cgracom.f |
. . . . . . . . . 10
β’ (π β πΉ β π) |
38 | 37 | ad6antr 735 |
. . . . . . . . 9
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β πΉ β π) |
39 | 14 | ad3antrrr 729 |
. . . . . . . . 9
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π β π) |
40 | | cgratr.j |
. . . . . . . . . . 11
β’ (π β π½ β π) |
41 | 40 | ad6antr 735 |
. . . . . . . . . 10
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π½ β π) |
42 | | cgratr.h |
. . . . . . . . . . . 12
β’ (π β π» β π) |
43 | 42 | ad6antr 735 |
. . . . . . . . . . 11
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π» β π) |
44 | | cgratr.1 |
. . . . . . . . . . . 12
β’ (π β β¨βπ·πΈπΉββ©(cgrAβπΊ)β¨βπ»ππ½ββ©) |
45 | 44 | ad6antr 735 |
. . . . . . . . . . 11
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β β¨βπ·πΈπΉββ©(cgrAβπΊ)β¨βπ»ππ½ββ©) |
46 | | simprll 778 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β π₯(πΎβπ)π») |
47 | 46 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π₯(πΎβπ)π») |
48 | 1, 16, 34, 22, 36, 28, 38, 43, 39, 41, 45, 32, 47 | cgrahl1 27800 |
. . . . . . . . . 10
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β β¨βπ·πΈπΉββ©(cgrAβπΊ)β¨βπ₯ππ½ββ©) |
49 | | simprrl 780 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β π¦(πΎβπ)π½) |
50 | 49 | ad3antrrr 729 |
. . . . . . . . . 10
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π¦(πΎβπ)π½) |
51 | 1, 16, 34, 22, 36, 28, 38, 32, 39, 41, 48, 33, 50 | cgrahl2 27801 |
. . . . . . . . 9
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β β¨βπ·πΈπΉββ©(cgrAβπΊ)β¨βπ₯ππ¦ββ©) |
52 | | simpr2 1196 |
. . . . . . . . 9
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π’(πΎβπΈ)π·) |
53 | | simpr3 1197 |
. . . . . . . . 9
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β π£(πΎβπΈ)πΉ) |
54 | 1, 2, 16, 3, 22, 23, 24, 25, 26, 28, 29, 30 | cgr3simp1 27504 |
. . . . . . . . . . . 12
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (π΄(distβπΊ)π΅) = (π’(distβπΊ)πΈ)) |
55 | 54 | eqcomd 2743 |
. . . . . . . . . . 11
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (π’(distβπΊ)πΈ) = (π΄(distβπΊ)π΅)) |
56 | 1, 2, 16, 22, 26, 28, 23, 24, 55 | tgcgrcomlr 27464 |
. . . . . . . . . 10
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (πΈ(distβπΊ)π’) = (π΅(distβπΊ)π΄)) |
57 | 18 | ad3antrrr 729 |
. . . . . . . . . 10
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (π΅(distβπΊ)π΄) = (π(distβπΊ)π₯)) |
58 | 56, 57 | eqtrd 2777 |
. . . . . . . . 9
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (πΈ(distβπΊ)π’) = (π(distβπΊ)π₯)) |
59 | 1, 2, 16, 3, 22, 23, 24, 25, 26, 28, 29, 30 | cgr3simp2 27505 |
. . . . . . . . . 10
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (π΅(distβπΊ)πΆ) = (πΈ(distβπΊ)π£)) |
60 | 21 | ad3antrrr 729 |
. . . . . . . . . 10
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (π΅(distβπΊ)πΆ) = (π(distβπΊ)π¦)) |
61 | 59, 60 | eqtr3d 2779 |
. . . . . . . . 9
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (πΈ(distβπΊ)π£) = (π(distβπΊ)π¦)) |
62 | 1, 16, 34, 22, 36, 28, 38, 32, 39, 33, 51, 26, 2, 29, 52, 53, 58, 61 | cgracgr 27802 |
. . . . . . . 8
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (π’(distβπΊ)π£) = (π₯(distβπΊ)π¦)) |
63 | 1, 2, 16, 22, 26, 29, 32, 33, 62 | tgcgrcomlr 27464 |
. . . . . . 7
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (π£(distβπΊ)π’) = (π¦(distβπΊ)π₯)) |
64 | 31, 63 | eqtrd 2777 |
. . . . . 6
β’
(((((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β§ π’ β π) β§ π£ β π) β§ (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) β (πΆ(distβπΊ)π΄) = (π¦(distβπΊ)π₯)) |
65 | | cgracom.1 |
. . . . . . . 8
β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) |
66 | 1, 16, 34, 4, 6, 8,
10, 35, 27, 37 | iscgra 27793 |
. . . . . . . 8
β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β βπ’ β π βπ£ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ))) |
67 | 65, 66 | mpbid 231 |
. . . . . . 7
β’ (π β βπ’ β π βπ£ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) |
68 | 67 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β βπ’ β π βπ£ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ’πΈπ£ββ© β§ π’(πΎβπΈ)π· β§ π£(πΎβπΈ)πΉ)) |
69 | 64, 68 | r19.29vva 3208 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (πΆ(distβπΊ)π΄) = (π¦(distβπΊ)π₯)) |
70 | 1, 2, 3, 5, 7, 9, 11, 12, 14, 15, 19, 21, 69 | trgcgr 27500 |
. . . 4
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯ππ¦ββ©) |
71 | 70, 46, 49 | 3jca 1129 |
. . 3
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯ππ¦ββ© β§ π₯(πΎβπ)π» β§ π¦(πΎβπ)π½)) |
72 | 1, 16, 34, 4, 35, 27, 37, 42, 13, 40, 44 | cgrane3 27798 |
. . . . . 6
β’ (π β π β π») |
73 | 72 | necomd 3000 |
. . . . 5
β’ (π β π» β π) |
74 | 1, 16, 34, 4, 6, 8,
10, 35, 27, 37, 65 | cgrane1 27796 |
. . . . . 6
β’ (π β π΄ β π΅) |
75 | 74 | necomd 3000 |
. . . . 5
β’ (π β π΅ β π΄) |
76 | 1, 16, 34, 13, 8, 6, 4, 42, 2,
73, 75 | hlcgrex 27600 |
. . . 4
β’ (π β βπ₯ β π (π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄))) |
77 | 1, 16, 34, 4, 35, 27, 37, 42, 13, 40, 44 | cgrane4 27799 |
. . . . . 6
β’ (π β π β π½) |
78 | 77 | necomd 3000 |
. . . . 5
β’ (π β π½ β π) |
79 | 1, 16, 34, 4, 6, 8,
10, 35, 27, 37, 65 | cgrane2 27797 |
. . . . 5
β’ (π β π΅ β πΆ) |
80 | 1, 16, 34, 13, 8, 10, 4, 40, 2, 78, 79 | hlcgrex 27600 |
. . . 4
β’ (π β βπ¦ β π (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ))) |
81 | | reeanv 3220 |
. . . 4
β’
(βπ₯ β
π βπ¦ β π ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ))) β (βπ₯ β π (π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ βπ¦ β π (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) |
82 | 76, 80, 81 | sylanbrc 584 |
. . 3
β’ (π β βπ₯ β π βπ¦ β π ((π₯(πΎβπ)π» β§ (π(distβπΊ)π₯) = (π΅(distβπΊ)π΄)) β§ (π¦(πΎβπ)π½ β§ (π(distβπΊ)π¦) = (π΅(distβπΊ)πΆ)))) |
83 | 71, 82 | reximddv2 3207 |
. 2
β’ (π β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯ππ¦ββ© β§ π₯(πΎβπ)π» β§ π¦(πΎβπ)π½)) |
84 | 1, 16, 34, 4, 6, 8,
10, 42, 13, 40 | iscgra 27793 |
. 2
β’ (π β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ»ππ½ββ© β βπ₯ β π βπ¦ β π (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ₯ππ¦ββ© β§ π₯(πΎβπ)π» β§ π¦(πΎβπ)π½))) |
85 | 83, 84 | mpbird 257 |
1
β’ (π β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ»ππ½ββ©) |