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

Theorem opphllem 25747
Description: Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 25748 and later for opphl 25766. (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 472 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐺 ∈ TarskiG)
8 eqid 2724 . . . 4 (𝑆𝑥) = (𝑆𝑥)
9 mideu.2 . . . . 5 (𝜑𝐵𝑃)
109adantr 472 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐵𝑃)
11 mideulem.3 . . . . 5 (𝜑𝑂𝑃)
1211adantr 472 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑂𝑃)
13 mideu.1 . . . . 5 (𝜑𝐴𝑃)
1413adantr 472 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐴𝑃)
15 opphllem.1 . . . . 5 (𝜑𝑅𝑃)
1615adantr 472 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑅𝑃)
17 simprl 811 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥𝑃)
18 mideulem.1 . . . . . . . . . . . . . 14 (𝜑𝐴𝐵)
1918necomd 2951 . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
2019neneqd 2901 . . . . . . . . . . . 12 (𝜑 → ¬ 𝐵 = 𝐴)
2120adantr 472 . . . . . . . . . . 11 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝐵 = 𝐴)
22 mideulem.6 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
234, 6, 22perpln2 25726 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐿𝑂) ∈ ran 𝐿)
241, 3, 4, 6, 13, 11, 23tglnne 25643 . . . . . . . . . . . . . 14 (𝜑𝐴𝑂)
2524necomd 2951 . . . . . . . . . . . . 13 (𝜑𝑂𝐴)
2625neneqd 2901 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑂 = 𝐴)
2726adantr 472 . . . . . . . . . . 11 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝑂 = 𝐴)
2821, 27jca 555 . . . . . . . . . 10 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
296adantr 472 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝐺 ∈ TarskiG)
309adantr 472 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝐵𝑃)
3113adantr 472 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝐴𝑃)
3211adantr 472 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝑂𝑃)
331, 3, 4, 6, 9, 13, 19tglinerflx2 25649 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ (𝐵𝐿𝐴))
341, 3, 4, 6, 13, 9, 18tglinecom 25650 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
3534, 22eqbrtrrd 4784 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝑂))
361, 2, 3, 4, 6, 9, 13, 33, 11, 35perprag 25738 . . . . . . . . . . . . 13 (𝜑 → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
3736adantr 472 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
38 simpr 479 . . . . . . . . . . . . 13 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝑂 ∈ (𝐵𝐿𝐴))
3938orcd 406 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → (𝑂 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
401, 2, 3, 4, 5, 29, 30, 31, 32, 37, 39ragflat3 25721 . . . . . . . . . . 11 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → (𝐵 = 𝐴𝑂 = 𝐴))
41 oran 518 . . . . . . . . . . 11 ((𝐵 = 𝐴𝑂 = 𝐴) ↔ ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
4240, 41sylib 208 . . . . . . . . . 10 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
4328, 42pm2.65da 601 . . . . . . . . 9 (𝜑 → ¬ 𝑂 ∈ (𝐵𝐿𝐴))
4443adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝑂 ∈ (𝐵𝐿𝐴))
4534adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
4644, 45neleqtrrd 2825 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
4718adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐴𝐵)
4847neneqd 2901 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝐴 = 𝐵)
4946, 48jca 555 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (¬ 𝑂 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
50 pm4.56 517 . . . . . 6 ((¬ 𝑂 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵) ↔ ¬ (𝑂 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
5149, 50sylib 208 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ (𝑂 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
521, 4, 3, 7, 14, 10, 12, 51ncolrot2 25578 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ (𝐵 ∈ (𝑂𝐿𝐴) ∨ 𝑂 = 𝐴))
53 simprrr 824 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝑅𝐼𝑂))
541, 2, 3, 7, 16, 17, 12, 53tgbtwncom 25503 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝑂𝐼𝑅))
55 mideulem.4 . . . . . . . 8 (𝜑𝑇𝑃)
5655adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑇𝑃)
57 mideulem.7 . . . . . . . 8 (𝜑𝑇 ∈ (𝐴𝐿𝐵))
5857adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑇 ∈ (𝐴𝐿𝐵))
59 simprrl 823 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝑇𝐼𝐵))
601, 3, 4, 7, 56, 14, 10, 17, 58, 59coltr3 25663 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝐴𝐿𝐵))
6143, 34neleqtrrd 2825 . . . . . . 7 (𝜑 → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
6261adantr 472 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
63 nelne2 2993 . . . . . 6 ((𝑥 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑂 ∈ (𝐴𝐿𝐵)) → 𝑥𝑂)
6460, 62, 63syl2anc 696 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥𝑂)
651, 2, 3, 7, 12, 17, 16, 54, 64tgbtwnne 25505 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑂𝑅)
661, 2, 3, 4, 5, 6, 9, 13, 11israg 25712 . . . . . . . 8 (𝜑 → (⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺) ↔ (𝐵 𝑂) = (𝐵 ((𝑆𝐴)‘𝑂))))
6736, 66mpbid 222 . . . . . . 7 (𝜑 → (𝐵 𝑂) = (𝐵 ((𝑆𝐴)‘𝑂)))
6867ad3antrrr 768 . . . . . 6 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 𝑂) = (𝐵 ((𝑆𝐴)‘𝑂)))
696ad3antrrr 768 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐺 ∈ TarskiG)
70 eqid 2724 . . . . . . . . 9 (𝑆𝐴) = (𝑆𝐴)
711, 2, 3, 4, 5, 7, 14, 70, 12mircl 25676 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ((𝑆𝐴)‘𝑂) ∈ 𝑃)
7271ad2antrr 764 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ((𝑆𝐴)‘𝑂) ∈ 𝑃)
7313ad3antrrr 768 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐴𝑃)
7411ad3antrrr 768 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑂𝑃)
7515ad3antrrr 768 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑅𝑃)
769ad3antrrr 768 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵𝑃)
77 simplr 809 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑠𝑃)
781, 2, 3, 4, 5, 69, 73, 70, 74mirbtwn 25673 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐴 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑂))
79 eqid 2724 . . . . . . . . 9 (𝑆𝐵) = (𝑆𝐵)
801, 2, 3, 4, 5, 69, 76, 79, 77mirbtwn 25673 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵 ∈ (((𝑆𝐵)‘𝑠)𝐼𝑠))
81 simpr 479 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅 = ((𝑆𝑚)‘𝑠))
8269ad2antrr 764 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐺 ∈ TarskiG)
8373ad2antrr 764 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐴𝑃)
8476ad2antrr 764 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐵𝑃)
8547ad4antr 771 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐴𝐵)
86 mideulem.2 . . . . . . . . . . . . . . . 16 (𝜑𝑄𝑃)
8786ad5antr 775 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑄𝑃)
8874ad2antrr 764 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑂𝑃)
8956ad4antr 771 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑇𝑃)
90 mideulem.5 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
9190ad5antr 775 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
9222ad5antr 775 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
9358ad4antr 771 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑇 ∈ (𝐴𝐿𝐵))
94 mideulem.8 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ (𝑄𝐼𝑂))
9594ad5antr 775 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑇 ∈ (𝑄𝐼𝑂))
9675ad2antrr 764 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅𝑃)
97 opphllem.2 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ (𝐵𝐼𝑄))
9897ad5antr 775 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅 ∈ (𝐵𝐼𝑄))
99 opphllem.3 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 𝑂) = (𝐵 𝑅))
10099ad5antr 775 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝐴 𝑂) = (𝐵 𝑅))
10117ad2antrr 764 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥𝑃)
102101ad2antrr 764 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥𝑃)
103 simp-5r 831 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂))))
104103simprd 482 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))
105104simpld 477 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥 ∈ (𝑇𝐼𝐵))
106104simprd 482 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥 ∈ (𝑅𝐼𝑂))
10777ad2antrr 764 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑠𝑃)
108 simpllr 817 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅)))
109108simpld 477 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠))
110 simprr 813 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 𝑠) = (𝑥 𝑅))
111110ad2antrr 764 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥 𝑠) = (𝑥 𝑅))
112 simplr 809 . . . . . . . . . . . . . . 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 25746 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐵 = 𝑚)
114113eqcomd 2730 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑚 = 𝐵)
115114fveq2d 6308 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑆𝑚) = (𝑆𝐵))
116115fveq1d 6306 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → ((𝑆𝑚)‘𝑠) = ((𝑆𝐵)‘𝑠))
11781, 116eqtrd 2758 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅 = ((𝑆𝐵)‘𝑠))
118 eqid 2724 . . . . . . . . . . 11 (𝑆𝑚) = (𝑆𝑚)
1191, 2, 3, 4, 5, 69, 118, 77, 75, 101, 110midexlem 25707 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ∃𝑚𝑃 𝑅 = ((𝑆𝑚)‘𝑠))
120117, 119r19.29a 3180 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑅 = ((𝑆𝐵)‘𝑠))
121120oveq1d 6780 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑅𝐼𝑠) = (((𝑆𝐵)‘𝑠)𝐼𝑠))
12280, 121eleqtrrd 2806 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵 ∈ (𝑅𝐼𝑠))
1231, 2, 3, 4, 5, 69, 73, 70, 74mircgr 25672 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 ((𝑆𝐴)‘𝑂)) = (𝐴 𝑂))
12499ad3antrrr 768 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 𝑂) = (𝐵 𝑅))
125123, 124eqtrd 2758 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 ((𝑆𝐴)‘𝑂)) = (𝐵 𝑅))
1261, 2, 3, 69, 73, 72, 76, 75, 125tgcgrcomlr 25495 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (((𝑆𝐴)‘𝑂) 𝐴) = (𝑅 𝐵))
127120oveq2d 6781 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 𝑅) = (𝐵 ((𝑆𝐵)‘𝑠)))
1281, 2, 3, 4, 5, 69, 76, 79, 77mircgr 25672 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 ((𝑆𝐵)‘𝑠)) = (𝐵 𝑠))
129124, 127, 1283eqtrd 2762 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 𝑂) = (𝐵 𝑠))
1301, 2, 3, 69, 72, 73, 74, 75, 76, 77, 78, 122, 126, 129tgcgrextend 25500 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (((𝑆𝐴)‘𝑂) 𝑂) = (𝑅 𝑠))
1311, 2, 3, 69, 72, 75axtgcgrrflx 25481 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (((𝑆𝐴)‘𝑂) 𝑅) = (𝑅 ((𝑆𝐴)‘𝑂)))
1321, 2, 3, 69, 74, 75axtgcgrrflx 25481 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑂 𝑅) = (𝑅 𝑂))
13353ad2antrr 764 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (𝑅𝐼𝑂))
134 simprl 811 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠))
1351, 2, 3, 69, 72, 101, 77, 134tgbtwncom 25503 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (𝑠𝐼((𝑆𝐴)‘𝑂)))
1361, 2, 3, 69, 101, 77, 101, 75, 110tgcgrcomlr 25495 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑠 𝑥) = (𝑅 𝑥))
137136eqcomd 2730 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑅 𝑥) = (𝑠 𝑥))
13836ad3antrrr 768 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
13947necomd 2951 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐵𝐴)
140139ad2antrr 764 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵𝐴)
14160ad2antrr 764 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (𝐴𝐿𝐵))
142141orcd 406 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
1431, 4, 3, 69, 73, 76, 101, 142colcom 25573 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
1441, 4, 3, 69, 76, 73, 101, 143colrot1 25574 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
1451, 2, 3, 4, 5, 69, 76, 73, 74, 101, 138, 140, 144ragcol 25714 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ⟨“𝑥𝐴𝑂”⟩ ∈ (∟G‘𝐺))
1461, 2, 3, 4, 5, 69, 101, 73, 74israg 25712 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (⟨“𝑥𝐴𝑂”⟩ ∈ (∟G‘𝐺) ↔ (𝑥 𝑂) = (𝑥 ((𝑆𝐴)‘𝑂))))
147145, 146mpbid 222 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 𝑂) = (𝑥 ((𝑆𝐴)‘𝑂)))
1481, 2, 3, 69, 75, 101, 74, 77, 101, 72, 133, 135, 137, 147tgcgrextend 25500 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑅 𝑂) = (𝑠 ((𝑆𝐴)‘𝑂)))
149132, 148eqtrd 2758 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑂 𝑅) = (𝑠 ((𝑆𝐴)‘𝑂)))
1501, 2, 3, 69, 72, 73, 74, 75, 75, 76, 77, 72, 78, 122, 130, 129, 131, 149tgifscgr 25523 . . . . . 6 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 𝑅) = (𝐵 ((𝑆𝐴)‘𝑂)))
15168, 150eqtr4d 2761 . . . . 5 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 𝑂) = (𝐴 𝑅))
1521, 2, 3, 7, 71, 17, 17, 16axtgsegcon 25483 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ∃𝑠𝑃 (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅)))
153151, 152r19.29a 3180 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐵 𝑂) = (𝐴 𝑅))
15499adantr 472 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐴 𝑂) = (𝐵 𝑅))
1551, 2, 3, 7, 14, 12, 10, 16, 154tgcgrcomlr 25495 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑂 𝐴) = (𝑅 𝐵))
156143, 152r19.29a 3180 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
1571, 4, 3, 7, 12, 16, 17, 54btwncolg1 25570 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 ∈ (𝑂𝐿𝑅) ∨ 𝑂 = 𝑅))
1581, 2, 3, 4, 5, 7, 8, 10, 12, 14, 16, 17, 52, 65, 153, 155, 156, 157symquadlem 25704 . . 3 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐵 = ((𝑆𝑥)‘𝐴))
1591, 2, 3, 4, 5, 7, 17, 8, 14mirbtwn 25673 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (((𝑆𝑥)‘𝐴)𝐼𝐴))
160158oveq1d 6780 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐵𝐼𝐴) = (((𝑆𝑥)‘𝐴)𝐼𝐴))
161159, 160eleqtrrd 2806 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝐵𝐼𝐴))
1621, 2, 3, 7, 10, 17, 14, 161tgbtwncom 25503 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝐴𝐼𝐵))
1631, 2, 3, 7, 14, 10axtgcgrrflx 25481 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐴 𝐵) = (𝐵 𝐴))
164158oveq2d 6781 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 𝐵) = (𝑥 ((𝑆𝑥)‘𝐴)))
1651, 2, 3, 4, 5, 7, 17, 8, 14mircgr 25672 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 ((𝑆𝑥)‘𝐴)) = (𝑥 𝐴))
166164, 165eqtrd 2758 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 𝐵) = (𝑥 𝐴))
1671, 2, 3, 7, 14, 17, 10, 12, 10, 17, 14, 16, 162, 161, 163, 166, 154, 153tgifscgr 25523 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 𝑂) = (𝑥 𝑅))
1681, 2, 3, 4, 5, 7, 17, 8, 16, 12, 167, 54ismir 25674 . . 3 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑂 = ((𝑆𝑥)‘𝑅))
169158, 168jca 555 . 2 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐵 = ((𝑆𝑥)‘𝐴) ∧ 𝑂 = ((𝑆𝑥)‘𝑅)))
1701, 2, 3, 6, 86, 55, 11, 94tgbtwncom 25503 . . 3 (𝜑𝑇 ∈ (𝑂𝐼𝑄))
1711, 2, 3, 6, 11, 9, 86, 55, 15, 170, 97axtgpasch 25486 . 2 (𝜑 → ∃𝑥𝑃 (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))
172169, 171reximddv 3120 1 (𝜑 → ∃𝑥𝑃 (𝐵 = ((𝑆𝑥)‘𝐴) ∧ 𝑂 = ((𝑆𝑥)‘𝑅)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383   = wceq 1596  wcel 2103  wne 2896  wrex 3015   class class class wbr 4760  cfv 6001  (class class class)co 6765  ⟨“cs3 13708  Basecbs 15980  distcds 16073  TarskiGcstrkg 25449  Itvcitv 25455  LineGclng 25456  pInvGcmir 25667  ∟Gcrag 25708  ⟂Gcperpg 25710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-oadd 7684  df-er 7862  df-map 7976  df-pm 7977  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-card 8878  df-cda 9103  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-nn 11134  df-2 11192  df-3 11193  df-n0 11406  df-xnn0 11477  df-z 11491  df-uz 11801  df-fz 12441  df-fzo 12581  df-hash 13233  df-word 13406  df-concat 13408  df-s1 13409  df-s2 13714  df-s3 13715  df-trkgc 25467  df-trkgb 25468  df-trkgcb 25469  df-trkg 25472  df-cgrg 25526  df-leg 25598  df-mir 25668  df-rag 25709  df-perpg 25711
This theorem is referenced by:  mideulem  25748  opphllem3  25761
  Copyright terms: Public domain W3C validator