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

Theorem opphllem 26513
 Description: Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 26514 and later for opphl 26532. (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 483 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐺 ∈ TarskiG)
8 eqid 2819 . . . 4 (𝑆𝑥) = (𝑆𝑥)
9 mideu.2 . . . . 5 (𝜑𝐵𝑃)
109adantr 483 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐵𝑃)
11 mideulem.3 . . . . 5 (𝜑𝑂𝑃)
1211adantr 483 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑂𝑃)
13 mideu.1 . . . . 5 (𝜑𝐴𝑃)
1413adantr 483 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐴𝑃)
15 opphllem.1 . . . . 5 (𝜑𝑅𝑃)
1615adantr 483 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑅𝑃)
17 simprl 769 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥𝑃)
18 mideulem.1 . . . . . . . . . . . . . 14 (𝜑𝐴𝐵)
1918necomd 3069 . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
2019neneqd 3019 . . . . . . . . . . . 12 (𝜑 → ¬ 𝐵 = 𝐴)
2120adantr 483 . . . . . . . . . . 11 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝐵 = 𝐴)
22 mideulem.6 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
234, 6, 22perpln2 26489 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐿𝑂) ∈ ran 𝐿)
241, 3, 4, 6, 13, 11, 23tglnne 26406 . . . . . . . . . . . . . 14 (𝜑𝐴𝑂)
2524necomd 3069 . . . . . . . . . . . . 13 (𝜑𝑂𝐴)
2625neneqd 3019 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑂 = 𝐴)
2726adantr 483 . . . . . . . . . . 11 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ¬ 𝑂 = 𝐴)
2821, 27jca 514 . . . . . . . . . 10 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
296adantr 483 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝐺 ∈ TarskiG)
309adantr 483 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝐵𝑃)
3113adantr 483 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝐴𝑃)
3211adantr 483 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝑂𝑃)
331, 3, 4, 6, 9, 13, 19tglinerflx2 26412 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ (𝐵𝐿𝐴))
341, 3, 4, 6, 13, 9, 18tglinecom 26413 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
3534, 22eqbrtrrd 5081 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝐴𝐿𝑂))
361, 2, 3, 4, 6, 9, 13, 33, 11, 35perprag 26504 . . . . . . . . . . . . 13 (𝜑 → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
3736adantr 483 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
38 simpr 487 . . . . . . . . . . . . 13 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → 𝑂 ∈ (𝐵𝐿𝐴))
3938orcd 869 . . . . . . . . . . . 12 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → (𝑂 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
401, 2, 3, 4, 5, 29, 30, 31, 32, 37, 39ragflat3 26484 . . . . . . . . . . 11 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → (𝐵 = 𝐴𝑂 = 𝐴))
41 oran 986 . . . . . . . . . . 11 ((𝐵 = 𝐴𝑂 = 𝐴) ↔ ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
4240, 41sylib 220 . . . . . . . . . 10 ((𝜑𝑂 ∈ (𝐵𝐿𝐴)) → ¬ (¬ 𝐵 = 𝐴 ∧ ¬ 𝑂 = 𝐴))
4328, 42pm2.65da 815 . . . . . . . . 9 (𝜑 → ¬ 𝑂 ∈ (𝐵𝐿𝐴))
4443adantr 483 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝑂 ∈ (𝐵𝐿𝐴))
4534adantr 483 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
4644, 45neleqtrrd 2933 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
4718adantr 483 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐴𝐵)
4847neneqd 3019 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝐴 = 𝐵)
4946, 48jca 514 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (¬ 𝑂 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
50 pm4.56 985 . . . . . 6 ((¬ 𝑂 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵) ↔ ¬ (𝑂 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
5149, 50sylib 220 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ (𝑂 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
521, 4, 3, 7, 14, 10, 12, 51ncolrot2 26341 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ (𝐵 ∈ (𝑂𝐿𝐴) ∨ 𝑂 = 𝐴))
53 simprrr 780 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝑅𝐼𝑂))
541, 2, 3, 7, 16, 17, 12, 53tgbtwncom 26266 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝑂𝐼𝑅))
55 mideulem.4 . . . . . . . 8 (𝜑𝑇𝑃)
5655adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑇𝑃)
57 mideulem.7 . . . . . . . 8 (𝜑𝑇 ∈ (𝐴𝐿𝐵))
5857adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑇 ∈ (𝐴𝐿𝐵))
59 simprrl 779 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝑇𝐼𝐵))
601, 3, 4, 7, 56, 14, 10, 17, 58, 59coltr3 26426 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝐴𝐿𝐵))
6143, 34neleqtrrd 2933 . . . . . . 7 (𝜑 → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
6261adantr 483 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ¬ 𝑂 ∈ (𝐴𝐿𝐵))
63 nelne2 3113 . . . . . 6 ((𝑥 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝑂 ∈ (𝐴𝐿𝐵)) → 𝑥𝑂)
6460, 62, 63syl2anc 586 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥𝑂)
651, 2, 3, 7, 12, 17, 16, 54, 64tgbtwnne 26268 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑂𝑅)
661, 2, 3, 4, 5, 6, 9, 13, 11israg 26475 . . . . . . . 8 (𝜑 → (⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺) ↔ (𝐵 𝑂) = (𝐵 ((𝑆𝐴)‘𝑂))))
6736, 66mpbid 234 . . . . . . 7 (𝜑 → (𝐵 𝑂) = (𝐵 ((𝑆𝐴)‘𝑂)))
6867ad3antrrr 728 . . . . . 6 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 𝑂) = (𝐵 ((𝑆𝐴)‘𝑂)))
696ad3antrrr 728 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐺 ∈ TarskiG)
70 eqid 2819 . . . . . . . . 9 (𝑆𝐴) = (𝑆𝐴)
711, 2, 3, 4, 5, 7, 14, 70, 12mircl 26439 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ((𝑆𝐴)‘𝑂) ∈ 𝑃)
7271ad2antrr 724 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ((𝑆𝐴)‘𝑂) ∈ 𝑃)
7313ad3antrrr 728 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐴𝑃)
7411ad3antrrr 728 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑂𝑃)
7515ad3antrrr 728 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑅𝑃)
769ad3antrrr 728 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵𝑃)
77 simplr 767 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑠𝑃)
781, 2, 3, 4, 5, 69, 73, 70, 74mirbtwn 26436 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐴 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑂))
79 eqid 2819 . . . . . . . . 9 (𝑆𝐵) = (𝑆𝐵)
801, 2, 3, 4, 5, 69, 76, 79, 77mirbtwn 26436 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵 ∈ (((𝑆𝐵)‘𝑠)𝐼𝑠))
81 simpr 487 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅 = ((𝑆𝑚)‘𝑠))
8269ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐺 ∈ TarskiG)
8373ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐴𝑃)
8476ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐵𝑃)
8547ad4antr 730 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐴𝐵)
86 mideulem.2 . . . . . . . . . . . . . . . 16 (𝜑𝑄𝑃)
8786ad5antr 732 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑄𝑃)
8874ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑂𝑃)
8956ad4antr 730 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑇𝑃)
90 mideulem.5 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
9190ad5antr 732 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑄𝐿𝐵))
9222ad5antr 732 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐴𝐿𝑂))
9358ad4antr 730 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑇 ∈ (𝐴𝐿𝐵))
94 mideulem.8 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ (𝑄𝐼𝑂))
9594ad5antr 732 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑇 ∈ (𝑄𝐼𝑂))
9675ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅𝑃)
97 opphllem.2 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ (𝐵𝐼𝑄))
9897ad5antr 732 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅 ∈ (𝐵𝐼𝑄))
99 opphllem.3 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 𝑂) = (𝐵 𝑅))
10099ad5antr 732 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝐴 𝑂) = (𝐵 𝑅))
10117ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥𝑃)
102101ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥𝑃)
103 simp-5r 784 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂))))
104103simprd 498 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))
105104simpld 497 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥 ∈ (𝑇𝐼𝐵))
106104simprd 498 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥 ∈ (𝑅𝐼𝑂))
10777ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑠𝑃)
108 simpllr 774 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅)))
109108simpld 497 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠))
110 simprr 771 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 𝑠) = (𝑥 𝑅))
111110ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑥 𝑠) = (𝑥 𝑅))
112 simplr 767 . . . . . . . . . . . . . . 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 26512 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝐵 = 𝑚)
114113eqcomd 2825 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑚 = 𝐵)
115114fveq2d 6667 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → (𝑆𝑚) = (𝑆𝐵))
116115fveq1d 6665 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → ((𝑆𝑚)‘𝑠) = ((𝑆𝐵)‘𝑠))
11781, 116eqtrd 2854 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) ∧ 𝑚𝑃) ∧ 𝑅 = ((𝑆𝑚)‘𝑠)) → 𝑅 = ((𝑆𝐵)‘𝑠))
118 eqid 2819 . . . . . . . . . . 11 (𝑆𝑚) = (𝑆𝑚)
1191, 2, 3, 4, 5, 69, 118, 77, 75, 101, 110midexlem 26470 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ∃𝑚𝑃 𝑅 = ((𝑆𝑚)‘𝑠))
120117, 119r19.29a 3287 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑅 = ((𝑆𝐵)‘𝑠))
121120oveq1d 7163 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑅𝐼𝑠) = (((𝑆𝐵)‘𝑠)𝐼𝑠))
12280, 121eleqtrrd 2914 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵 ∈ (𝑅𝐼𝑠))
1231, 2, 3, 4, 5, 69, 73, 70, 74mircgr 26435 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 ((𝑆𝐴)‘𝑂)) = (𝐴 𝑂))
12499ad3antrrr 728 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 𝑂) = (𝐵 𝑅))
125123, 124eqtrd 2854 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 ((𝑆𝐴)‘𝑂)) = (𝐵 𝑅))
1261, 2, 3, 69, 73, 72, 76, 75, 125tgcgrcomlr 26258 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (((𝑆𝐴)‘𝑂) 𝐴) = (𝑅 𝐵))
127120oveq2d 7164 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 𝑅) = (𝐵 ((𝑆𝐵)‘𝑠)))
1281, 2, 3, 4, 5, 69, 76, 79, 77mircgr 26435 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 ((𝑆𝐵)‘𝑠)) = (𝐵 𝑠))
129124, 127, 1283eqtrd 2858 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 𝑂) = (𝐵 𝑠))
1301, 2, 3, 69, 72, 73, 74, 75, 76, 77, 78, 122, 126, 129tgcgrextend 26263 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (((𝑆𝐴)‘𝑂) 𝑂) = (𝑅 𝑠))
1311, 2, 3, 69, 72, 75axtgcgrrflx 26240 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (((𝑆𝐴)‘𝑂) 𝑅) = (𝑅 ((𝑆𝐴)‘𝑂)))
1321, 2, 3, 69, 74, 75axtgcgrrflx 26240 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑂 𝑅) = (𝑅 𝑂))
13353ad2antrr 724 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (𝑅𝐼𝑂))
134 simprl 769 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠))
1351, 2, 3, 69, 72, 101, 77, 134tgbtwncom 26266 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (𝑠𝐼((𝑆𝐴)‘𝑂)))
1361, 2, 3, 69, 101, 77, 101, 75, 110tgcgrcomlr 26258 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑠 𝑥) = (𝑅 𝑥))
137136eqcomd 2825 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑅 𝑥) = (𝑠 𝑥))
13836ad3antrrr 728 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ⟨“𝐵𝐴𝑂”⟩ ∈ (∟G‘𝐺))
13947necomd 3069 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐵𝐴)
140139ad2antrr 724 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝐵𝐴)
14160ad2antrr 724 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → 𝑥 ∈ (𝐴𝐿𝐵))
142141orcd 869 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
1431, 4, 3, 69, 73, 76, 101, 142colcom 26336 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
1441, 4, 3, 69, 76, 73, 101, 143colrot1 26337 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
1451, 2, 3, 4, 5, 69, 76, 73, 74, 101, 138, 140, 144ragcol 26477 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → ⟨“𝑥𝐴𝑂”⟩ ∈ (∟G‘𝐺))
1461, 2, 3, 4, 5, 69, 101, 73, 74israg 26475 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (⟨“𝑥𝐴𝑂”⟩ ∈ (∟G‘𝐺) ↔ (𝑥 𝑂) = (𝑥 ((𝑆𝐴)‘𝑂))))
147145, 146mpbid 234 . . . . . . . . 9 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑥 𝑂) = (𝑥 ((𝑆𝐴)‘𝑂)))
1481, 2, 3, 69, 75, 101, 74, 77, 101, 72, 133, 135, 137, 147tgcgrextend 26263 . . . . . . . 8 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑅 𝑂) = (𝑠 ((𝑆𝐴)‘𝑂)))
149132, 148eqtrd 2854 . . . . . . 7 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝑂 𝑅) = (𝑠 ((𝑆𝐴)‘𝑂)))
1501, 2, 3, 69, 72, 73, 74, 75, 75, 76, 77, 72, 78, 122, 130, 129, 131, 149tgifscgr 26286 . . . . . 6 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐴 𝑅) = (𝐵 ((𝑆𝐴)‘𝑂)))
15168, 150eqtr4d 2857 . . . . 5 ((((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) ∧ 𝑠𝑃) ∧ (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅))) → (𝐵 𝑂) = (𝐴 𝑅))
1521, 2, 3, 7, 71, 17, 17, 16axtgsegcon 26242 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → ∃𝑠𝑃 (𝑥 ∈ (((𝑆𝐴)‘𝑂)𝐼𝑠) ∧ (𝑥 𝑠) = (𝑥 𝑅)))
153151, 152r19.29a 3287 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐵 𝑂) = (𝐴 𝑅))
15499adantr 483 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐴 𝑂) = (𝐵 𝑅))
1551, 2, 3, 7, 14, 12, 10, 16, 154tgcgrcomlr 26258 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑂 𝐴) = (𝑅 𝐵))
156143, 152r19.29a 3287 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
1571, 4, 3, 7, 12, 16, 17, 54btwncolg1 26333 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 ∈ (𝑂𝐿𝑅) ∨ 𝑂 = 𝑅))
1581, 2, 3, 4, 5, 7, 8, 10, 12, 14, 16, 17, 52, 65, 153, 155, 156, 157symquadlem 26467 . . 3 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝐵 = ((𝑆𝑥)‘𝐴))
1591, 2, 3, 4, 5, 7, 17, 8, 14mirbtwn 26436 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (((𝑆𝑥)‘𝐴)𝐼𝐴))
160158oveq1d 7163 . . . . . . 7 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐵𝐼𝐴) = (((𝑆𝑥)‘𝐴)𝐼𝐴))
161159, 160eleqtrrd 2914 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝐵𝐼𝐴))
1621, 2, 3, 7, 10, 17, 14, 161tgbtwncom 26266 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑥 ∈ (𝐴𝐼𝐵))
1631, 2, 3, 7, 14, 10axtgcgrrflx 26240 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐴 𝐵) = (𝐵 𝐴))
164158oveq2d 7164 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 𝐵) = (𝑥 ((𝑆𝑥)‘𝐴)))
1651, 2, 3, 4, 5, 7, 17, 8, 14mircgr 26435 . . . . . 6 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 ((𝑆𝑥)‘𝐴)) = (𝑥 𝐴))
166164, 165eqtrd 2854 . . . . 5 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 𝐵) = (𝑥 𝐴))
1671, 2, 3, 7, 14, 17, 10, 12, 10, 17, 14, 16, 162, 161, 163, 166, 154, 153tgifscgr 26286 . . . 4 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝑥 𝑂) = (𝑥 𝑅))
1681, 2, 3, 4, 5, 7, 17, 8, 16, 12, 167, 54ismir 26437 . . 3 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → 𝑂 = ((𝑆𝑥)‘𝑅))
169158, 168jca 514 . 2 ((𝜑 ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))) → (𝐵 = ((𝑆𝑥)‘𝐴) ∧ 𝑂 = ((𝑆𝑥)‘𝑅)))
1701, 2, 3, 6, 86, 55, 11, 94tgbtwncom 26266 . . 3 (𝜑𝑇 ∈ (𝑂𝐼𝑄))
1711, 2, 3, 6, 11, 9, 86, 55, 15, 170, 97axtgpasch 26245 . 2 (𝜑 → ∃𝑥𝑃 (𝑥 ∈ (𝑇𝐼𝐵) ∧ 𝑥 ∈ (𝑅𝐼𝑂)))
172169, 171reximddv 3273 1 (𝜑 → ∃𝑥𝑃 (𝐵 = ((𝑆𝑥)‘𝐴) ∧ 𝑂 = ((𝑆𝑥)‘𝑅)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∨ wo 843   = wceq 1531   ∈ wcel 2108   ≠ wne 3014  ∃wrex 3137   class class class wbr 5057  ‘cfv 6348  (class class class)co 7148  ⟨“cs3 14196  Basecbs 16475  distcds 16566  TarskiGcstrkg 26208  Itvcitv 26214  LineGclng 26215  pInvGcmir 26430  ∟Gcrag 26471  ⟂Gcperpg 26473 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-map 8400  df-pm 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-dju 9322  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-3 11693  df-n0 11890  df-xnn0 11960  df-z 11974  df-uz 12236  df-fz 12885  df-fzo 13026  df-hash 13683  df-word 13854  df-concat 13915  df-s1 13942  df-s2 14202  df-s3 14203  df-trkgc 26226  df-trkgb 26227  df-trkgcb 26228  df-trkg 26231  df-cgrg 26289  df-leg 26361  df-mir 26431  df-rag 26472  df-perpg 26474 This theorem is referenced by:  mideulem  26514  opphllem3  26527
 Copyright terms: Public domain W3C validator