Proof of Theorem footexlem2
| Step | Hyp | Ref
| Expression |
| 1 | | isperp.p |
. 2
⊢ 𝑃 = (Base‘𝐺) |
| 2 | | isperp.d |
. 2
⊢ − =
(dist‘𝐺) |
| 3 | | isperp.i |
. 2
⊢ 𝐼 = (Itv‘𝐺) |
| 4 | | isperp.l |
. 2
⊢ 𝐿 = (LineG‘𝐺) |
| 5 | | isperp.g |
. 2
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 6 | | foot.x |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 7 | | footexlem.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
| 8 | | isperp.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ran 𝐿) |
| 9 | | foot.y |
. . . . . 6
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) |
| 10 | | footexlem.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
| 11 | | footexlem.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
| 12 | | footexlem.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ 𝑃) |
| 13 | | footexlem.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
| 14 | | footexlem.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑃) |
| 15 | | footexlem.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 16 | | footexlem.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 = (𝐸𝐿𝐹)) |
| 17 | | footexlem.2 |
. . . . . 6
⊢ (𝜑 → 𝐸 ≠ 𝐹) |
| 18 | | footexlem.3 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ (𝐹𝐼𝑌)) |
| 19 | | footexlem.4 |
. . . . . 6
⊢ (𝜑 → (𝐸 − 𝑌) = (𝐸 − 𝐶)) |
| 20 | | footexlem.5 |
. . . . . 6
⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘𝑅)‘𝑌)) |
| 21 | | footexlem.6 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝐸𝐼𝑍)) |
| 22 | | footexlem.7 |
. . . . . 6
⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 − 𝑅)) |
| 23 | | footexlem.q |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ 𝑃) |
| 24 | | footexlem.8 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝑅𝐼𝑄)) |
| 25 | | footexlem.9 |
. . . . . 6
⊢ (𝜑 → (𝑌 − 𝑄) = (𝑌 − 𝐸)) |
| 26 | | footexlem.10 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ((((pInvG‘𝐺)‘𝑍)‘𝑄)𝐼𝐷)) |
| 27 | | footexlem.11 |
. . . . . 6
⊢ (𝜑 → (𝑌 − 𝐷) = (𝑌 − 𝐶)) |
| 28 | | footexlem.12 |
. . . . . 6
⊢ (𝜑 → 𝐷 = (((pInvG‘𝐺)‘𝑋)‘𝐶)) |
| 29 | 1, 2, 3, 4, 5, 8, 6, 9, 10, 11, 12, 7, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28 | footexlem1 28727 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
| 30 | | nelne2 3040 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴) → 𝑋 ≠ 𝐶) |
| 31 | 29, 9, 30 | syl2anc 584 |
. . . 4
⊢ (𝜑 → 𝑋 ≠ 𝐶) |
| 32 | 31 | necomd 2996 |
. . 3
⊢ (𝜑 → 𝐶 ≠ 𝑋) |
| 33 | 1, 3, 4, 5, 6, 7, 32 | tgelrnln 28638 |
. 2
⊢ (𝜑 → (𝐶𝐿𝑋) ∈ ran 𝐿) |
| 34 | 1, 3, 4, 5, 6, 7, 32 | tglinerflx2 28642 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (𝐶𝐿𝑋)) |
| 35 | 34, 29 | elind 4200 |
. 2
⊢ (𝜑 → 𝑋 ∈ ((𝐶𝐿𝑋) ∩ 𝐴)) |
| 36 | 1, 3, 4, 5, 6, 7, 32 | tglinerflx1 28641 |
. 2
⊢ (𝜑 → 𝐶 ∈ (𝐶𝐿𝑋)) |
| 37 | 17 | necomd 2996 |
. . . . 5
⊢ (𝜑 → 𝐹 ≠ 𝐸) |
| 38 | 1, 3, 4, 5, 11, 10, 13, 37, 18 | btwnlng3 28629 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (𝐹𝐿𝐸)) |
| 39 | 1, 3, 4, 5, 10, 11, 13, 17, 38 | lncom 28630 |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝐸𝐿𝐹)) |
| 40 | 39, 16 | eleqtrrd 2844 |
. 2
⊢ (𝜑 → 𝑌 ∈ 𝐴) |
| 41 | | eqid 2737 |
. . . . 5
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
| 42 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐺 ∈ TarskiG) |
| 43 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐸 ∈ 𝑃) |
| 44 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑌 ∈ 𝑃) |
| 45 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑅 ∈ 𝑃) |
| 46 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐶 ∈ 𝑃) |
| 47 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐶 = 𝐶) |
| 48 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑌 = 𝑋) |
| 49 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐸 = 𝐸) |
| 50 | 47, 48, 49 | s3eqd 14903 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 〈“𝐶𝑌𝐸”〉 = 〈“𝐶𝑋𝐸”〉) |
| 51 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑋 ∈ 𝑃) |
| 52 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ∈ 𝑃) |
| 53 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
((pInvG‘𝐺)‘𝑍) = ((pInvG‘𝐺)‘𝑍) |
| 54 | 1, 2, 3, 4, 41, 5,
14, 53, 23 | mircl 28669 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((pInvG‘𝐺)‘𝑍)‘𝑄) ∈ 𝑃) |
| 55 | 1, 2, 3, 5, 10, 13, 10, 6, 19 | tgcgrcomlr 28488 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑌 − 𝐸) = (𝐶 − 𝐸)) |
| 56 | 25, 55 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐶 − 𝐸) = (𝑌 − 𝑄)) |
| 57 | 1, 3, 4, 5, 10, 11, 17 | tglinerflx1 28641 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐸 ∈ (𝐸𝐿𝐹)) |
| 58 | 57, 16 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐸 ∈ 𝐴) |
| 59 | | nelne2 3040 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴) → 𝐸 ≠ 𝐶) |
| 60 | 58, 9, 59 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐸 ≠ 𝐶) |
| 61 | 60 | necomd 2996 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ≠ 𝐸) |
| 62 | 1, 2, 3, 5, 6, 10,
13, 23, 56, 61 | tgcgrneq 28491 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ≠ 𝑄) |
| 63 | 62 | necomd 2996 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑄 ≠ 𝑌) |
| 64 | | nelne2 3040 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑌 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴) → 𝑌 ≠ 𝐶) |
| 65 | 40, 9, 64 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑌 ≠ 𝐶) |
| 66 | 65 | necomd 2996 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐶 ≠ 𝑌) |
| 67 | 20, 66 | eqnetrrd 3009 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((pInvG‘𝐺)‘𝑅)‘𝑌) ≠ 𝑌) |
| 68 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((pInvG‘𝐺)‘𝑅) = ((pInvG‘𝐺)‘𝑅) |
| 69 | 1, 2, 3, 4, 41, 5,
12, 68, 13 | mirinv 28674 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((((pInvG‘𝐺)‘𝑅)‘𝑌) = 𝑌 ↔ 𝑅 = 𝑌)) |
| 70 | 69 | necon3bid 2985 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((pInvG‘𝐺)‘𝑅)‘𝑌) ≠ 𝑌 ↔ 𝑅 ≠ 𝑌)) |
| 71 | 67, 70 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 ≠ 𝑌) |
| 72 | 1, 2, 3, 4, 41, 5,
12, 68, 13 | mirbtwn 28666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑅 ∈ ((((pInvG‘𝐺)‘𝑅)‘𝑌)𝐼𝑌)) |
| 73 | 20 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐶𝐼𝑌) = ((((pInvG‘𝐺)‘𝑅)‘𝑌)𝐼𝑌)) |
| 74 | 72, 73 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 ∈ (𝐶𝐼𝑌)) |
| 75 | 1, 2, 3, 5, 6, 12,
13, 23, 71, 74, 24 | tgbtwnouttr2 28503 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ (𝐶𝐼𝑄)) |
| 76 | 1, 2, 3, 5, 6, 13,
23, 75 | tgbtwncom 28496 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ (𝑄𝐼𝐶)) |
| 77 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
| 78 | 20 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐸 − 𝐶) = (𝐸 − (((pInvG‘𝐺)‘𝑅)‘𝑌))) |
| 79 | 19, 78 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐸 − 𝑌) = (𝐸 − (((pInvG‘𝐺)‘𝑅)‘𝑌))) |
| 80 | 1, 2, 3, 4, 41, 5,
10, 12, 13 | israg 28705 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (〈“𝐸𝑅𝑌”〉 ∈ (∟G‘𝐺) ↔ (𝐸 − 𝑌) = (𝐸 − (((pInvG‘𝐺)‘𝑅)‘𝑌)))) |
| 81 | 79, 80 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 〈“𝐸𝑅𝑌”〉 ∈ (∟G‘𝐺)) |
| 82 | 1, 2, 3, 5, 12, 13, 23, 24 | tgbtwncom 28496 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑌 ∈ (𝑄𝐼𝑅)) |
| 83 | 1, 2, 3, 5, 13, 23, 13, 10, 25 | tgcgrcomlr 28488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑄 − 𝑌) = (𝐸 − 𝑌)) |
| 84 | 22 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑌 − 𝑅) = (𝑌 − 𝑍)) |
| 85 | 1, 2, 3, 5, 23, 10 | axtgcgrrflx 28470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑄 − 𝐸) = (𝐸 − 𝑄)) |
| 86 | 25 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑌 − 𝐸) = (𝑌 − 𝑄)) |
| 87 | 1, 2, 3, 5, 23, 13, 12, 10, 13, 14, 10, 23, 63, 82, 21, 83, 84, 85, 86 | axtg5seg 28473 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑅 − 𝐸) = (𝑍 − 𝑄)) |
| 88 | 1, 2, 3, 5, 12, 10, 14, 23, 87 | tgcgrcomlr 28488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐸 − 𝑅) = (𝑄 − 𝑍)) |
| 89 | 1, 2, 3, 5, 13, 12, 13, 14, 84 | tgcgrcomlr 28488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑅 − 𝑌) = (𝑍 − 𝑌)) |
| 90 | 1, 2, 77, 5, 10, 12, 13, 23, 14, 13, 88, 89, 86 | trgcgr 28524 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 〈“𝐸𝑅𝑌”〉(cgrG‘𝐺)〈“𝑄𝑍𝑌”〉) |
| 91 | 1, 2, 3, 4, 41, 5,
10, 12, 13, 77, 23, 14, 13, 81, 90 | ragcgr 28715 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 〈“𝑄𝑍𝑌”〉 ∈ (∟G‘𝐺)) |
| 92 | 1, 2, 3, 4, 41, 5,
23, 14, 13, 91 | ragcom 28706 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 〈“𝑌𝑍𝑄”〉 ∈ (∟G‘𝐺)) |
| 93 | 1, 2, 3, 4, 41, 5,
13, 14, 23 | israg 28705 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (〈“𝑌𝑍𝑄”〉 ∈ (∟G‘𝐺) ↔ (𝑌 − 𝑄) = (𝑌 − (((pInvG‘𝐺)‘𝑍)‘𝑄)))) |
| 94 | 92, 93 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑌 − 𝑄) = (𝑌 − (((pInvG‘𝐺)‘𝑍)‘𝑄))) |
| 95 | 1, 2, 3, 5, 13, 23, 13, 54, 94 | tgcgrcomlr 28488 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 − 𝑌) = ((((pInvG‘𝐺)‘𝑍)‘𝑄) − 𝑌)) |
| 96 | 27 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 − 𝐶) = (𝑌 − 𝐷)) |
| 97 | 1, 2, 3, 4, 41, 5,
14, 53, 23 | mircgr 28665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑍 − (((pInvG‘𝐺)‘𝑍)‘𝑄)) = (𝑍 − 𝑄)) |
| 98 | 97 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑍 − 𝑄) = (𝑍 − (((pInvG‘𝐺)‘𝑍)‘𝑄))) |
| 99 | 1, 2, 3, 5, 14, 23, 14, 54, 98 | tgcgrcomlr 28488 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 − 𝑍) = ((((pInvG‘𝐺)‘𝑍)‘𝑄) − 𝑍)) |
| 100 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 − 𝑍) = (𝑌 − 𝑍)) |
| 101 | 1, 2, 3, 5, 23, 13, 6, 54, 13, 15, 14, 14, 63, 76, 26, 95, 96, 99, 100 | axtg5seg 28473 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 − 𝑍) = (𝐷 − 𝑍)) |
| 102 | 1, 2, 3, 5, 6, 14,
15, 14, 101 | tgcgrcomlr 28488 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑍 − 𝐶) = (𝑍 − 𝐷)) |
| 103 | 28 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑍 − 𝐷) = (𝑍 − (((pInvG‘𝐺)‘𝑋)‘𝐶))) |
| 104 | 102, 103 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑍 − 𝐶) = (𝑍 − (((pInvG‘𝐺)‘𝑋)‘𝐶))) |
| 105 | 1, 2, 3, 4, 41, 5,
14, 7, 6 | israg 28705 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈“𝑍𝑋𝐶”〉 ∈ (∟G‘𝐺) ↔ (𝑍 − 𝐶) = (𝑍 − (((pInvG‘𝐺)‘𝑋)‘𝐶)))) |
| 106 | 104, 105 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝜑 → 〈“𝑍𝑋𝐶”〉 ∈ (∟G‘𝐺)) |
| 107 | 106 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 〈“𝑍𝑋𝐶”〉 ∈ (∟G‘𝐺)) |
| 108 | 71 | necomd 2996 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ≠ 𝑅) |
| 109 | 1, 2, 3, 5, 13, 12, 13, 14, 84, 108 | tgcgrneq 28491 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ≠ 𝑍) |
| 110 | 109 | necomd 2996 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ≠ 𝑌) |
| 111 | 110 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ≠ 𝑌) |
| 112 | 111, 48 | neeqtrd 3010 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ≠ 𝑋) |
| 113 | 19 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 − 𝐶) = (𝐸 − 𝑌)) |
| 114 | 113 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → (𝐸 − 𝐶) = (𝐸 − 𝑌)) |
| 115 | 60 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐸 ≠ 𝐶) |
| 116 | 1, 2, 3, 42, 43, 46, 43, 44, 114, 115 | tgcgrneq 28491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐸 ≠ 𝑌) |
| 117 | 116 | necomd 2996 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑌 ≠ 𝐸) |
| 118 | 1, 2, 3, 5, 10, 6,
10, 13, 113, 60 | tgcgrneq 28491 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 ≠ 𝑌) |
| 119 | 1, 3, 4, 5, 10, 13, 14, 118, 21 | btwnlng3 28629 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ∈ (𝐸𝐿𝑌)) |
| 120 | 119 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ∈ (𝐸𝐿𝑌)) |
| 121 | 1, 3, 4, 42, 44, 43, 52, 117, 120 | lncom 28630 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ∈ (𝑌𝐿𝐸)) |
| 122 | 48 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → (𝑌𝐿𝐸) = (𝑋𝐿𝐸)) |
| 123 | 121, 122 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑍 ∈ (𝑋𝐿𝐸)) |
| 124 | 123 | orcd 874 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → (𝑍 ∈ (𝑋𝐿𝐸) ∨ 𝑋 = 𝐸)) |
| 125 | 1, 2, 3, 4, 41, 42, 52, 51, 46, 43, 107, 112, 124 | ragcol 28707 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 〈“𝐸𝑋𝐶”〉 ∈ (∟G‘𝐺)) |
| 126 | 1, 2, 3, 4, 41, 42, 43, 51, 46, 125 | ragcom 28706 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 〈“𝐶𝑋𝐸”〉 ∈ (∟G‘𝐺)) |
| 127 | 50, 126 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 〈“𝐶𝑌𝐸”〉 ∈ (∟G‘𝐺)) |
| 128 | 66 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝐶 ≠ 𝑌) |
| 129 | 1, 2, 3, 5, 6, 12,
13, 74 | tgbtwncom 28496 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ (𝑌𝐼𝐶)) |
| 130 | 1, 4, 3, 5, 13, 12, 6, 129 | btwncolg3 28565 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ (𝑌𝐿𝑅) ∨ 𝑌 = 𝑅)) |
| 131 | 130 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → (𝐶 ∈ (𝑌𝐿𝑅) ∨ 𝑌 = 𝑅)) |
| 132 | 1, 2, 3, 4, 41, 42, 46, 44, 43, 45, 127, 128, 131 | ragcol 28707 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 〈“𝑅𝑌𝐸”〉 ∈ (∟G‘𝐺)) |
| 133 | 1, 2, 3, 4, 41, 42, 45, 44, 43, 132 | ragcom 28706 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 〈“𝐸𝑌𝑅”〉 ∈ (∟G‘𝐺)) |
| 134 | 81 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 〈“𝐸𝑅𝑌”〉 ∈ (∟G‘𝐺)) |
| 135 | 1, 2, 3, 4, 41, 42, 43, 44, 45, 133, 134 | ragflat 28712 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑌 = 𝑅) |
| 136 | 108 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → 𝑌 ≠ 𝑅) |
| 137 | 136 | neneqd 2945 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑋) → ¬ 𝑌 = 𝑅) |
| 138 | 135, 137 | pm2.65da 817 |
. . 3
⊢ (𝜑 → ¬ 𝑌 = 𝑋) |
| 139 | 138 | neqned 2947 |
. 2
⊢ (𝜑 → 𝑌 ≠ 𝑋) |
| 140 | 28 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (𝑌 − 𝐷) = (𝑌 − (((pInvG‘𝐺)‘𝑋)‘𝐶))) |
| 141 | 96, 140 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝑌 − 𝐶) = (𝑌 − (((pInvG‘𝐺)‘𝑋)‘𝐶))) |
| 142 | 1, 2, 3, 4, 41, 5,
13, 7, 6 | israg 28705 |
. . . 4
⊢ (𝜑 → (〈“𝑌𝑋𝐶”〉 ∈ (∟G‘𝐺) ↔ (𝑌 − 𝐶) = (𝑌 − (((pInvG‘𝐺)‘𝑋)‘𝐶)))) |
| 143 | 141, 142 | mpbird 257 |
. . 3
⊢ (𝜑 → 〈“𝑌𝑋𝐶”〉 ∈ (∟G‘𝐺)) |
| 144 | 1, 2, 3, 4, 41, 5,
13, 7, 6, 143 | ragcom 28706 |
. 2
⊢ (𝜑 → 〈“𝐶𝑋𝑌”〉 ∈ (∟G‘𝐺)) |
| 145 | 1, 2, 3, 4, 5, 33,
8, 35, 36, 40, 32, 139, 144 | ragperp 28725 |
1
⊢ (𝜑 → (𝐶𝐿𝑋)(⟂G‘𝐺)𝐴) |