Proof of Theorem footexlem1
| 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 2743 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝑅) = (𝑌 − 𝑍)) |
| 12 | | footexlem.5 |
. . . . . . 7
⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘𝑅)‘𝑌)) |
| 13 | | footexlem.e |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
| 14 | | footexlem.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
| 15 | | footexlem.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ≠ 𝐹) |
| 16 | 15 | necomd 2996 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ≠ 𝐸) |
| 17 | | footexlem.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ (𝐹𝐼𝑌)) |
| 18 | 1, 2, 3, 4, 14, 13, 5, 16, 17 | btwnlng3 28629 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ (𝐹𝐿𝐸)) |
| 19 | 1, 2, 3, 4, 13, 14, 5, 15, 18 | lncom 28630 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝐸𝐿𝐹)) |
| 20 | | footexlem.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = (𝐸𝐿𝐹)) |
| 21 | 19, 20 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝐴) |
| 22 | | foot.y |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) |
| 23 | | nelne2 3040 |
. . . . . . . . 9
⊢ ((𝑌 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴) → 𝑌 ≠ 𝐶) |
| 24 | 21, 22, 23 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ≠ 𝐶) |
| 25 | 24 | necomd 2996 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ≠ 𝑌) |
| 26 | 12, 25 | eqnetrrd 3009 |
. . . . . 6
⊢ (𝜑 → (((pInvG‘𝐺)‘𝑅)‘𝑌) ≠ 𝑌) |
| 27 | | eqid 2737 |
. . . . . . . 8
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
| 28 | | eqid 2737 |
. . . . . . . 8
⊢
((pInvG‘𝐺)‘𝑅) = ((pInvG‘𝐺)‘𝑅) |
| 29 | 1, 8, 2, 3, 27, 4,
9, 28, 5 | mirinv 28674 |
. . . . . . 7
⊢ (𝜑 → ((((pInvG‘𝐺)‘𝑅)‘𝑌) = 𝑌 ↔ 𝑅 = 𝑌)) |
| 30 | 29 | necon3bid 2985 |
. . . . . 6
⊢ (𝜑 → ((((pInvG‘𝐺)‘𝑅)‘𝑌) ≠ 𝑌 ↔ 𝑅 ≠ 𝑌)) |
| 31 | 26, 30 | mpbid 232 |
. . . . 5
⊢ (𝜑 → 𝑅 ≠ 𝑌) |
| 32 | 31 | necomd 2996 |
. . . 4
⊢ (𝜑 → 𝑌 ≠ 𝑅) |
| 33 | 1, 8, 2, 4, 5, 9, 5, 6, 11, 32 | tgcgrneq 28491 |
. . 3
⊢ (𝜑 → 𝑌 ≠ 𝑍) |
| 34 | 33 | necomd 2996 |
. . . 4
⊢ (𝜑 → 𝑍 ≠ 𝑌) |
| 35 | | eqid 2737 |
. . . . 5
⊢
((pInvG‘𝐺)‘𝑍) = ((pInvG‘𝐺)‘𝑍) |
| 36 | | eqid 2737 |
. . . . 5
⊢
((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋) |
| 37 | | footexlem.q |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ 𝑃) |
| 38 | 1, 8, 2, 3, 27, 4,
6, 35, 37 | mircl 28669 |
. . . . 5
⊢ (𝜑 → (((pInvG‘𝐺)‘𝑍)‘𝑄) ∈ 𝑃) |
| 39 | | foot.x |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 40 | | footexlem.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 41 | 1, 8, 2, 3, 27, 4,
9, 28, 5 | mirbtwn 28666 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ ((((pInvG‘𝐺)‘𝑅)‘𝑌)𝐼𝑌)) |
| 42 | 12 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → (𝐶𝐼𝑌) = ((((pInvG‘𝐺)‘𝑅)‘𝑌)𝐼𝑌)) |
| 43 | 41, 42 | eleqtrrd 2844 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (𝐶𝐼𝑌)) |
| 44 | | footexlem.8 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝑅𝐼𝑄)) |
| 45 | 1, 8, 2, 4, 39, 9,
5, 37, 31, 43, 44 | tgbtwnouttr2 28503 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝐶𝐼𝑄)) |
| 46 | 1, 8, 2, 4, 39, 5,
37, 45 | tgbtwncom 28496 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ (𝑄𝐼𝐶)) |
| 47 | | footexlem.10 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ((((pInvG‘𝐺)‘𝑍)‘𝑄)𝐼𝐷)) |
| 48 | | eqid 2737 |
. . . . . . . 8
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
| 49 | | footexlem.4 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 − 𝑌) = (𝐸 − 𝐶)) |
| 50 | 12 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 − 𝐶) = (𝐸 − (((pInvG‘𝐺)‘𝑅)‘𝑌))) |
| 51 | 49, 50 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 − 𝑌) = (𝐸 − (((pInvG‘𝐺)‘𝑅)‘𝑌))) |
| 52 | 1, 8, 2, 3, 27, 4,
13, 9, 5 | israg 28705 |
. . . . . . . . 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 28488 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − 𝐸) = (𝐶 − 𝐸)) |
| 56 | 54, 55 | eqtr2d 2778 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 − 𝐸) = (𝑌 − 𝑄)) |
| 57 | 1, 2, 3, 4, 13, 14, 15 | tglinerflx1 28641 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 ∈ (𝐸𝐿𝐹)) |
| 58 | 57, 20 | eleqtrrd 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 ∈ 𝐴) |
| 59 | | nelne2 3040 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐸 ≠ 𝐶) |
| 60 | 58, 22, 59 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ≠ 𝐶) |
| 61 | 60 | necomd 2996 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ≠ 𝐸) |
| 62 | 1, 8, 2, 4, 39, 13, 5, 37, 56, 61 | tgcgrneq 28491 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ≠ 𝑄) |
| 63 | 62 | necomd 2996 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ≠ 𝑌) |
| 64 | 1, 8, 2, 4, 9, 5, 37, 44 | tgbtwncom 28496 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ (𝑄𝐼𝑅)) |
| 65 | | footexlem.6 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ (𝐸𝐼𝑍)) |
| 66 | 1, 8, 2, 4, 5, 37,
5, 13, 54 | tgcgrcomlr 28488 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 − 𝑌) = (𝐸 − 𝑌)) |
| 67 | 1, 8, 2, 4, 37, 13 | axtgcgrrflx 28470 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 − 𝐸) = (𝐸 − 𝑄)) |
| 68 | 54 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 − 𝐸) = (𝑌 − 𝑄)) |
| 69 | 1, 8, 2, 4, 37, 5,
9, 13, 5, 6, 13, 37, 63, 64, 65, 66, 11, 67, 68 | axtg5seg 28473 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 − 𝐸) = (𝑍 − 𝑄)) |
| 70 | 1, 8, 2, 4, 9, 13,
6, 37, 69 | tgcgrcomlr 28488 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 − 𝑅) = (𝑄 − 𝑍)) |
| 71 | 1, 8, 2, 4, 5, 9, 5, 6, 11 | tgcgrcomlr 28488 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 − 𝑌) = (𝑍 − 𝑌)) |
| 72 | 1, 8, 48, 4, 13, 9, 5, 37, 6,
5, 70, 71, 68 | trgcgr 28524 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝐸𝑅𝑌”〉(cgrG‘𝐺)〈“𝑄𝑍𝑌”〉) |
| 73 | 1, 8, 2, 3, 27, 4,
13, 9, 5, 48, 37, 6, 5, 53, 72 | ragcgr 28715 |
. . . . . . 7
⊢ (𝜑 → 〈“𝑄𝑍𝑌”〉 ∈ (∟G‘𝐺)) |
| 74 | 1, 8, 2, 3, 27, 4,
37, 6, 5, 73 | ragcom 28706 |
. . . . . 6
⊢ (𝜑 → 〈“𝑌𝑍𝑄”〉 ∈ (∟G‘𝐺)) |
| 75 | 1, 8, 2, 3, 27, 4,
5, 6, 37 | israg 28705 |
. . . . . 6
⊢ (𝜑 → (〈“𝑌𝑍𝑄”〉 ∈ (∟G‘𝐺) ↔ (𝑌 − 𝑄) = (𝑌 − (((pInvG‘𝐺)‘𝑍)‘𝑄)))) |
| 76 | 74, 75 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝑌 − 𝑄) = (𝑌 − (((pInvG‘𝐺)‘𝑍)‘𝑄))) |
| 77 | | footexlem.11 |
. . . . . 6
⊢ (𝜑 → (𝑌 − 𝐷) = (𝑌 − 𝐶)) |
| 78 | 77 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → (𝑌 − 𝐶) = (𝑌 − 𝐷)) |
| 79 | | eqidd 2738 |
. . . . 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 28699 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (𝑍𝐼𝑋)) |
| 82 | 1, 2, 3, 4, 6, 5, 7, 34, 81 | btwnlng3 28629 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (𝑍𝐿𝑌)) |
| 83 | 1, 2, 3, 4, 5, 6, 7, 33, 82 | lncom 28630 |
. 2
⊢ (𝜑 → 𝑋 ∈ (𝑌𝐿𝑍)) |
| 84 | | isperp.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ran 𝐿) |
| 85 | 49 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → (𝐸 − 𝐶) = (𝐸 − 𝑌)) |
| 86 | 1, 8, 2, 4, 13, 39, 13, 5, 85, 60 | tgcgrneq 28491 |
. . . . 5
⊢ (𝜑 → 𝐸 ≠ 𝑌) |
| 87 | 1, 2, 3, 4, 13, 5,
6, 86, 65 | btwnlng3 28629 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ (𝐸𝐿𝑌)) |
| 88 | 1, 2, 3, 4, 13, 5,
86, 86, 84, 58, 21 | tglinethru 28644 |
. . . 4
⊢ (𝜑 → 𝐴 = (𝐸𝐿𝑌)) |
| 89 | 87, 88 | eleqtrrd 2844 |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝐴) |
| 90 | 1, 2, 3, 4, 5, 6, 33, 33, 84, 21, 89 | tglinethru 28644 |
. 2
⊢ (𝜑 → 𝐴 = (𝑌𝐿𝑍)) |
| 91 | 83, 90 | eleqtrrd 2844 |
1
⊢ (𝜑 → 𝑋 ∈ 𝐴) |