Step | Hyp | Ref
| Expression |
1 | | tkgeom.p |
. . . . 5
β’ π = (BaseβπΊ) |
2 | | tkgeom.d |
. . . . 5
β’ β =
(distβπΊ) |
3 | | tkgeom.i |
. . . . 5
β’ πΌ = (ItvβπΊ) |
4 | | tkgeom.g |
. . . . . 6
β’ (π β πΊ β TarskiG) |
5 | 4 | ad2antrr 723 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (π΄ β (π΅πΌπ₯) β§ (π΄ β π₯) = (π΅ β π΅))) β πΊ β TarskiG) |
6 | | tgcgrtriv.1 |
. . . . . 6
β’ (π β π΄ β π) |
7 | 6 | ad2antrr 723 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (π΄ β (π΅πΌπ₯) β§ (π΄ β π₯) = (π΅ β π΅))) β π΄ β π) |
8 | | simplr 766 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (π΄ β (π΅πΌπ₯) β§ (π΄ β π₯) = (π΅ β π΅))) β π₯ β π) |
9 | | tgcgrtriv.2 |
. . . . . 6
β’ (π β π΅ β π) |
10 | 9 | ad2antrr 723 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (π΄ β (π΅πΌπ₯) β§ (π΄ β π₯) = (π΅ β π΅))) β π΅ β π) |
11 | | simprr 770 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (π΄ β (π΅πΌπ₯) β§ (π΄ β π₯) = (π΅ β π΅))) β (π΄ β π₯) = (π΅ β π΅)) |
12 | 1, 2, 3, 5, 7, 8, 10, 11 | axtgcgrid 27978 |
. . . 4
β’ (((π β§ π₯ β π) β§ (π΄ β (π΅πΌπ₯) β§ (π΄ β π₯) = (π΅ β π΅))) β π΄ = π₯) |
13 | 12 | oveq2d 7428 |
. . 3
β’ (((π β§ π₯ β π) β§ (π΄ β (π΅πΌπ₯) β§ (π΄ β π₯) = (π΅ β π΅))) β (π΄ β π΄) = (π΄ β π₯)) |
14 | 13, 11 | eqtrd 2771 |
. 2
β’ (((π β§ π₯ β π) β§ (π΄ β (π΅πΌπ₯) β§ (π΄ β π₯) = (π΅ β π΅))) β (π΄ β π΄) = (π΅ β π΅)) |
15 | 1, 2, 3, 4, 9, 6, 9, 9 | axtgsegcon 27979 |
. 2
β’ (π β βπ₯ β π (π΄ β (π΅πΌπ₯) β§ (π΄ β π₯) = (π΅ β π΅))) |
16 | 14, 15 | r19.29a 3161 |
1
β’ (π β (π΄ β π΄) = (π΅ β π΅)) |