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

Theorem opphllem 26045
Description: Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 26046 and later for opphl 26064. (Contributed by Thierry Arnoux, 21-Dec-2019.)
Hypotheses
Ref Expression
colperpex.p 𝑃 = (Base‘𝐺)
colperpex.d = (dist‘𝐺)
colperpex.i 𝐼 = (Itv‘𝐺)
colperpex.l 𝐿 = (LineG‘𝐺)
colperpex.g (𝜑𝐺 ∈ TarskiG)
mideu.s 𝑆 = (pInvG‘𝐺)
mideu.1 (𝜑𝐴𝑃)
mideu.2 (𝜑𝐵𝑃)
mideulem.1 (𝜑𝐴𝐵)
mideulem.2 (𝜑𝑄𝑃)
mideulem.3 (𝜑𝑂𝑃)
mideulem.4 (𝜑𝑇𝑃)
mideulem.5 (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
mideulem.6 (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
mideulem.7 (𝜑𝑇 ∈ (𝐴𝐿𝐵))
mideulem.8 (𝜑𝑇 ∈ (𝑄𝐼𝑂))
opphllem.1 (𝜑𝑅𝑃)
opphllem.2 (𝜑𝑅 ∈ (𝐵𝐼𝑄))
opphllem.3 (𝜑 → (𝐴 𝑂) = (𝐵 𝑅))
Assertion
Ref Expression
opphllem (𝜑 → ∃𝑥𝑃 (𝐵 = ((𝑆𝑥)‘𝐴) ∧ 𝑂 = ((𝑆𝑥)‘𝑅)))
Distinct variable groups:   𝑥,   𝑥,𝐴   𝑥,𝐵   𝑥,𝐼   𝑥,𝑂   𝑥,𝑃   𝑥,𝑄   𝑥,𝑅   𝑥,𝑇   𝜑,𝑥
Allowed substitution hints:   𝑆(𝑥)   𝐺(𝑥)   𝐿(𝑥)

Proof of Theorem opphllem
Dummy variables 𝑚 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 colperpex.p . . . 4 𝑃 = (Base‘𝐺)
2 colperpex.d . . . 4 = (dist‘𝐺)
3 colperpex.i . . . 4 𝐼 = (Itv‘𝐺)
4 colperpex.l . . . 4 𝐿 = (LineG‘𝐺)
5 mideu.s . . . 4 𝑆 = (pInvG‘𝐺)
6 colperpex.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
76adantr 474 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐺 ∈ TarskiG)
8 eqid 2826 . . . 4 (𝑆𝑥) = (𝑆𝑥)
9 mideu.2 . . . . 5 (𝜑𝐵𝑃)
109adantr 474 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐵𝑃)
11 mideulem.3 . . . . 5 (𝜑𝑂𝑃)
1211adantr 474 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑂𝑃)
13 mideu.1 . . . . 5 (𝜑𝐴𝑃)
1413adantr 474 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐴𝑃)
15 opphllem.1 . . . . 5 (𝜑𝑅𝑃)
1615adantr 474 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑅𝑃)
17 simprl 789 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥𝑃)
18 mideulem.1 . . . . . . . . . . . . . 14 (𝜑𝐴𝐵)
1918necomd 3055 . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
2019neneqd 3005 . . . . . . . . . . . 12 (𝜑 → ¬ 𝐵 = 𝐴)
2120adantr 474 . . . . . . . . . . 11 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝐵 = 𝐴)
22 mideulem.6 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
234, 6, 22perpln2 26024 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐿𝑂) ∈ ran 𝐿)
241, 3, 4, 6, 13, 11, 23tglnne 25941 . . . . . . . . . . . . . 14 (𝜑𝐴𝑂)
2524necomd 3055 . . . . . . . . . . . . 13 (𝜑𝑂𝐴)
2625neneqd 3005 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑂 = 𝐴)
2726adantr 474 . . . . . . . . . . 11 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝑂 = 𝐴)
2821, 27jca 509 . . . . . . . . . 10 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
296adantr 474 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝐺 ∈ TarskiG)
309adantr 474 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝐵𝑃)
3113adantr 474 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝐴𝑃)
3211adantr 474 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝑂𝑃)
331, 3, 4, 6, 9, 13, 19tglinerflx2 25947 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ (𝐵𝐿𝐴))
341, 3, 4, 6, 13, 9, 18tglinecom 25948 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
3534, 22eqbrtrrd 4898 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝑂))
361, 2, 3, 4, 6, 9, 13, 33, 11, 35perprag 26036 . . . . . . . . . . . . 13 (𝜑 → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
3736adantr 474 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
38 simpr 479 . . . . . . . . . . . . 13 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝑂 ∈ (𝐵𝐿𝐴))
3938orcd 906 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → (𝑂 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
401, 2, 3, 4, 5, 29, 30, 31, 32, 37, 39ragflat3 26019 . . . . . . . . . . 11 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → (𝐵 = 𝐴𝑂 = 𝐴))
41 oran 1019 . . . . . . . . . . 11 ((𝐵 = 𝐴𝑂 = 𝐴) ↔ ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
4240, 41sylib 210 . . . . . . . . . 10 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
4328, 42pm2.65da 853 . . . . . . . . 9 (𝜑 → ¬ 𝑂 ∈ (𝐵𝐿𝐴))
4443adantr 474 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝑂 ∈ (𝐵𝐿𝐴))
4534adantr 474 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
4644, 45neleqtrrd 2929 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
4718adantr 474 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐴𝐵)
4847neneqd 3005 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝐴 = 𝐵)
4946, 48jca 509 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (¬ 𝑂 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
50 pm4.56 1018 . . . . . 6 ((¬ 𝑂 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵) ↔ ¬ (𝑂 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
5149, 50sylib 210 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ (𝑂 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
521, 4, 3, 7, 14, 10, 12, 51ncolrot2 25876 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ (𝐵 ∈ (𝑂𝐿𝐴) ∨ 𝑂 = 𝐴))
53 simprrr 802 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝑅𝐼𝑂))
541, 2, 3, 7, 16, 17, 12, 53tgbtwncom 25801 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝑂𝐼𝑅))
55 mideulem.4 . . . . . . . 8 (𝜑𝑇𝑃)
5655adantr 474 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑇𝑃)
57 mideulem.7 . . . . . . . 8 (𝜑𝑇 ∈ (𝐴𝐿𝐵))
5857adantr 474 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑇 ∈ (𝐴𝐿𝐵))
59 simprrl 801 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝑇𝐼𝐵))
601, 3, 4, 7, 56, 14, 10, 17, 58, 59coltr3 25961 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝐴𝐿𝐵))
6143, 34neleqtrrd 2929 . . . . . . 7 (𝜑 → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
6261adantr 474 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
63 nelne2 3097 . . . . . 6 ((𝑥 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑂 ∈ (𝐴𝐿𝐵)) → 𝑥𝑂)
6460, 62, 63syl2anc 581 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥𝑂)
651, 2, 3, 7, 12, 17, 16, 54, 64tgbtwnne 25803 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑂𝑅)
661, 2, 3, 4, 5, 6, 9, 13, 11israg 26010 . . . . . . . 8 (𝜑 → (⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺) ↔ (𝐵 𝑂) = (𝐵 ((𝑆𝐴)‘𝑂))))
6736, 66mpbid 224 . . . . . . 7 (𝜑 → (𝐵 𝑂) = (𝐵 ((𝑆𝐴)‘𝑂)))
6867ad3antrrr 723 . . . . . 6 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 𝑂) = (𝐵 ((𝑆𝐴)‘𝑂)))
696ad3antrrr 723 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐺 ∈ TarskiG)
70 eqid 2826 . . . . . . . . 9 (𝑆𝐴) = (𝑆𝐴)
711, 2, 3, 4, 5, 7, 14, 70, 12mircl 25974 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ((𝑆𝐴)‘𝑂) ∈ 𝑃)
7271ad2antrr 719 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ((𝑆𝐴)‘𝑂) ∈ 𝑃)
7313ad3antrrr 723 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐴𝑃)
7411ad3antrrr 723 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑂𝑃)
7515ad3antrrr 723 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑅𝑃)
769ad3antrrr 723 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵𝑃)
77 simplr 787 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑠𝑃)
781, 2, 3, 4, 5, 69, 73, 70, 74mirbtwn 25971 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐴 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑂))
79 eqid 2826 . . . . . . . . 9 (𝑆𝐵) = (𝑆𝐵)
801, 2, 3, 4, 5, 69, 76, 79, 77mirbtwn 25971 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵 ∈ (((𝑆𝐵)‘𝑠)𝐼𝑠))
81 simpr 479 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅 = ((𝑆𝑚)‘𝑠))
8269ad2antrr 719 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐺 ∈ TarskiG)
8373ad2antrr 719 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐴𝑃)
8476ad2antrr 719 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐵𝑃)
8547ad4antr 726 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐴𝐵)
86 mideulem.2 . . . . . . . . . . . . . . . 16 (𝜑𝑄𝑃)
8786ad5antr 730 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑄𝑃)
8874ad2antrr 719 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑂𝑃)
8956ad4antr 726 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑇𝑃)
90 mideulem.5 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
9190ad5antr 730 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
9222ad5antr 730 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
9358ad4antr 726 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑇 ∈ (𝐴𝐿𝐵))
94 mideulem.8 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ (𝑄𝐼𝑂))
9594ad5antr 730 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑇 ∈ (𝑄𝐼𝑂))
9675ad2antrr 719 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅𝑃)
97 opphllem.2 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ (𝐵𝐼𝑄))
9897ad5antr 730 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅 ∈ (𝐵𝐼𝑄))
99 opphllem.3 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 𝑂) = (𝐵 𝑅))
10099ad5antr 730 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝐴 𝑂) = (𝐵 𝑅))
10117ad2antrr 719 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥𝑃)
102101ad2antrr 719 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥𝑃)
103 simp-5r 809 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂))))
104103simprd 491 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))
105104simpld 490 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥 ∈ (𝑇𝐼𝐵))
106104simprd 491 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥 ∈ (𝑅𝐼𝑂))
10777ad2antrr 719 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑠𝑃)
108 simpllr 795 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅)))
109108simpld 490 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠))
110 simprr 791 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 𝑠) = (𝑥 𝑅))
111110ad2antrr 719 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥 𝑠) = (𝑥 𝑅))
112 simplr 787 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑚𝑃)
1131, 2, 3, 4, 82, 5, 83, 84, 85, 87, 88, 89, 91, 92, 93, 95, 96, 98, 100, 102, 105, 106, 107, 109, 111, 112, 81mideulem2 26044 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐵 = 𝑚)
114113eqcomd 2832 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑚 = 𝐵)
115114fveq2d 6438 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑆𝑚) = (𝑆𝐵))
116115fveq1d 6436 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → ((𝑆𝑚)‘𝑠) = ((𝑆𝐵)‘𝑠))
11781, 116eqtrd 2862 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅 = ((𝑆𝐵)‘𝑠))
118 eqid 2826 . . . . . . . . . . 11 (𝑆𝑚) = (𝑆𝑚)
1191, 2, 3, 4, 5, 69, 118, 77, 75, 101, 110midexlem 26005 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ∃𝑚𝑃 𝑅 = ((𝑆𝑚)‘𝑠))
120117, 119r19.29a 3289 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑅 = ((𝑆𝐵)‘𝑠))
121120oveq1d 6921 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑅𝐼𝑠) = (((𝑆𝐵)‘𝑠)𝐼𝑠))
12280, 121eleqtrrd 2910 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵 ∈ (𝑅𝐼𝑠))
1231, 2, 3, 4, 5, 69, 73, 70, 74mircgr 25970 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 ((𝑆𝐴)‘𝑂)) = (𝐴 𝑂))
12499ad3antrrr 723 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 𝑂) = (𝐵 𝑅))
125123, 124eqtrd 2862 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 ((𝑆𝐴)‘𝑂)) = (𝐵 𝑅))
1261, 2, 3, 69, 73, 72, 76, 75, 125tgcgrcomlr 25793 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (((𝑆𝐴)‘𝑂) 𝐴) = (𝑅 𝐵))
127120oveq2d 6922 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 𝑅) = (𝐵 ((𝑆𝐵)‘𝑠)))
1281, 2, 3, 4, 5, 69, 76, 79, 77mircgr 25970 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 ((𝑆𝐵)‘𝑠)) = (𝐵 𝑠))
129124, 127, 1283eqtrd 2866 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 𝑂) = (𝐵 𝑠))
1301, 2, 3, 69, 72, 73, 74, 75, 76, 77, 78, 122, 126, 129tgcgrextend 25798 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (((𝑆𝐴)‘𝑂) 𝑂) = (𝑅 𝑠))
1311, 2, 3, 69, 72, 75axtgcgrrflx 25775 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (((𝑆𝐴)‘𝑂) 𝑅) = (𝑅 ((𝑆𝐴)‘𝑂)))
1321, 2, 3, 69, 74, 75axtgcgrrflx 25775 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑂 𝑅) = (𝑅 𝑂))
13353ad2antrr 719 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (𝑅𝐼𝑂))
134 simprl 789 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠))
1351, 2, 3, 69, 72, 101, 77, 134tgbtwncom 25801 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (𝑠𝐼((𝑆𝐴)‘𝑂)))
1361, 2, 3, 69, 101, 77, 101, 75, 110tgcgrcomlr 25793 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑠 𝑥) = (𝑅 𝑥))
137136eqcomd 2832 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑅 𝑥) = (𝑠 𝑥))
13836ad3antrrr 723 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
13947necomd 3055 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐵𝐴)
140139ad2antrr 719 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵𝐴)
14160ad2antrr 719 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (𝐴𝐿𝐵))
142141orcd 906 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
1431, 4, 3, 69, 73, 76, 101, 142colcom 25871 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
1441, 4, 3, 69, 76, 73, 101, 143colrot1 25872 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
1451, 2, 3, 4, 5, 69, 76, 73, 74, 101, 138, 140, 144ragcol 26012 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ⟨“𝑥𝐴𝑂”⟩ ∈ (∟G‘𝐺))
1461, 2, 3, 4, 5, 69, 101, 73, 74israg 26010 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (⟨“𝑥𝐴𝑂”⟩ ∈ (∟G‘𝐺) ↔ (𝑥 𝑂) = (𝑥 ((𝑆𝐴)‘𝑂))))
147145, 146mpbid 224 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 𝑂) = (𝑥 ((𝑆𝐴)‘𝑂)))
1481, 2, 3, 69, 75, 101, 74, 77, 101, 72, 133, 135, 137, 147tgcgrextend 25798 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑅 𝑂) = (𝑠 ((𝑆𝐴)‘𝑂)))
149132, 148eqtrd 2862 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑂 𝑅) = (𝑠 ((𝑆𝐴)‘𝑂)))
1501, 2, 3, 69, 72, 73, 74, 75, 75, 76, 77, 72, 78, 122, 130, 129, 131, 149tgifscgr 25821 . . . . . 6 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 𝑅) = (𝐵 ((𝑆𝐴)‘𝑂)))
15168, 150eqtr4d 2865 . . . . 5 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 𝑂) = (𝐴 𝑅))
1521, 2, 3, 7, 71, 17, 17, 16axtgsegcon 25777 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ∃𝑠𝑃 (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅)))
153151, 152r19.29a 3289 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐵 𝑂) = (𝐴 𝑅))
15499adantr 474 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐴 𝑂) = (𝐵 𝑅))
1551, 2, 3, 7, 14, 12, 10, 16, 154tgcgrcomlr 25793 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑂 𝐴) = (𝑅 𝐵))
156143, 152r19.29a 3289 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
1571, 4, 3, 7, 12, 16, 17, 54btwncolg1 25868 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 ∈ (𝑂𝐿𝑅) ∨ 𝑂 = 𝑅))
1581, 2, 3, 4, 5, 7, 8, 10, 12, 14, 16, 17, 52, 65, 153, 155, 156, 157symquadlem 26002 . . 3 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐵 = ((𝑆𝑥)‘𝐴))
1591, 2, 3, 4, 5, 7, 17, 8, 14mirbtwn 25971 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (((𝑆𝑥)‘𝐴)𝐼𝐴))
160158oveq1d 6921 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐵𝐼𝐴) = (((𝑆𝑥)‘𝐴)𝐼𝐴))
161159, 160eleqtrrd 2910 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝐵𝐼𝐴))
1621, 2, 3, 7, 10, 17, 14, 161tgbtwncom 25801 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝐴𝐼𝐵))
1631, 2, 3, 7, 14, 10axtgcgrrflx 25775 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐴 𝐵) = (𝐵 𝐴))
164158oveq2d 6922 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 𝐵) = (𝑥 ((𝑆𝑥)‘𝐴)))
1651, 2, 3, 4, 5, 7, 17, 8, 14mircgr 25970 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 ((𝑆𝑥)‘𝐴)) = (𝑥 𝐴))
166164, 165eqtrd 2862 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 𝐵) = (𝑥 𝐴))
1671, 2, 3, 7, 14, 17, 10, 12, 10, 17, 14, 16, 162, 161, 163, 166, 154, 153tgifscgr 25821 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 𝑂) = (𝑥 𝑅))
1681, 2, 3, 4, 5, 7, 17, 8, 16, 12, 167, 54ismir 25972 . . 3 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑂 = ((𝑆𝑥)‘𝑅))
169158, 168jca 509 . 2 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐵 = ((𝑆𝑥)‘𝐴) ∧ 𝑂 = ((𝑆𝑥)‘𝑅)))
1701, 2, 3, 6, 86, 55, 11, 94tgbtwncom 25801 . . 3 (𝜑𝑇 ∈ (𝑂𝐼𝑄))
1711, 2, 3, 6, 11, 9, 86, 55, 15, 170, 97axtgpasch 25780 . 2 (𝜑 → ∃𝑥𝑃 (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))
172169, 171reximddv 3227 1 (𝜑 → ∃𝑥𝑃 (𝐵 = ((𝑆𝑥)‘𝐴) ∧ 𝑂 = ((𝑆𝑥)‘𝑅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386  wo 880   = wceq 1658  wcel 2166  wne 3000  wrex 3119   class class class wbr 4874  cfv 6124  (class class class)co 6906  ⟨“cs3 13964  Basecbs 16223  distcds 16315  TarskiGcstrkg 25743  Itvcitv 25749  LineGclng 25750  pInvGcmir 25965  ∟Gcrag 26006  ⟂Gcperpg 26008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-cnex 10309  ax-resscn 10310  ax-1cn 10311  ax-icn 10312  ax-addcl 10313  ax-addrcl 10314  ax-mulcl 10315  ax-mulrcl 10316  ax-mulcom 10317  ax-addass 10318  ax-mulass 10319  ax-distr 10320  ax-i2m1 10321  ax-1ne0 10322  ax-1rid 10323  ax-rnegex 10324  ax-rrecex 10325  ax-cnre 10326  ax-pre-lttri 10327  ax-pre-lttrn 10328  ax-pre-ltadd 10329  ax-pre-mulgt0 10330
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-int 4699  df-iun 4743  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-om 7328  df-1st 7429  df-2nd 7430  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-1o 7827  df-oadd 7831  df-er 8010  df-map 8125  df-pm 8126  df-en 8224  df-dom 8225  df-sdom 8226  df-fin 8227  df-card 9079  df-cda 9306  df-pnf 10394  df-mnf 10395  df-xr 10396  df-ltxr 10397  df-le 10398  df-sub 10588  df-neg 10589  df-nn 11352  df-2 11415  df-3 11416  df-n0 11620  df-xnn0 11692  df-z 11706  df-uz 11970  df-fz 12621  df-fzo 12762  df-hash 13412  df-word 13576  df-concat 13632  df-s1 13657  df-s2 13970  df-s3 13971  df-trkgc 25761  df-trkgb 25762  df-trkgcb 25763  df-trkg 25766  df-cgrg 25824  df-leg 25896  df-mir 25966  df-rag 26007  df-perpg 26009
This theorem is referenced by:  mideulem  26046  opphllem3  26059
  Copyright terms: Public domain W3C validator