Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  footexlem2 Structured version   Visualization version   GIF version

Theorem footexlem2 26528
 Description: Lemma for footex 26529. (Contributed by Thierry Arnoux, 19-Oct-2019.) (Revised by Thierry Arnoux, 1-Jul-2023.)
Hypotheses
Ref Expression
isperp.p 𝑃 = (Base‘𝐺)
isperp.d = (dist‘𝐺)
isperp.i 𝐼 = (Itv‘𝐺)
isperp.l 𝐿 = (LineG‘𝐺)
isperp.g (𝜑𝐺 ∈ TarskiG)
isperp.a (𝜑𝐴 ∈ ran 𝐿)
foot.x (𝜑𝐶𝑃)
foot.y (𝜑 → ¬ 𝐶𝐴)
footexlem.e (𝜑𝐸𝑃)
footexlem.f (𝜑𝐹𝑃)
footexlem.r (𝜑𝑅𝑃)
footexlem.x (𝜑𝑋𝑃)
footexlem.y (𝜑𝑌𝑃)
footexlem.z (𝜑𝑍𝑃)
footexlem.d (𝜑𝐷𝑃)
footexlem.1 (𝜑𝐴 = (𝐸𝐿𝐹))
footexlem.2 (𝜑𝐸𝐹)
footexlem.3 (𝜑𝐸 ∈ (𝐹𝐼𝑌))
footexlem.4 (𝜑 → (𝐸 𝑌) = (𝐸 𝐶))
footexlem.5 (𝜑𝐶 = (((pInvG‘𝐺)‘𝑅)‘𝑌))
footexlem.6 (𝜑𝑌 ∈ (𝐸𝐼𝑍))
footexlem.7 (𝜑 → (𝑌 𝑍) = (𝑌 𝑅))
footexlem.q (𝜑𝑄𝑃)
footexlem.8 (𝜑𝑌 ∈ (𝑅𝐼𝑄))
footexlem.9 (𝜑 → (𝑌 𝑄) = (𝑌 𝐸))
footexlem.10 (𝜑𝑌 ∈ ((((pInvG‘𝐺)‘𝑍)‘𝑄)𝐼𝐷))
footexlem.11 (𝜑 → (𝑌 𝐷) = (𝑌 𝐶))
footexlem.12 (𝜑𝐷 = (((pInvG‘𝐺)‘𝑋)‘𝐶))
Assertion
Ref Expression
footexlem2 (𝜑 → (𝐶𝐿𝑋)(⟂G‘𝐺)𝐴)

Proof of Theorem footexlem2
StepHypRef 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‘𝐺)‘𝑋)‘𝐶))
291, 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, 28footexlem1 26527 . . . . 5 (𝜑𝑋𝐴)
30 nelne2 3084 . . . . 5 ((𝑋𝐴 ∧ ¬ 𝐶𝐴) → 𝑋𝐶)
3129, 9, 30syl2anc 587 . . . 4 (𝜑𝑋𝐶)
3231necomd 3042 . . 3 (𝜑𝐶𝑋)
331, 3, 4, 5, 6, 7, 32tgelrnln 26438 . 2 (𝜑 → (𝐶𝐿𝑋) ∈ ran 𝐿)
341, 3, 4, 5, 6, 7, 32tglinerflx2 26442 . . 3 (𝜑𝑋 ∈ (𝐶𝐿𝑋))
3534, 29elind 4121 . 2 (𝜑𝑋 ∈ ((𝐶𝐿𝑋) ∩ 𝐴))
361, 3, 4, 5, 6, 7, 32tglinerflx1 26441 . 2 (𝜑𝐶 ∈ (𝐶𝐿𝑋))
3717necomd 3042 . . . . 5 (𝜑𝐹𝐸)
381, 3, 4, 5, 11, 10, 13, 37, 18btwnlng3 26429 . . . 4 (𝜑𝑌 ∈ (𝐹𝐿𝐸))
391, 3, 4, 5, 10, 11, 13, 17, 38lncom 26430 . . 3 (𝜑𝑌 ∈ (𝐸𝐿𝐹))
4039, 16eleqtrrd 2893 . 2 (𝜑𝑌𝐴)
41 eqid 2798 . . . . 5 (pInvG‘𝐺) = (pInvG‘𝐺)
425adantr 484 . . . . 5 ((𝜑𝑌 = 𝑋) → 𝐺 ∈ TarskiG)
4310adantr 484 . . . . 5 ((𝜑𝑌 = 𝑋) → 𝐸𝑃)
4413adantr 484 . . . . 5 ((𝜑𝑌 = 𝑋) → 𝑌𝑃)
4512adantr 484 . . . . 5 ((𝜑𝑌 = 𝑋) → 𝑅𝑃)
466adantr 484 . . . . . . 7 ((𝜑𝑌 = 𝑋) → 𝐶𝑃)
47 eqidd 2799 . . . . . . . . 9 ((𝜑𝑌 = 𝑋) → 𝐶 = 𝐶)
48 simpr 488 . . . . . . . . 9 ((𝜑𝑌 = 𝑋) → 𝑌 = 𝑋)
49 eqidd 2799 . . . . . . . . 9 ((𝜑𝑌 = 𝑋) → 𝐸 = 𝐸)
5047, 48, 49s3eqd 14224 . . . . . . . 8 ((𝜑𝑌 = 𝑋) → ⟨“𝐶𝑌𝐸”⟩ = ⟨“𝐶𝑋𝐸”⟩)
517adantr 484 . . . . . . . . 9 ((𝜑𝑌 = 𝑋) → 𝑋𝑃)
5214adantr 484 . . . . . . . . . 10 ((𝜑𝑌 = 𝑋) → 𝑍𝑃)
53 eqid 2798 . . . . . . . . . . . . . . . 16 ((pInvG‘𝐺)‘𝑍) = ((pInvG‘𝐺)‘𝑍)
541, 2, 3, 4, 41, 5, 14, 53, 23mircl 26469 . . . . . . . . . . . . . . 15 (𝜑 → (((pInvG‘𝐺)‘𝑍)‘𝑄) ∈ 𝑃)
551, 2, 3, 5, 10, 13, 10, 6, 19tgcgrcomlr 26288 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑌 𝐸) = (𝐶 𝐸))
5625, 55eqtr2d 2834 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐶 𝐸) = (𝑌 𝑄))
571, 3, 4, 5, 10, 11, 17tglinerflx1 26441 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐸 ∈ (𝐸𝐿𝐹))
5857, 16eleqtrrd 2893 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐸𝐴)
59 nelne2 3084 . . . . . . . . . . . . . . . . . . 19 ((𝐸𝐴 ∧ ¬ 𝐶𝐴) → 𝐸𝐶)
6058, 9, 59syl2anc 587 . . . . . . . . . . . . . . . . . 18 (𝜑𝐸𝐶)
6160necomd 3042 . . . . . . . . . . . . . . . . 17 (𝜑𝐶𝐸)
621, 2, 3, 5, 6, 10, 13, 23, 56, 61tgcgrneq 26291 . . . . . . . . . . . . . . . 16 (𝜑𝑌𝑄)
6362necomd 3042 . . . . . . . . . . . . . . 15 (𝜑𝑄𝑌)
64 nelne2 3084 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌𝐴 ∧ ¬ 𝐶𝐴) → 𝑌𝐶)
6540, 9, 64syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑌𝐶)
6665necomd 3042 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐶𝑌)
6720, 66eqnetrrd 3055 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((pInvG‘𝐺)‘𝑅)‘𝑌) ≠ 𝑌)
68 eqid 2798 . . . . . . . . . . . . . . . . . . . 20 ((pInvG‘𝐺)‘𝑅) = ((pInvG‘𝐺)‘𝑅)
691, 2, 3, 4, 41, 5, 12, 68, 13mirinv 26474 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((pInvG‘𝐺)‘𝑅)‘𝑌) = 𝑌𝑅 = 𝑌))
7069necon3bid 3031 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((pInvG‘𝐺)‘𝑅)‘𝑌) ≠ 𝑌𝑅𝑌))
7167, 70mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑𝑅𝑌)
721, 2, 3, 4, 41, 5, 12, 68, 13mirbtwn 26466 . . . . . . . . . . . . . . . . . 18 (𝜑𝑅 ∈ ((((pInvG‘𝐺)‘𝑅)‘𝑌)𝐼𝑌))
7320oveq1d 7155 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐶𝐼𝑌) = ((((pInvG‘𝐺)‘𝑅)‘𝑌)𝐼𝑌))
7472, 73eleqtrrd 2893 . . . . . . . . . . . . . . . . 17 (𝜑𝑅 ∈ (𝐶𝐼𝑌))
751, 2, 3, 5, 6, 12, 13, 23, 71, 74, 24tgbtwnouttr2 26303 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ (𝐶𝐼𝑄))
761, 2, 3, 5, 6, 13, 23, 75tgbtwncom 26296 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ (𝑄𝐼𝐶))
77 eqid 2798 . . . . . . . . . . . . . . . . . . 19 (cgrG‘𝐺) = (cgrG‘𝐺)
7820oveq2d 7156 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸 𝐶) = (𝐸 (((pInvG‘𝐺)‘𝑅)‘𝑌)))
7919, 78eqtrd 2833 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸 𝑌) = (𝐸 (((pInvG‘𝐺)‘𝑅)‘𝑌)))
801, 2, 3, 4, 41, 5, 10, 12, 13israg 26505 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (⟨“𝐸𝑅𝑌”⟩ ∈ (∟G‘𝐺) ↔ (𝐸 𝑌) = (𝐸 (((pInvG‘𝐺)‘𝑅)‘𝑌))))
8179, 80mpbird 260 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ⟨“𝐸𝑅𝑌”⟩ ∈ (∟G‘𝐺))
821, 2, 3, 5, 12, 13, 23, 24tgbtwncom 26296 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑌 ∈ (𝑄𝐼𝑅))
831, 2, 3, 5, 13, 23, 13, 10, 25tgcgrcomlr 26288 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑄 𝑌) = (𝐸 𝑌))
8422eqcomd 2804 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑌 𝑅) = (𝑌 𝑍))
851, 2, 3, 5, 23, 10axtgcgrrflx 26270 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑄 𝐸) = (𝐸 𝑄))
8625eqcomd 2804 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑌 𝐸) = (𝑌 𝑄))
871, 2, 3, 5, 23, 13, 12, 10, 13, 14, 10, 23, 63, 82, 21, 83, 84, 85, 86axtg5seg 26273 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑅 𝐸) = (𝑍 𝑄))
881, 2, 3, 5, 12, 10, 14, 23, 87tgcgrcomlr 26288 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸 𝑅) = (𝑄 𝑍))
891, 2, 3, 5, 13, 12, 13, 14, 84tgcgrcomlr 26288 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑅 𝑌) = (𝑍 𝑌))
901, 2, 77, 5, 10, 12, 13, 23, 14, 13, 88, 89, 86trgcgr 26324 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ⟨“𝐸𝑅𝑌”⟩(cgrG‘𝐺)⟨“𝑄𝑍𝑌”⟩)
911, 2, 3, 4, 41, 5, 10, 12, 13, 77, 23, 14, 13, 81, 90ragcgr 26515 . . . . . . . . . . . . . . . . . 18 (𝜑 → ⟨“𝑄𝑍𝑌”⟩ ∈ (∟G‘𝐺))
921, 2, 3, 4, 41, 5, 23, 14, 13, 91ragcom 26506 . . . . . . . . . . . . . . . . 17 (𝜑 → ⟨“𝑌𝑍𝑄”⟩ ∈ (∟G‘𝐺))
931, 2, 3, 4, 41, 5, 13, 14, 23israg 26505 . . . . . . . . . . . . . . . . 17 (𝜑 → (⟨“𝑌𝑍𝑄”⟩ ∈ (∟G‘𝐺) ↔ (𝑌 𝑄) = (𝑌 (((pInvG‘𝐺)‘𝑍)‘𝑄))))
9492, 93mpbid 235 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 𝑄) = (𝑌 (((pInvG‘𝐺)‘𝑍)‘𝑄)))
951, 2, 3, 5, 13, 23, 13, 54, 94tgcgrcomlr 26288 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄 𝑌) = ((((pInvG‘𝐺)‘𝑍)‘𝑄) 𝑌))
9627eqcomd 2804 . . . . . . . . . . . . . . 15 (𝜑 → (𝑌 𝐶) = (𝑌 𝐷))
971, 2, 3, 4, 41, 5, 14, 53, 23mircgr 26465 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑍 (((pInvG‘𝐺)‘𝑍)‘𝑄)) = (𝑍 𝑄))
9897eqcomd 2804 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍 𝑄) = (𝑍 (((pInvG‘𝐺)‘𝑍)‘𝑄)))
991, 2, 3, 5, 14, 23, 14, 54, 98tgcgrcomlr 26288 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄 𝑍) = ((((pInvG‘𝐺)‘𝑍)‘𝑄) 𝑍))
100 eqidd 2799 . . . . . . . . . . . . . . 15 (𝜑 → (𝑌 𝑍) = (𝑌 𝑍))
1011, 2, 3, 5, 23, 13, 6, 54, 13, 15, 14, 14, 63, 76, 26, 95, 96, 99, 100axtg5seg 26273 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 𝑍) = (𝐷 𝑍))
1021, 2, 3, 5, 6, 14, 15, 14, 101tgcgrcomlr 26288 . . . . . . . . . . . . 13 (𝜑 → (𝑍 𝐶) = (𝑍 𝐷))
10328oveq2d 7156 . . . . . . . . . . . . 13 (𝜑 → (𝑍 𝐷) = (𝑍 (((pInvG‘𝐺)‘𝑋)‘𝐶)))
104102, 103eqtrd 2833 . . . . . . . . . . . 12 (𝜑 → (𝑍 𝐶) = (𝑍 (((pInvG‘𝐺)‘𝑋)‘𝐶)))
1051, 2, 3, 4, 41, 5, 14, 7, 6israg 26505 . . . . . . . . . . . 12 (𝜑 → (⟨“𝑍𝑋𝐶”⟩ ∈ (∟G‘𝐺) ↔ (𝑍 𝐶) = (𝑍 (((pInvG‘𝐺)‘𝑋)‘𝐶))))
106104, 105mpbird 260 . . . . . . . . . . 11 (𝜑 → ⟨“𝑍𝑋𝐶”⟩ ∈ (∟G‘𝐺))
107106adantr 484 . . . . . . . . . 10 ((𝜑𝑌 = 𝑋) → ⟨“𝑍𝑋𝐶”⟩ ∈ (∟G‘𝐺))
10871necomd 3042 . . . . . . . . . . . . . 14 (𝜑𝑌𝑅)
1091, 2, 3, 5, 13, 12, 13, 14, 84, 108tgcgrneq 26291 . . . . . . . . . . . . 13 (𝜑𝑌𝑍)
110109necomd 3042 . . . . . . . . . . . 12 (𝜑𝑍𝑌)
111110adantr 484 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑋) → 𝑍𝑌)
112111, 48neeqtrd 3056 . . . . . . . . . 10 ((𝜑𝑌 = 𝑋) → 𝑍𝑋)
11319eqcomd 2804 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 𝐶) = (𝐸 𝑌))
114113adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑌 = 𝑋) → (𝐸 𝐶) = (𝐸 𝑌))
11560adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑌 = 𝑋) → 𝐸𝐶)
1161, 2, 3, 42, 43, 46, 43, 44, 114, 115tgcgrneq 26291 . . . . . . . . . . . . . 14 ((𝜑𝑌 = 𝑋) → 𝐸𝑌)
117116necomd 3042 . . . . . . . . . . . . 13 ((𝜑𝑌 = 𝑋) → 𝑌𝐸)
1181, 2, 3, 5, 10, 6, 10, 13, 113, 60tgcgrneq 26291 . . . . . . . . . . . . . . 15 (𝜑𝐸𝑌)
1191, 3, 4, 5, 10, 13, 14, 118, 21btwnlng3 26429 . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ (𝐸𝐿𝑌))
120119adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑌 = 𝑋) → 𝑍 ∈ (𝐸𝐿𝑌))
1211, 3, 4, 42, 44, 43, 52, 117, 120lncom 26430 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑋) → 𝑍 ∈ (𝑌𝐿𝐸))
12248oveq1d 7155 . . . . . . . . . . . 12 ((𝜑𝑌 = 𝑋) → (𝑌𝐿𝐸) = (𝑋𝐿𝐸))
123121, 122eleqtrd 2892 . . . . . . . . . . 11 ((𝜑𝑌 = 𝑋) → 𝑍 ∈ (𝑋𝐿𝐸))
124123orcd 870 . . . . . . . . . 10 ((𝜑𝑌 = 𝑋) → (𝑍 ∈ (𝑋𝐿𝐸) ∨ 𝑋 = 𝐸))
1251, 2, 3, 4, 41, 42, 52, 51, 46, 43, 107, 112, 124ragcol 26507 . . . . . . . . 9 ((𝜑𝑌 = 𝑋) → ⟨“𝐸𝑋𝐶”⟩ ∈ (∟G‘𝐺))
1261, 2, 3, 4, 41, 42, 43, 51, 46, 125ragcom 26506 . . . . . . . 8 ((𝜑𝑌 = 𝑋) → ⟨“𝐶𝑋𝐸”⟩ ∈ (∟G‘𝐺))
12750, 126eqeltrd 2890 . . . . . . 7 ((𝜑𝑌 = 𝑋) → ⟨“𝐶𝑌𝐸”⟩ ∈ (∟G‘𝐺))
12866adantr 484 . . . . . . 7 ((𝜑𝑌 = 𝑋) → 𝐶𝑌)
1291, 2, 3, 5, 6, 12, 13, 74tgbtwncom 26296 . . . . . . . . 9 (𝜑𝑅 ∈ (𝑌𝐼𝐶))
1301, 4, 3, 5, 13, 12, 6, 129btwncolg3 26365 . . . . . . . 8 (𝜑 → (𝐶 ∈ (𝑌𝐿𝑅) ∨ 𝑌 = 𝑅))
131130adantr 484 . . . . . . 7 ((𝜑𝑌 = 𝑋) → (𝐶 ∈ (𝑌𝐿𝑅) ∨ 𝑌 = 𝑅))
1321, 2, 3, 4, 41, 42, 46, 44, 43, 45, 127, 128, 131ragcol 26507 . . . . . 6 ((𝜑𝑌 = 𝑋) → ⟨“𝑅𝑌𝐸”⟩ ∈ (∟G‘𝐺))
1331, 2, 3, 4, 41, 42, 45, 44, 43, 132ragcom 26506 . . . . 5 ((𝜑𝑌 = 𝑋) → ⟨“𝐸𝑌𝑅”⟩ ∈ (∟G‘𝐺))
13481adantr 484 . . . . 5 ((𝜑𝑌 = 𝑋) → ⟨“𝐸𝑅𝑌”⟩ ∈ (∟G‘𝐺))
1351, 2, 3, 4, 41, 42, 43, 44, 45, 133, 134ragflat 26512 . . . 4 ((𝜑𝑌 = 𝑋) → 𝑌 = 𝑅)
136108adantr 484 . . . . 5 ((𝜑𝑌 = 𝑋) → 𝑌𝑅)
137136neneqd 2992 . . . 4 ((𝜑𝑌 = 𝑋) → ¬ 𝑌 = 𝑅)
138135, 137pm2.65da 816 . . 3 (𝜑 → ¬ 𝑌 = 𝑋)
139138neqned 2994 . 2 (𝜑𝑌𝑋)
14028oveq2d 7156 . . . . 5 (𝜑 → (𝑌 𝐷) = (𝑌 (((pInvG‘𝐺)‘𝑋)‘𝐶)))
14196, 140eqtrd 2833 . . . 4 (𝜑 → (𝑌 𝐶) = (𝑌 (((pInvG‘𝐺)‘𝑋)‘𝐶)))
1421, 2, 3, 4, 41, 5, 13, 7, 6israg 26505 . . . 4 (𝜑 → (⟨“𝑌𝑋𝐶”⟩ ∈ (∟G‘𝐺) ↔ (𝑌 𝐶) = (𝑌 (((pInvG‘𝐺)‘𝑋)‘𝐶))))
143141, 142mpbird 260 . . 3 (𝜑 → ⟨“𝑌𝑋𝐶”⟩ ∈ (∟G‘𝐺))
1441, 2, 3, 4, 41, 5, 13, 7, 6, 143ragcom 26506 . 2 (𝜑 → ⟨“𝐶𝑋𝑌”⟩ ∈ (∟G‘𝐺))
1451, 2, 3, 4, 5, 33, 8, 35, 36, 40, 32, 139, 144ragperp 26525 1 (𝜑 → (𝐶𝐿𝑋)(⟂G‘𝐺)𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ≠ wne 2987   class class class wbr 5031  ran crn 5521  ‘cfv 6327  (class class class)co 7140  ⟨“cs3 14202  Basecbs 16482  distcds 16573  TarskiGcstrkg 26238  Itvcitv 26244  LineGclng 26245  cgrGccgrg 26318  pInvGcmir 26460  ∟Gcrag 26501  ⟂Gcperpg 26503 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7448  ax-cnex 10589  ax-resscn 10590  ax-1cn 10591  ax-icn 10592  ax-addcl 10593  ax-addrcl 10594  ax-mulcl 10595  ax-mulrcl 10596  ax-mulcom 10597  ax-addass 10598  ax-mulass 10599  ax-distr 10600  ax-i2m1 10601  ax-1ne0 10602  ax-1rid 10603  ax-rnegex 10604  ax-rrecex 10605  ax-cnre 10606  ax-pre-lttri 10607  ax-pre-lttrn 10608  ax-pre-ltadd 10609  ax-pre-mulgt0 10610 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6286  df-fun 6329  df-fn 6330  df-f 6331  df-f1 6332  df-fo 6333  df-f1o 6334  df-fv 6335  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7568  df-1st 7678  df-2nd 7679  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-oadd 8096  df-er 8279  df-map 8398  df-pm 8399  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-dju 9321  df-card 9359  df-pnf 10673  df-mnf 10674  df-xr 10675  df-ltxr 10676  df-le 10677  df-sub 10868  df-neg 10869  df-nn 11633  df-2 11695  df-3 11696  df-n0 11893  df-xnn0 11963  df-z 11977  df-uz 12239  df-fz 12893  df-fzo 13036  df-hash 13694  df-word 13865  df-concat 13921  df-s1 13948  df-s2 14208  df-s3 14209  df-trkgc 26256  df-trkgb 26257  df-trkgcb 26258  df-trkg 26261  df-cgrg 26319  df-leg 26391  df-mir 26461  df-rag 26502  df-perpg 26504 This theorem is referenced by:  footex  26529
 Copyright terms: Public domain W3C validator