Step | Hyp | Ref
| Expression |
1 | | tglineintmo.p |
. . . . . . . 8
β’ π = (BaseβπΊ) |
2 | | tglineintmo.i |
. . . . . . . 8
β’ πΌ = (ItvβπΊ) |
3 | | tglineintmo.l |
. . . . . . . 8
β’ πΏ = (LineGβπΊ) |
4 | | tglineintmo.g |
. . . . . . . . 9
β’ (π β πΊ β TarskiG) |
5 | 4 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β πΊ β TarskiG) |
6 | | colline.1 |
. . . . . . . . 9
β’ (π β π β π) |
7 | 6 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β π β π) |
8 | | simplr 768 |
. . . . . . . 8
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β π₯ β π) |
9 | | simpr 486 |
. . . . . . . 8
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β π β π₯) |
10 | 1, 2, 3, 5, 7, 8, 9 | tgelrnln 27621 |
. . . . . . 7
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β (ππΏπ₯) β ran πΏ) |
11 | 1, 2, 3, 5, 7, 8, 9 | tglinerflx1 27624 |
. . . . . . 7
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β π β (ππΏπ₯)) |
12 | | simp-4r 783 |
. . . . . . . 8
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β π = π) |
13 | | simpllr 775 |
. . . . . . . . 9
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β π = π) |
14 | 13, 11 | eqeltrrd 2835 |
. . . . . . . 8
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β π β (ππΏπ₯)) |
15 | 12, 14 | eqeltrd 2834 |
. . . . . . 7
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β π β (ππΏπ₯)) |
16 | | eleq2 2823 |
. . . . . . . . 9
β’ (π = (ππΏπ₯) β (π β π β π β (ππΏπ₯))) |
17 | | eleq2 2823 |
. . . . . . . . 9
β’ (π = (ππΏπ₯) β (π β π β π β (ππΏπ₯))) |
18 | | eleq2 2823 |
. . . . . . . . 9
β’ (π = (ππΏπ₯) β (π β π β π β (ππΏπ₯))) |
19 | 16, 17, 18 | 3anbi123d 1437 |
. . . . . . . 8
β’ (π = (ππΏπ₯) β ((π β π β§ π β π β§ π β π) β (π β (ππΏπ₯) β§ π β (ππΏπ₯) β§ π β (ππΏπ₯)))) |
20 | 19 | rspcev 3583 |
. . . . . . 7
β’ (((ππΏπ₯) β ran πΏ β§ (π β (ππΏπ₯) β§ π β (ππΏπ₯) β§ π β (ππΏπ₯))) β βπ β ran πΏ(π β π β§ π β π β§ π β π)) |
21 | 10, 11, 15, 14, 20 | syl13anc 1373 |
. . . . . 6
β’
(((((π β§ π = π) β§ π = π) β§ π₯ β π) β§ π β π₯) β βπ β ran πΏ(π β π β§ π β π β§ π β π)) |
22 | | eqid 2733 |
. . . . . . . 8
β’
(distβπΊ) =
(distβπΊ) |
23 | | colline.4 |
. . . . . . . 8
β’ (π β 2 β€
(β―βπ)) |
24 | 1, 22, 2, 4, 23, 6 | tglowdim1i 27492 |
. . . . . . 7
β’ (π β βπ₯ β π π β π₯) |
25 | 24 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π = π) β§ π = π) β βπ₯ β π π β π₯) |
26 | 21, 25 | r19.29a 3156 |
. . . . 5
β’ (((π β§ π = π) β§ π = π) β βπ β ran πΏ(π β π β§ π β π β§ π β π)) |
27 | 4 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π = π) β§ π β π) β πΊ β TarskiG) |
28 | 6 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π = π) β§ π β π) β π β π) |
29 | | colline.3 |
. . . . . . . 8
β’ (π β π β π) |
30 | 29 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π = π) β§ π β π) β π β π) |
31 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π = π) β§ π β π) β π β π) |
32 | 1, 2, 3, 27, 28, 30, 31 | tgelrnln 27621 |
. . . . . 6
β’ (((π β§ π = π) β§ π β π) β (ππΏπ) β ran πΏ) |
33 | 1, 2, 3, 27, 28, 30, 31 | tglinerflx1 27624 |
. . . . . 6
β’ (((π β§ π = π) β§ π β π) β π β (ππΏπ)) |
34 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π = π) β§ π β π) β π = π) |
35 | 1, 2, 3, 27, 28, 30, 31 | tglinerflx2 27625 |
. . . . . . 7
β’ (((π β§ π = π) β§ π β π) β π β (ππΏπ)) |
36 | 34, 35 | eqeltrd 2834 |
. . . . . 6
β’ (((π β§ π = π) β§ π β π) β π β (ππΏπ)) |
37 | | eleq2 2823 |
. . . . . . . 8
β’ (π = (ππΏπ) β (π β π β π β (ππΏπ))) |
38 | | eleq2 2823 |
. . . . . . . 8
β’ (π = (ππΏπ) β (π β π β π β (ππΏπ))) |
39 | | eleq2 2823 |
. . . . . . . 8
β’ (π = (ππΏπ) β (π β π β π β (ππΏπ))) |
40 | 37, 38, 39 | 3anbi123d 1437 |
. . . . . . 7
β’ (π = (ππΏπ) β ((π β π β§ π β π β§ π β π) β (π β (ππΏπ) β§ π β (ππΏπ) β§ π β (ππΏπ)))) |
41 | 40 | rspcev 3583 |
. . . . . 6
β’ (((ππΏπ) β ran πΏ β§ (π β (ππΏπ) β§ π β (ππΏπ) β§ π β (ππΏπ))) β βπ β ran πΏ(π β π β§ π β π β§ π β π)) |
42 | 32, 33, 36, 35, 41 | syl13anc 1373 |
. . . . 5
β’ (((π β§ π = π) β§ π β π) β βπ β ran πΏ(π β π β§ π β π β§ π β π)) |
43 | 26, 42 | pm2.61dane 3029 |
. . . 4
β’ ((π β§ π = π) β βπ β ran πΏ(π β π β§ π β π β§ π β π)) |
44 | 43 | adantlr 714 |
. . 3
β’ (((π β§ (π β (ππΏπ) β¨ π = π)) β§ π = π) β βπ β ran πΏ(π β π β§ π β π β§ π β π)) |
45 | | simpll 766 |
. . . . 5
β’ (((π β§ (π β (ππΏπ) β¨ π = π)) β§ π β π) β π) |
46 | | simpr 486 |
. . . . . . 7
β’ (((π β§ (π β (ππΏπ) β¨ π = π)) β§ π β π) β π β π) |
47 | 46 | neneqd 2945 |
. . . . . 6
β’ (((π β§ (π β (ππΏπ) β¨ π = π)) β§ π β π) β Β¬ π = π) |
48 | | simplr 768 |
. . . . . 6
β’ (((π β§ (π β (ππΏπ) β¨ π = π)) β§ π β π) β (π β (ππΏπ) β¨ π = π)) |
49 | | orel2 890 |
. . . . . 6
β’ (Β¬
π = π β ((π β (ππΏπ) β¨ π = π) β π β (ππΏπ))) |
50 | 47, 48, 49 | sylc 65 |
. . . . 5
β’ (((π β§ (π β (ππΏπ) β¨ π = π)) β§ π β π) β π β (ππΏπ)) |
51 | 4 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β (ππΏπ)) β§ π β π) β πΊ β TarskiG) |
52 | | colline.2 |
. . . . . . 7
β’ (π β π β π) |
53 | 52 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β (ππΏπ)) β§ π β π) β π β π) |
54 | 29 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β (ππΏπ)) β§ π β π) β π β π) |
55 | | simpr 486 |
. . . . . 6
β’ (((π β§ π β (ππΏπ)) β§ π β π) β π β π) |
56 | 1, 2, 3, 51, 53, 54, 55 | tgelrnln 27621 |
. . . . 5
β’ (((π β§ π β (ππΏπ)) β§ π β π) β (ππΏπ) β ran πΏ) |
57 | 45, 50, 46, 56 | syl21anc 837 |
. . . 4
β’ (((π β§ (π β (ππΏπ) β¨ π = π)) β§ π β π) β (ππΏπ) β ran πΏ) |
58 | 1, 2, 3, 51, 53, 54, 55 | tglinerflx1 27624 |
. . . . 5
β’ (((π β§ π β (ππΏπ)) β§ π β π) β π β (ππΏπ)) |
59 | 45, 50, 46, 58 | syl21anc 837 |
. . . 4
β’ (((π β§ (π β (ππΏπ) β¨ π = π)) β§ π β π) β π β (ππΏπ)) |
60 | 1, 2, 3, 51, 53, 54, 55 | tglinerflx2 27625 |
. . . . 5
β’ (((π β§ π β (ππΏπ)) β§ π β π) β π β (ππΏπ)) |
61 | 45, 50, 46, 60 | syl21anc 837 |
. . . 4
β’ (((π β§ (π β (ππΏπ) β¨ π = π)) β§ π β π) β π β (ππΏπ)) |
62 | | eleq2 2823 |
. . . . . 6
β’ (π = (ππΏπ) β (π β π β π β (ππΏπ))) |
63 | | eleq2 2823 |
. . . . . 6
β’ (π = (ππΏπ) β (π β π β π β (ππΏπ))) |
64 | | eleq2 2823 |
. . . . . 6
β’ (π = (ππΏπ) β (π β π β π β (ππΏπ))) |
65 | 62, 63, 64 | 3anbi123d 1437 |
. . . . 5
β’ (π = (ππΏπ) β ((π β π β§ π β π β§ π β π) β (π β (ππΏπ) β§ π β (ππΏπ) β§ π β (ππΏπ)))) |
66 | 65 | rspcev 3583 |
. . . 4
β’ (((ππΏπ) β ran πΏ β§ (π β (ππΏπ) β§ π β (ππΏπ) β§ π β (ππΏπ))) β βπ β ran πΏ(π β π β§ π β π β§ π β π)) |
67 | 57, 50, 59, 61, 66 | syl13anc 1373 |
. . 3
β’ (((π β§ (π β (ππΏπ) β¨ π = π)) β§ π β π) β βπ β ran πΏ(π β π β§ π β π β§ π β π)) |
68 | 44, 67 | pm2.61dane 3029 |
. 2
β’ ((π β§ (π β (ππΏπ) β¨ π = π)) β βπ β ran πΏ(π β π β§ π β π β§ π β π)) |
69 | | df-ne 2941 |
. . . . . 6
β’ (π β π β Β¬ π = π) |
70 | | simplr1 1216 |
. . . . . . . 8
β’ ((((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β§ π β π) β π β π) |
71 | 4 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β§ π β π) β πΊ β TarskiG) |
72 | 52 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β§ π β π) β π β π) |
73 | 29 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β§ π β π) β π β π) |
74 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β§ π β π) β π β π) |
75 | | simpllr 775 |
. . . . . . . . 9
β’ ((((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β§ π β π) β π β ran πΏ) |
76 | | simplr2 1217 |
. . . . . . . . 9
β’ ((((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β§ π β π) β π β π) |
77 | | simplr3 1218 |
. . . . . . . . 9
β’ ((((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β§ π β π) β π β π) |
78 | 1, 2, 3, 71, 72, 73, 74, 74, 75, 76, 77 | tglinethru 27627 |
. . . . . . . 8
β’ ((((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β§ π β π) β π = (ππΏπ)) |
79 | 70, 78 | eleqtrd 2836 |
. . . . . . 7
β’ ((((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β§ π β π) β π β (ππΏπ)) |
80 | 79 | ex 414 |
. . . . . 6
β’ (((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β (π β π β π β (ππΏπ))) |
81 | 69, 80 | biimtrrid 242 |
. . . . 5
β’ (((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β (Β¬ π = π β π β (ππΏπ))) |
82 | 81 | orrd 862 |
. . . 4
β’ (((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β (π = π β¨ π β (ππΏπ))) |
83 | 82 | orcomd 870 |
. . 3
β’ (((π β§ π β ran πΏ) β§ (π β π β§ π β π β§ π β π)) β (π β (ππΏπ) β¨ π = π)) |
84 | 83 | r19.29an 3152 |
. 2
β’ ((π β§ βπ β ran πΏ(π β π β§ π β π β§ π β π)) β (π β (ππΏπ) β¨ π = π)) |
85 | 68, 84 | impbida 800 |
1
β’ (π β ((π β (ππΏπ) β¨ π = π) β βπ β ran πΏ(π β π β§ π β π β§ π β π))) |