Step | Hyp | Ref
| Expression |
1 | | simprl 768 |
. . 3
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β πΆ β (π΄πΌπ₯)) |
2 | | tkgeom.p |
. . . . 5
β’ π = (BaseβπΊ) |
3 | | tkgeom.d |
. . . . 5
β’ β =
(distβπΊ) |
4 | | tkgeom.i |
. . . . 5
β’ πΌ = (ItvβπΊ) |
5 | | tkgeom.g |
. . . . . 6
β’ (π β πΊ β TarskiG) |
6 | 5 | ad2antrr 723 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β πΊ β TarskiG) |
7 | | tgbtwnintr.3 |
. . . . . 6
β’ (π β πΆ β π) |
8 | 7 | ad2antrr 723 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β πΆ β π) |
9 | | tgbtwnintr.4 |
. . . . . 6
β’ (π β π· β π) |
10 | 9 | ad2antrr 723 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β π· β π) |
11 | | tgbtwnintr.2 |
. . . . . 6
β’ (π β π΅ β π) |
12 | 11 | ad2antrr 723 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β π΅ β π) |
13 | | simplr 766 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β π₯ β π) |
14 | | tgbtwnouttr2.1 |
. . . . . 6
β’ (π β π΅ β πΆ) |
15 | 14 | ad2antrr 723 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β π΅ β πΆ) |
16 | | tgbtwnintr.1 |
. . . . . . 7
β’ (π β π΄ β π) |
17 | 16 | ad2antrr 723 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β π΄ β π) |
18 | | tgbtwnouttr2.2 |
. . . . . . 7
β’ (π β π΅ β (π΄πΌπΆ)) |
19 | 18 | ad2antrr 723 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β π΅ β (π΄πΌπΆ)) |
20 | 2, 3, 4, 6, 17, 12, 8, 13, 19, 1 | tgbtwnexch3 28013 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β πΆ β (π΅πΌπ₯)) |
21 | | tgbtwnouttr2.3 |
. . . . . 6
β’ (π β πΆ β (π΅πΌπ·)) |
22 | 21 | ad2antrr 723 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β πΆ β (π΅πΌπ·)) |
23 | | simprr 770 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β (πΆ β π₯) = (πΆ β π·)) |
24 | | eqidd 2732 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β (πΆ β π·) = (πΆ β π·)) |
25 | 2, 3, 4, 6, 8, 8, 10, 12, 13, 10, 15, 20, 22, 23, 24 | tgsegconeq 28005 |
. . . 4
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β π₯ = π·) |
26 | 25 | oveq2d 7428 |
. . 3
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β (π΄πΌπ₯) = (π΄πΌπ·)) |
27 | 1, 26 | eleqtrd 2834 |
. 2
β’ (((π β§ π₯ β π) β§ (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) β πΆ β (π΄πΌπ·)) |
28 | 2, 3, 4, 5, 16, 7,
7, 9 | axtgsegcon 27983 |
. 2
β’ (π β βπ₯ β π (πΆ β (π΄πΌπ₯) β§ (πΆ β π₯) = (πΆ β π·))) |
29 | 27, 28 | r19.29a 3161 |
1
β’ (π β πΆ β (π΄πΌπ·)) |