Step | Hyp | Ref
| Expression |
1 | | dfcgrg2.p |
. . . . . 6
β’ π = (BaseβπΊ) |
2 | | dfcgrg2.m |
. . . . . 6
β’ β =
(distβπΊ) |
3 | | eqid 2737 |
. . . . . 6
β’
(ItvβπΊ) =
(ItvβπΊ) |
4 | | dfcgrg2.g |
. . . . . . 7
β’ (π β πΊ β TarskiG) |
5 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β πΊ β TarskiG) |
6 | | dfcgrg2.a |
. . . . . . 7
β’ (π β π΄ β π) |
7 | 6 | adantr 482 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β π΄ β π) |
8 | | dfcgrg2.b |
. . . . . . 7
β’ (π β π΅ β π) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β π΅ β π) |
10 | | dfcgrg2.c |
. . . . . . 7
β’ (π β πΆ β π) |
11 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β πΆ β π) |
12 | | dfcgrg2.d |
. . . . . . 7
β’ (π β π· β π) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β π· β π) |
14 | | dfcgrg2.e |
. . . . . . 7
β’ (π β πΈ β π) |
15 | 14 | adantr 482 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β πΈ β π) |
16 | | dfcgrg2.f |
. . . . . . 7
β’ (π β πΉ β π) |
17 | 16 | adantr 482 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β πΉ β π) |
18 | | eqid 2737 |
. . . . . . . . 9
β’
(cgrGβπΊ) =
(cgrGβπΊ) |
19 | 1, 2, 18, 4, 6, 8,
10, 12, 14, 16 | trgcgrg 27499 |
. . . . . . . 8
β’ (π β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ© β ((π΄ β π΅) = (π· β πΈ) β§ (π΅ β πΆ) = (πΈ β πΉ) β§ (πΆ β π΄) = (πΉ β π·)))) |
20 | 19 | biimpa 478 |
. . . . . . 7
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β ((π΄ β π΅) = (π· β πΈ) β§ (π΅ β πΆ) = (πΈ β πΉ) β§ (πΆ β π΄) = (πΉ β π·))) |
21 | 20 | simp1d 1143 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β (π΄ β π΅) = (π· β πΈ)) |
22 | 20 | simp2d 1144 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β (π΅ β πΆ) = (πΈ β πΉ)) |
23 | 20 | simp3d 1145 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β (πΆ β π΄) = (πΉ β π·)) |
24 | | dfcgrg2.1 |
. . . . . . 7
β’ (π β π΄ β π΅) |
25 | 24 | adantr 482 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β π΄ β π΅) |
26 | | dfcgrg2.2 |
. . . . . . 7
β’ (π β π΅ β πΆ) |
27 | 26 | adantr 482 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β π΅ β πΆ) |
28 | | dfcgrg2.3 |
. . . . . . 7
β’ (π β πΆ β π΄) |
29 | 28 | adantr 482 |
. . . . . 6
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β πΆ β π΄) |
30 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 21, 22, 23, 25, 27, 29 | tgsss1 27844 |
. . . . 5
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ©) |
31 | 1, 2, 3, 5, 11, 7,
9, 17, 13, 15, 23, 21, 22, 29, 25, 27 | tgsss1 27844 |
. . . . 5
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ©) |
32 | 1, 2, 3, 5, 9, 11,
7, 15, 17, 13, 22, 23, 21, 27, 29, 25 | tgsss1 27844 |
. . . . 5
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©) |
33 | 30, 31, 32 | 3jca 1129 |
. . . 4
β’ ((π β§ β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ©) β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ© β§ β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©)) |
34 | 33 | ex 414 |
. . 3
β’ (π β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ© β (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ© β§ β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©))) |
35 | 34 | pm4.71d 563 |
. 2
β’ (π β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ© β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ© β§ (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ© β§ β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©)))) |
36 | 19 | anbi1d 631 |
. 2
β’ (π β ((β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ© β§ (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ© β§ β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©)) β (((π΄ β π΅) = (π· β πΈ) β§ (π΅ β πΆ) = (πΈ β πΉ) β§ (πΆ β π΄) = (πΉ β π·)) β§ (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ© β§ β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©)))) |
37 | 35, 36 | bitrd 279 |
1
β’ (π β (β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπΉββ© β (((π΄ β π΅) = (π· β πΈ) β§ (π΅ β πΆ) = (πΈ β πΉ) β§ (πΆ β π΄) = (πΉ β π·)) β§ (β¨βπ΄π΅πΆββ©(cgrAβπΊ)β¨βπ·πΈπΉββ© β§ β¨βπΆπ΄π΅ββ©(cgrAβπΊ)β¨βπΉπ·πΈββ© β§ β¨βπ΅πΆπ΄ββ©(cgrAβπΊ)β¨βπΈπΉπ·ββ©)))) |