Step | Hyp | Ref
| Expression |
1 | | tglnpt2.p |
. . . . . 6
β’ π = (BaseβπΊ) |
2 | | tglnpt2.i |
. . . . . 6
β’ πΌ = (ItvβπΊ) |
3 | | tglnpt2.l |
. . . . . 6
β’ πΏ = (LineGβπΊ) |
4 | | tglnpt2.g |
. . . . . . 7
β’ (π β πΊ β TarskiG) |
5 | 4 | ad4antr 731 |
. . . . . 6
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π = π₯) β πΊ β TarskiG) |
6 | | simp-4r 783 |
. . . . . 6
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π = π₯) β π₯ β π) |
7 | | simpllr 775 |
. . . . . 6
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π = π₯) β π§ β π) |
8 | | simplrr 777 |
. . . . . 6
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π = π₯) β π₯ β π§) |
9 | 1, 2, 3, 5, 6, 7, 8 | tglinerflx2 27885 |
. . . . 5
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π = π₯) β π§ β (π₯πΏπ§)) |
10 | | simplrl 776 |
. . . . 5
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π = π₯) β π΄ = (π₯πΏπ§)) |
11 | 9, 10 | eleqtrrd 2837 |
. . . 4
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π = π₯) β π§ β π΄) |
12 | | simpr 486 |
. . . . 5
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π = π₯) β π = π₯) |
13 | 12, 8 | eqnetrd 3009 |
. . . 4
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π = π₯) β π β π§) |
14 | | neeq2 3005 |
. . . . 5
β’ (π¦ = π§ β (π β π¦ β π β π§)) |
15 | 14 | rspcev 3613 |
. . . 4
β’ ((π§ β π΄ β§ π β π§) β βπ¦ β π΄ π β π¦) |
16 | 11, 13, 15 | syl2anc 585 |
. . 3
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π = π₯) β βπ¦ β π΄ π β π¦) |
17 | 4 | ad4antr 731 |
. . . . . 6
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π β π₯) β πΊ β TarskiG) |
18 | | simp-4r 783 |
. . . . . 6
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π β π₯) β π₯ β π) |
19 | | simpllr 775 |
. . . . . 6
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π β π₯) β π§ β π) |
20 | | simplrr 777 |
. . . . . 6
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π β π₯) β π₯ β π§) |
21 | 1, 2, 3, 17, 18, 19, 20 | tglinerflx1 27884 |
. . . . 5
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π β π₯) β π₯ β (π₯πΏπ§)) |
22 | | simplrl 776 |
. . . . 5
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π β π₯) β π΄ = (π₯πΏπ§)) |
23 | 21, 22 | eleqtrrd 2837 |
. . . 4
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π β π₯) β π₯ β π΄) |
24 | | simpr 486 |
. . . 4
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π β π₯) β π β π₯) |
25 | | neeq2 3005 |
. . . . 5
β’ (π¦ = π₯ β (π β π¦ β π β π₯)) |
26 | 25 | rspcev 3613 |
. . . 4
β’ ((π₯ β π΄ β§ π β π₯) β βπ¦ β π΄ π β π¦) |
27 | 23, 24, 26 | syl2anc 585 |
. . 3
β’
(((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β§ π β π₯) β βπ¦ β π΄ π β π¦) |
28 | 16, 27 | pm2.61dane 3030 |
. 2
β’ ((((π β§ π₯ β π) β§ π§ β π) β§ (π΄ = (π₯πΏπ§) β§ π₯ β π§)) β βπ¦ β π΄ π β π¦) |
29 | | tglnpt2.a |
. . 3
β’ (π β π΄ β ran πΏ) |
30 | 1, 2, 3, 4, 29 | tgisline 27878 |
. 2
β’ (π β βπ₯ β π βπ§ β π (π΄ = (π₯πΏπ§) β§ π₯ β π§)) |
31 | 28, 30 | r19.29vva 3214 |
1
β’ (π β βπ¦ β π΄ π β π¦) |