Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . 3
β’ (((π β§ π₯ β π) β§ (π΅ β (π΄πΌπ₯) β§ (π΅ β π₯) = (π΅ β π΅))) β π΅ β (π΄πΌπ₯)) |
2 | | tkgeom.p |
. . . . . 6
β’ π = (BaseβπΊ) |
3 | | tkgeom.d |
. . . . . 6
β’ β =
(distβπΊ) |
4 | | tkgeom.i |
. . . . . 6
β’ πΌ = (ItvβπΊ) |
5 | | tkgeom.g |
. . . . . . 7
β’ (π β πΊ β TarskiG) |
6 | 5 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ (π΅ β π₯) = (π΅ β π΅)) β πΊ β TarskiG) |
7 | | tgbtwntriv2.2 |
. . . . . . 7
β’ (π β π΅ β π) |
8 | 7 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ (π΅ β π₯) = (π΅ β π΅)) β π΅ β π) |
9 | | simplr 768 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ (π΅ β π₯) = (π΅ β π΅)) β π₯ β π) |
10 | | simpr 486 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ (π΅ β π₯) = (π΅ β π΅)) β (π΅ β π₯) = (π΅ β π΅)) |
11 | 2, 3, 4, 6, 8, 9, 8, 10 | axtgcgrid 27714 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (π΅ β π₯) = (π΅ β π΅)) β π΅ = π₯) |
12 | 11 | adantrl 715 |
. . . 4
β’ (((π β§ π₯ β π) β§ (π΅ β (π΄πΌπ₯) β§ (π΅ β π₯) = (π΅ β π΅))) β π΅ = π₯) |
13 | 12 | oveq2d 7425 |
. . 3
β’ (((π β§ π₯ β π) β§ (π΅ β (π΄πΌπ₯) β§ (π΅ β π₯) = (π΅ β π΅))) β (π΄πΌπ΅) = (π΄πΌπ₯)) |
14 | 1, 13 | eleqtrrd 2837 |
. 2
β’ (((π β§ π₯ β π) β§ (π΅ β (π΄πΌπ₯) β§ (π΅ β π₯) = (π΅ β π΅))) β π΅ β (π΄πΌπ΅)) |
15 | | tgbtwntriv2.1 |
. . 3
β’ (π β π΄ β π) |
16 | 2, 3, 4, 5, 15, 7,
7, 7 | axtgsegcon 27715 |
. 2
β’ (π β βπ₯ β π (π΅ β (π΄πΌπ₯) β§ (π΅ β π₯) = (π΅ β π΅))) |
17 | 14, 16 | r19.29a 3163 |
1
β’ (π β π΅ β (π΄πΌπ΅)) |