Step | Hyp | Ref
| Expression |
1 | | lmiopp.p |
. . . . . 6
β’ π = (BaseβπΊ) |
2 | | lmiopp.m |
. . . . . 6
β’ β =
(distβπΊ) |
3 | | lmiopp.i |
. . . . . 6
β’ πΌ = (ItvβπΊ) |
4 | | lmiopp.l |
. . . . . 6
β’ πΏ = (LineGβπΊ) |
5 | | lmiopp.g |
. . . . . . . 8
β’ (π β πΊ β TarskiG) |
6 | 5 | ad4antr 731 |
. . . . . . 7
β’
(((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β πΊ β TarskiG) |
7 | 6 | adantr 482 |
. . . . . 6
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β πΊ β TarskiG) |
8 | | simprl 770 |
. . . . . . 7
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β π β π) |
9 | | lmiopp.d |
. . . . . . . . . 10
β’ (π β π· β ran πΏ) |
10 | | lnperpex.a |
. . . . . . . . . 10
β’ (π β π΄ β π·) |
11 | 1, 4, 3, 5, 9, 10 | tglnpt 27533 |
. . . . . . . . 9
β’ (π β π΄ β π) |
12 | 11 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π΄ β π) β π΄ β π) |
13 | 12 | ad3antrrr 729 |
. . . . . . 7
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β π΄ β π) |
14 | | simprrl 780 |
. . . . . . . . . 10
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β (π΄πΏπ)(βGβπΊ)π·) |
15 | 4, 7, 14 | perpln1 27694 |
. . . . . . . . 9
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β (π΄πΏπ) β ran πΏ) |
16 | 1, 3, 4, 7, 13, 8,
15 | tglnne 27612 |
. . . . . . . 8
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β π΄ β π) |
17 | 16 | necomd 3000 |
. . . . . . 7
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β π β π΄) |
18 | 1, 3, 4, 7, 8, 13,
17 | tgelrnln 27614 |
. . . . . 6
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β (ππΏπ΄) β ran πΏ) |
19 | 9 | ad4antr 731 |
. . . . . . 7
β’
(((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β π· β ran πΏ) |
20 | 19 | adantr 482 |
. . . . . 6
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β π· β ran πΏ) |
21 | 1, 3, 4, 7, 8, 13,
17 | tglinecom 27619 |
. . . . . . 7
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β (ππΏπ΄) = (π΄πΏπ)) |
22 | 21, 14 | eqbrtrd 5132 |
. . . . . 6
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β (ππΏπ΄)(βGβπΊ)π·) |
23 | 1, 2, 3, 4, 7, 18,
20, 22 | perpcom 27697 |
. . . . 5
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β π·(βGβπΊ)(ππΏπ΄)) |
24 | | simplr 768 |
. . . . . 6
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β πππ) |
25 | | lmiopp.o |
. . . . . . 7
β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} |
26 | | lnperpex.q |
. . . . . . . . 9
β’ (π β π β π) |
27 | 26 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β π β π) |
28 | 27 | adantr 482 |
. . . . . . 7
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β π β π) |
29 | | simplr 768 |
. . . . . . . 8
β’
(((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β π β π) |
30 | 29 | adantr 482 |
. . . . . . 7
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β π β π) |
31 | | simprrr 781 |
. . . . . . . 8
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β πππ) |
32 | 1, 2, 3, 25, 4, 20, 7, 30, 8, 31 | oppcom 27728 |
. . . . . . 7
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β πππ) |
33 | 1, 3, 4, 25, 7, 20, 8, 28, 30, 32 | lnopp2hpgb 27747 |
. . . . . 6
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β (πππ β π((hpGβπΊ)βπ·)π)) |
34 | 24, 33 | mpbid 231 |
. . . . 5
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β π((hpGβπΊ)βπ·)π) |
35 | 23, 34 | jca 513 |
. . . 4
β’
((((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β§ (π β π β§ ((π΄πΏπ)(βGβπΊ)π· β§ πππ))) β (π·(βGβπΊ)(ππΏπ΄) β§ π((hpGβπΊ)βπ·)π)) |
36 | | eqid 2737 |
. . . . 5
β’
(hlGβπΊ) =
(hlGβπΊ) |
37 | 10 | ad4antr 731 |
. . . . 5
β’
(((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β π΄ β π·) |
38 | | simpr 486 |
. . . . . 6
β’
(((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β πππ) |
39 | 1, 2, 3, 25, 4, 19, 6, 27, 29, 38 | oppne2 27726 |
. . . . 5
β’
(((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β Β¬ π β π·) |
40 | | lmiopp.h |
. . . . . 6
β’ (π β πΊDimTarskiGβ₯2) |
41 | 40 | ad4antr 731 |
. . . . 5
β’
(((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β πΊDimTarskiGβ₯2) |
42 | 1, 2, 3, 25, 4, 19, 6, 36, 37, 29, 39, 41 | oppperpex 27737 |
. . . 4
β’
(((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β βπ β π ((π΄πΏπ)(βGβπΊ)π· β§ πππ)) |
43 | 35, 42 | reximddv 3169 |
. . 3
β’
(((((π β§ π β π·) β§ π΄ β π) β§ π β π) β§ πππ) β βπ β π (π·(βGβπΊ)(ππΏπ΄) β§ π((hpGβπΊ)βπ·)π)) |
44 | | lnperpex.1 |
. . . . 5
β’ (π β Β¬ π β π·) |
45 | 1, 3, 4, 5, 9, 26,
25, 44 | hpgerlem 27749 |
. . . 4
β’ (π β βπ β π πππ) |
46 | 45 | ad2antrr 725 |
. . 3
β’ (((π β§ π β π·) β§ π΄ β π) β βπ β π πππ) |
47 | 43, 46 | r19.29a 3160 |
. 2
β’ (((π β§ π β π·) β§ π΄ β π) β βπ β π (π·(βGβπΊ)(ππΏπ΄) β§ π((hpGβπΊ)βπ·)π)) |
48 | 1, 3, 4, 5, 9, 10 | tglnpt2 27625 |
. 2
β’ (π β βπ β π· π΄ β π) |
49 | 47, 48 | r19.29a 3160 |
1
β’ (π β βπ β π (π·(βGβπΊ)(ππΏπ΄) β§ π((hpGβπΊ)βπ·)π)) |