Step | Hyp | Ref
| Expression |
1 | | simprrl 780 |
. . . . 5
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) |
2 | | hpg.p |
. . . . . . 7
β’ π = (BaseβπΊ) |
3 | | hpg.i |
. . . . . . 7
β’ πΌ = (ItvβπΊ) |
4 | | opphl.l |
. . . . . . 7
β’ πΏ = (LineGβπΊ) |
5 | | opphl.g |
. . . . . . . 8
β’ (π β πΊ β TarskiG) |
6 | 5 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β πΊ β TarskiG) |
7 | | opphl.d |
. . . . . . . . 9
β’ (π β π· β ran πΏ) |
8 | 7 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β π· β ran πΏ) |
9 | | oppperpex.1 |
. . . . . . . . 9
β’ (π β π΄ β π·) |
10 | 9 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β π΄ β π·) |
11 | 2, 4, 3, 6, 8, 10 | tglnpt 27800 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β π΄ β π) |
12 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β π₯ β π·) |
13 | 2, 4, 3, 6, 8, 12 | tglnpt 27800 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β π₯ β π) |
14 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β π΄ β π₯) |
15 | 2, 3, 4, 6, 11, 13, 14, 14, 8, 10, 12 | tglinethru 27887 |
. . . . . 6
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β π· = (π΄πΏπ₯)) |
16 | 15 | adantr 482 |
. . . . 5
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β π· = (π΄πΏπ₯)) |
17 | 1, 16 | breqtrrd 5177 |
. . . 4
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β (π΄πΏπ)(βGβπΊ)π·) |
18 | | oppperpex.3 |
. . . . . . 7
β’ (π β Β¬ πΆ β π·) |
19 | 18 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β Β¬ πΆ β π·) |
20 | | hpg.d |
. . . . . . 7
β’ β =
(distβπΊ) |
21 | 6 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β πΊ β TarskiG) |
22 | 8 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β π· β ran πΏ) |
23 | 10 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β π΄ β π·) |
24 | | simprl 770 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β π β π) |
25 | 2, 20, 3, 4, 21, 22, 23, 24, 17 | footne 27974 |
. . . . . 6
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β Β¬ π β π·) |
26 | 14 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β§ (π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β π΄ β π₯) |
27 | 26 | neneqd 2946 |
. . . . . . . . . . . . 13
β’
((((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β§ (π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β Β¬ π΄ = π₯) |
28 | | simprrl 780 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β§ (π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β (π‘ β (π΄πΏπ₯) β¨ π΄ = π₯)) |
29 | 28 | orcomd 870 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β§ (π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β (π΄ = π₯ β¨ π‘ β (π΄πΏπ₯))) |
30 | 29 | ord 863 |
. . . . . . . . . . . . 13
β’
((((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β§ (π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β (Β¬ π΄ = π₯ β π‘ β (π΄πΏπ₯))) |
31 | 27, 30 | mpd 15 |
. . . . . . . . . . . 12
β’
((((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β§ (π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β π‘ β (π΄πΏπ₯)) |
32 | 15 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’
((((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β§ (π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β π· = (π΄πΏπ₯)) |
33 | 31, 32 | eleqtrrd 2837 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β§ (π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β π‘ β π·) |
34 | | simprrr 781 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β§ (π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β π‘ β (πΆπΌπ)) |
35 | 33, 34 | jca 513 |
. . . . . . . . . 10
β’
((((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β§ (π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β (π‘ β π· β§ π‘ β (πΆπΌπ))) |
36 | 35 | ex 414 |
. . . . . . . . 9
β’
(((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β ((π‘ β π β§ ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))) β (π‘ β π· β§ π‘ β (πΆπΌπ)))) |
37 | 36 | reximdv2 3165 |
. . . . . . . 8
β’
(((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β (βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)) β βπ‘ β π· π‘ β (πΆπΌπ))) |
38 | 37 | impr 456 |
. . . . . . 7
β’
(((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β βπ‘ β π· π‘ β (πΆπΌπ)) |
39 | 38 | anasss 468 |
. . . . . 6
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β βπ‘ β π· π‘ β (πΆπΌπ)) |
40 | 19, 25, 39 | jca31 516 |
. . . . 5
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β ((Β¬ πΆ β π· β§ Β¬ π β π·) β§ βπ‘ β π· π‘ β (πΆπΌπ))) |
41 | | hpg.o |
. . . . . . . 8
β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} |
42 | | oppperpex.2 |
. . . . . . . . . 10
β’ (π β πΆ β π) |
43 | 42 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β πΆ β π) |
44 | 43 | ad2antrr 725 |
. . . . . . . 8
β’
(((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β πΆ β π) |
45 | | simplr 768 |
. . . . . . . 8
β’
(((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β π β π) |
46 | 2, 20, 3, 41, 44, 45 | islnopp 27990 |
. . . . . . 7
β’
(((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ (π΄πΏπ)(βGβπΊ)(π΄πΏπ₯)) β (πΆππ β ((Β¬ πΆ β π· β§ Β¬ π β π·) β§ βπ‘ β π· π‘ β (πΆπΌπ)))) |
47 | 46 | adantrr 716 |
. . . . . 6
β’
(((((π β§ π₯ β π·) β§ π΄ β π₯) β§ π β π) β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) β (πΆππ β ((Β¬ πΆ β π· β§ Β¬ π β π·) β§ βπ‘ β π· π‘ β (πΆπΌπ)))) |
48 | 47 | anasss 468 |
. . . . 5
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β (πΆππ β ((Β¬ πΆ β π· β§ Β¬ π β π·) β§ βπ‘ β π· π‘ β (πΆπΌπ)))) |
49 | 40, 48 | mpbird 257 |
. . . 4
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β πΆππ) |
50 | 17, 49 | jca 513 |
. . 3
β’ ((((π β§ π₯ β π·) β§ π΄ β π₯) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ))))) β ((π΄πΏπ)(βGβπΊ)π· β§ πΆππ)) |
51 | | oppperpex.4 |
. . . . 5
β’ (π β πΊDimTarskiGβ₯2) |
52 | 51 | ad2antrr 725 |
. . . 4
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β πΊDimTarskiGβ₯2) |
53 | 2, 20, 3, 4, 6, 11,
13, 43, 14, 52 | colperpex 27984 |
. . 3
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β βπ β π ((π΄πΏπ)(βGβπΊ)(π΄πΏπ₯) β§ βπ‘ β π ((π‘ β (π΄πΏπ₯) β¨ π΄ = π₯) β§ π‘ β (πΆπΌπ)))) |
54 | 50, 53 | reximddv 3172 |
. 2
β’ (((π β§ π₯ β π·) β§ π΄ β π₯) β βπ β π ((π΄πΏπ)(βGβπΊ)π· β§ πΆππ)) |
55 | 2, 3, 4, 5, 7, 9 | tglnpt2 27892 |
. 2
β’ (π β βπ₯ β π· π΄ β π₯) |
56 | 54, 55 | r19.29a 3163 |
1
β’ (π β βπ β π ((π΄πΏπ)(βGβπΊ)π· β§ πΆππ)) |