Step | Hyp | Ref
| Expression |
1 | | isperp.p |
. . 3
β’ π = (BaseβπΊ) |
2 | | isperp.i |
. . 3
β’ πΌ = (ItvβπΊ) |
3 | | isperp.l |
. . 3
β’ πΏ = (LineGβπΊ) |
4 | | isperp.g |
. . 3
β’ (π β πΊ β TarskiG) |
5 | | footexlem.y |
. . 3
β’ (π β π β π) |
6 | | footexlem.z |
. . 3
β’ (π β π β π) |
7 | | footexlem.x |
. . 3
β’ (π β π β π) |
8 | | isperp.d |
. . . 4
β’ β =
(distβπΊ) |
9 | | footexlem.r |
. . . 4
β’ (π β π
β π) |
10 | | footexlem.7 |
. . . . 5
β’ (π β (π β π) = (π β π
)) |
11 | 10 | eqcomd 2739 |
. . . 4
β’ (π β (π β π
) = (π β π)) |
12 | | footexlem.5 |
. . . . . . 7
β’ (π β πΆ = (((pInvGβπΊ)βπ
)βπ)) |
13 | | footexlem.e |
. . . . . . . . . . 11
β’ (π β πΈ β π) |
14 | | footexlem.f |
. . . . . . . . . . 11
β’ (π β πΉ β π) |
15 | | footexlem.2 |
. . . . . . . . . . 11
β’ (π β πΈ β πΉ) |
16 | 15 | necomd 2997 |
. . . . . . . . . . . 12
β’ (π β πΉ β πΈ) |
17 | | footexlem.3 |
. . . . . . . . . . . 12
β’ (π β πΈ β (πΉπΌπ)) |
18 | 1, 2, 3, 4, 14, 13, 5, 16, 17 | btwnlng3 27872 |
. . . . . . . . . . 11
β’ (π β π β (πΉπΏπΈ)) |
19 | 1, 2, 3, 4, 13, 14, 5, 15, 18 | lncom 27873 |
. . . . . . . . . 10
β’ (π β π β (πΈπΏπΉ)) |
20 | | footexlem.1 |
. . . . . . . . . 10
β’ (π β π΄ = (πΈπΏπΉ)) |
21 | 19, 20 | eleqtrrd 2837 |
. . . . . . . . 9
β’ (π β π β π΄) |
22 | | foot.y |
. . . . . . . . 9
β’ (π β Β¬ πΆ β π΄) |
23 | | nelne2 3041 |
. . . . . . . . 9
β’ ((π β π΄ β§ Β¬ πΆ β π΄) β π β πΆ) |
24 | 21, 22, 23 | syl2anc 585 |
. . . . . . . 8
β’ (π β π β πΆ) |
25 | 24 | necomd 2997 |
. . . . . . 7
β’ (π β πΆ β π) |
26 | 12, 25 | eqnetrrd 3010 |
. . . . . 6
β’ (π β (((pInvGβπΊ)βπ
)βπ) β π) |
27 | | eqid 2733 |
. . . . . . . 8
β’
(pInvGβπΊ) =
(pInvGβπΊ) |
28 | | eqid 2733 |
. . . . . . . 8
β’
((pInvGβπΊ)βπ
) = ((pInvGβπΊ)βπ
) |
29 | 1, 8, 2, 3, 27, 4,
9, 28, 5 | mirinv 27917 |
. . . . . . 7
β’ (π β ((((pInvGβπΊ)βπ
)βπ) = π β π
= π)) |
30 | 29 | necon3bid 2986 |
. . . . . 6
β’ (π β ((((pInvGβπΊ)βπ
)βπ) β π β π
β π)) |
31 | 26, 30 | mpbid 231 |
. . . . 5
β’ (π β π
β π) |
32 | 31 | necomd 2997 |
. . . 4
β’ (π β π β π
) |
33 | 1, 8, 2, 4, 5, 9, 5, 6, 11, 32 | tgcgrneq 27734 |
. . 3
β’ (π β π β π) |
34 | 33 | necomd 2997 |
. . . 4
β’ (π β π β π) |
35 | | eqid 2733 |
. . . . 5
β’
((pInvGβπΊ)βπ) = ((pInvGβπΊ)βπ) |
36 | | eqid 2733 |
. . . . 5
β’
((pInvGβπΊ)βπ) = ((pInvGβπΊ)βπ) |
37 | | footexlem.q |
. . . . 5
β’ (π β π β π) |
38 | 1, 8, 2, 3, 27, 4,
6, 35, 37 | mircl 27912 |
. . . . 5
β’ (π β (((pInvGβπΊ)βπ)βπ) β π) |
39 | | foot.x |
. . . . 5
β’ (π β πΆ β π) |
40 | | footexlem.d |
. . . . 5
β’ (π β π· β π) |
41 | 1, 8, 2, 3, 27, 4,
9, 28, 5 | mirbtwn 27909 |
. . . . . . . 8
β’ (π β π
β ((((pInvGβπΊ)βπ
)βπ)πΌπ)) |
42 | 12 | oveq1d 7424 |
. . . . . . . 8
β’ (π β (πΆπΌπ) = ((((pInvGβπΊ)βπ
)βπ)πΌπ)) |
43 | 41, 42 | eleqtrrd 2837 |
. . . . . . 7
β’ (π β π
β (πΆπΌπ)) |
44 | | footexlem.8 |
. . . . . . 7
β’ (π β π β (π
πΌπ)) |
45 | 1, 8, 2, 4, 39, 9,
5, 37, 31, 43, 44 | tgbtwnouttr2 27746 |
. . . . . 6
β’ (π β π β (πΆπΌπ)) |
46 | 1, 8, 2, 4, 39, 5,
37, 45 | tgbtwncom 27739 |
. . . . 5
β’ (π β π β (ππΌπΆ)) |
47 | | footexlem.10 |
. . . . 5
β’ (π β π β ((((pInvGβπΊ)βπ)βπ)πΌπ·)) |
48 | | eqid 2733 |
. . . . . . . 8
β’
(cgrGβπΊ) =
(cgrGβπΊ) |
49 | | footexlem.4 |
. . . . . . . . . 10
β’ (π β (πΈ β π) = (πΈ β πΆ)) |
50 | 12 | oveq2d 7425 |
. . . . . . . . . 10
β’ (π β (πΈ β πΆ) = (πΈ β (((pInvGβπΊ)βπ
)βπ))) |
51 | 49, 50 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β (πΈ β π) = (πΈ β (((pInvGβπΊ)βπ
)βπ))) |
52 | 1, 8, 2, 3, 27, 4,
13, 9, 5 | israg 27948 |
. . . . . . . . 9
β’ (π β (β¨βπΈπ
πββ© β (βGβπΊ) β (πΈ β π) = (πΈ β (((pInvGβπΊ)βπ
)βπ)))) |
53 | 51, 52 | mpbird 257 |
. . . . . . . 8
β’ (π β β¨βπΈπ
πββ© β (βGβπΊ)) |
54 | | footexlem.9 |
. . . . . . . . . . . . . 14
β’ (π β (π β π) = (π β πΈ)) |
55 | 1, 8, 2, 4, 13, 5,
13, 39, 49 | tgcgrcomlr 27731 |
. . . . . . . . . . . . . 14
β’ (π β (π β πΈ) = (πΆ β πΈ)) |
56 | 54, 55 | eqtr2d 2774 |
. . . . . . . . . . . . 13
β’ (π β (πΆ β πΈ) = (π β π)) |
57 | 1, 2, 3, 4, 13, 14, 15 | tglinerflx1 27884 |
. . . . . . . . . . . . . . . 16
β’ (π β πΈ β (πΈπΏπΉ)) |
58 | 57, 20 | eleqtrrd 2837 |
. . . . . . . . . . . . . . 15
β’ (π β πΈ β π΄) |
59 | | nelne2 3041 |
. . . . . . . . . . . . . . 15
β’ ((πΈ β π΄ β§ Β¬ πΆ β π΄) β πΈ β πΆ) |
60 | 58, 22, 59 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β πΈ β πΆ) |
61 | 60 | necomd 2997 |
. . . . . . . . . . . . 13
β’ (π β πΆ β πΈ) |
62 | 1, 8, 2, 4, 39, 13, 5, 37, 56, 61 | tgcgrneq 27734 |
. . . . . . . . . . . 12
β’ (π β π β π) |
63 | 62 | necomd 2997 |
. . . . . . . . . . 11
β’ (π β π β π) |
64 | 1, 8, 2, 4, 9, 5, 37, 44 | tgbtwncom 27739 |
. . . . . . . . . . 11
β’ (π β π β (ππΌπ
)) |
65 | | footexlem.6 |
. . . . . . . . . . 11
β’ (π β π β (πΈπΌπ)) |
66 | 1, 8, 2, 4, 5, 37,
5, 13, 54 | tgcgrcomlr 27731 |
. . . . . . . . . . 11
β’ (π β (π β π) = (πΈ β π)) |
67 | 1, 8, 2, 4, 37, 13 | axtgcgrrflx 27713 |
. . . . . . . . . . 11
β’ (π β (π β πΈ) = (πΈ β π)) |
68 | 54 | eqcomd 2739 |
. . . . . . . . . . 11
β’ (π β (π β πΈ) = (π β π)) |
69 | 1, 8, 2, 4, 37, 5,
9, 13, 5, 6, 13, 37, 63, 64, 65, 66, 11, 67, 68 | axtg5seg 27716 |
. . . . . . . . . 10
β’ (π β (π
β πΈ) = (π β π)) |
70 | 1, 8, 2, 4, 9, 13,
6, 37, 69 | tgcgrcomlr 27731 |
. . . . . . . . 9
β’ (π β (πΈ β π
) = (π β π)) |
71 | 1, 8, 2, 4, 5, 9, 5, 6, 11 | tgcgrcomlr 27731 |
. . . . . . . . 9
β’ (π β (π
β π) = (π β π)) |
72 | 1, 8, 48, 4, 13, 9, 5, 37, 6,
5, 70, 71, 68 | trgcgr 27767 |
. . . . . . . 8
β’ (π β β¨βπΈπ
πββ©(cgrGβπΊ)β¨βπππββ©) |
73 | 1, 8, 2, 3, 27, 4,
13, 9, 5, 48, 37, 6, 5, 53, 72 | ragcgr 27958 |
. . . . . . 7
β’ (π β β¨βπππββ© β (βGβπΊ)) |
74 | 1, 8, 2, 3, 27, 4,
37, 6, 5, 73 | ragcom 27949 |
. . . . . 6
β’ (π β β¨βπππββ© β (βGβπΊ)) |
75 | 1, 8, 2, 3, 27, 4,
5, 6, 37 | israg 27948 |
. . . . . 6
β’ (π β (β¨βπππββ© β (βGβπΊ) β (π β π) = (π β (((pInvGβπΊ)βπ)βπ)))) |
76 | 74, 75 | mpbid 231 |
. . . . 5
β’ (π β (π β π) = (π β (((pInvGβπΊ)βπ)βπ))) |
77 | | footexlem.11 |
. . . . . 6
β’ (π β (π β π·) = (π β πΆ)) |
78 | 77 | eqcomd 2739 |
. . . . 5
β’ (π β (π β πΆ) = (π β π·)) |
79 | | eqidd 2734 |
. . . . 5
β’ (π β (((pInvGβπΊ)βπ)βπ) = (((pInvGβπΊ)βπ)βπ)) |
80 | | footexlem.12 |
. . . . 5
β’ (π β π· = (((pInvGβπΊ)βπ)βπΆ)) |
81 | 1, 8, 2, 3, 27, 4,
35, 36, 37, 38, 5, 39, 40, 6, 7, 46, 47, 76, 78, 79, 80 | krippen 27942 |
. . . 4
β’ (π β π β (ππΌπ)) |
82 | 1, 2, 3, 4, 6, 5, 7, 34, 81 | btwnlng3 27872 |
. . 3
β’ (π β π β (ππΏπ)) |
83 | 1, 2, 3, 4, 5, 6, 7, 33, 82 | lncom 27873 |
. 2
β’ (π β π β (ππΏπ)) |
84 | | isperp.a |
. . 3
β’ (π β π΄ β ran πΏ) |
85 | 49 | eqcomd 2739 |
. . . . . 6
β’ (π β (πΈ β πΆ) = (πΈ β π)) |
86 | 1, 8, 2, 4, 13, 39, 13, 5, 85, 60 | tgcgrneq 27734 |
. . . . 5
β’ (π β πΈ β π) |
87 | 1, 2, 3, 4, 13, 5,
6, 86, 65 | btwnlng3 27872 |
. . . 4
β’ (π β π β (πΈπΏπ)) |
88 | 1, 2, 3, 4, 13, 5,
86, 86, 84, 58, 21 | tglinethru 27887 |
. . . 4
β’ (π β π΄ = (πΈπΏπ)) |
89 | 87, 88 | eleqtrrd 2837 |
. . 3
β’ (π β π β π΄) |
90 | 1, 2, 3, 4, 5, 6, 33, 33, 84, 21, 89 | tglinethru 27887 |
. 2
β’ (π β π΄ = (ππΏπ)) |
91 | 83, 90 | eleqtrrd 2837 |
1
β’ (π β π β π΄) |