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

Theorem opphllem 27719
Description: Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 27720 and later for opphl 27738. (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 482 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐺 ∈ TarskiG)
8 eqid 2733 . . . 4 (π‘†β€˜π‘₯) = (π‘†β€˜π‘₯)
9 mideu.2 . . . . 5 (πœ‘ β†’ 𝐡 ∈ 𝑃)
109adantr 482 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐡 ∈ 𝑃)
11 mideulem.3 . . . . 5 (πœ‘ β†’ 𝑂 ∈ 𝑃)
1211adantr 482 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑂 ∈ 𝑃)
13 mideu.1 . . . . 5 (πœ‘ β†’ 𝐴 ∈ 𝑃)
1413adantr 482 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐴 ∈ 𝑃)
15 opphllem.1 . . . . 5 (πœ‘ β†’ 𝑅 ∈ 𝑃)
1615adantr 482 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑅 ∈ 𝑃)
17 simprl 770 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ 𝑃)
18 mideulem.1 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 β‰  𝐡)
1918necomd 2996 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 β‰  𝐴)
2019neneqd 2945 . . . . . . . . . . . 12 (πœ‘ β†’ Β¬ 𝐡 = 𝐴)
2120adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ Β¬ 𝐡 = 𝐴)
22 mideulem.6 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐴𝐿𝐡)(βŸ‚Gβ€˜πΊ)(𝐴𝐿𝑂))
234, 6, 22perpln2 27695 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐴𝐿𝑂) ∈ ran 𝐿)
241, 3, 4, 6, 13, 11, 23tglnne 27612 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 β‰  𝑂)
2524necomd 2996 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑂 β‰  𝐴)
2625neneqd 2945 . . . . . . . . . . . 12 (πœ‘ β†’ Β¬ 𝑂 = 𝐴)
2726adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ Β¬ 𝑂 = 𝐴)
2821, 27jca 513 . . . . . . . . . 10 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ (Β¬ 𝐡 = 𝐴 ∧ Β¬ 𝑂 = 𝐴))
296adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ 𝐺 ∈ TarskiG)
309adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ 𝐡 ∈ 𝑃)
3113adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ 𝐴 ∈ 𝑃)
3211adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ 𝑂 ∈ 𝑃)
331, 3, 4, 6, 9, 13, 19tglinerflx2 27618 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 ∈ (𝐡𝐿𝐴))
341, 3, 4, 6, 13, 9, 18tglinecom 27619 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐴𝐿𝐡) = (𝐡𝐿𝐴))
3534, 22eqbrtrrd 5130 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐡𝐿𝐴)(βŸ‚Gβ€˜πΊ)(𝐴𝐿𝑂))
361, 2, 3, 4, 6, 9, 13, 33, 11, 35perprag 27710 . . . . . . . . . . . . 13 (πœ‘ β†’ βŸ¨β€œπ΅π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ))
3736adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ βŸ¨β€œπ΅π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ))
38 simpr 486 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ 𝑂 ∈ (𝐡𝐿𝐴))
3938orcd 872 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ (𝑂 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴))
401, 2, 3, 4, 5, 29, 30, 31, 32, 37, 39ragflat3 27690 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ (𝐡 = 𝐴 ∨ 𝑂 = 𝐴))
41 oran 989 . . . . . . . . . . 11 ((𝐡 = 𝐴 ∨ 𝑂 = 𝐴) ↔ Β¬ (Β¬ 𝐡 = 𝐴 ∧ Β¬ 𝑂 = 𝐴))
4240, 41sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ Β¬ (Β¬ 𝐡 = 𝐴 ∧ Β¬ 𝑂 = 𝐴))
4328, 42pm2.65da 816 . . . . . . . . 9 (πœ‘ β†’ Β¬ 𝑂 ∈ (𝐡𝐿𝐴))
4443adantr 482 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ 𝑂 ∈ (𝐡𝐿𝐴))
4534adantr 482 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐴𝐿𝐡) = (𝐡𝐿𝐴))
4644, 45neleqtrrd 2857 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ 𝑂 ∈ (𝐴𝐿𝐡))
4718adantr 482 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐴 β‰  𝐡)
4847neneqd 2945 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ 𝐴 = 𝐡)
4946, 48jca 513 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (Β¬ 𝑂 ∈ (𝐴𝐿𝐡) ∧ Β¬ 𝐴 = 𝐡))
50 pm4.56 988 . . . . . 6 ((Β¬ 𝑂 ∈ (𝐴𝐿𝐡) ∧ Β¬ 𝐴 = 𝐡) ↔ Β¬ (𝑂 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
5149, 50sylib 217 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ (𝑂 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
521, 4, 3, 7, 14, 10, 12, 51ncolrot2 27547 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ (𝐡 ∈ (𝑂𝐿𝐴) ∨ 𝑂 = 𝐴))
53 simprrr 781 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝑅𝐼𝑂))
541, 2, 3, 7, 16, 17, 12, 53tgbtwncom 27472 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝑂𝐼𝑅))
55 mideulem.4 . . . . . . . 8 (πœ‘ β†’ 𝑇 ∈ 𝑃)
5655adantr 482 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑇 ∈ 𝑃)
57 mideulem.7 . . . . . . . 8 (πœ‘ β†’ 𝑇 ∈ (𝐴𝐿𝐡))
5857adantr 482 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑇 ∈ (𝐴𝐿𝐡))
59 simprrl 780 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝑇𝐼𝐡))
601, 3, 4, 7, 56, 14, 10, 17, 58, 59coltr3 27632 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝐴𝐿𝐡))
6143, 34neleqtrrd 2857 . . . . . . 7 (πœ‘ β†’ Β¬ 𝑂 ∈ (𝐴𝐿𝐡))
6261adantr 482 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ 𝑂 ∈ (𝐴𝐿𝐡))
63 nelne2 3039 . . . . . 6 ((π‘₯ ∈ (𝐴𝐿𝐡) ∧ Β¬ 𝑂 ∈ (𝐴𝐿𝐡)) β†’ π‘₯ β‰  𝑂)
6460, 62, 63syl2anc 585 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ β‰  𝑂)
651, 2, 3, 7, 12, 17, 16, 54, 64tgbtwnne 27474 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑂 β‰  𝑅)
661, 2, 3, 4, 5, 6, 9, 13, 11israg 27681 . . . . . . . 8 (πœ‘ β†’ (βŸ¨β€œπ΅π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ) ↔ (𝐡 βˆ’ 𝑂) = (𝐡 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚))))
6736, 66mpbid 231 . . . . . . 7 (πœ‘ β†’ (𝐡 βˆ’ 𝑂) = (𝐡 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
6867ad3antrrr 729 . . . . . 6 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐡 βˆ’ 𝑂) = (𝐡 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
696ad3antrrr 729 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐺 ∈ TarskiG)
70 eqid 2733 . . . . . . . . 9 (π‘†β€˜π΄) = (π‘†β€˜π΄)
711, 2, 3, 4, 5, 7, 14, 70, 12mircl 27645 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ ((π‘†β€˜π΄)β€˜π‘‚) ∈ 𝑃)
7271ad2antrr 725 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ ((π‘†β€˜π΄)β€˜π‘‚) ∈ 𝑃)
7313ad3antrrr 729 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐴 ∈ 𝑃)
7411ad3antrrr 729 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝑂 ∈ 𝑃)
7515ad3antrrr 729 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝑅 ∈ 𝑃)
769ad3antrrr 729 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐡 ∈ 𝑃)
77 simplr 768 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝑠 ∈ 𝑃)
781, 2, 3, 4, 5, 69, 73, 70, 74mirbtwn 27642 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐴 ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑂))
79 eqid 2733 . . . . . . . . 9 (π‘†β€˜π΅) = (π‘†β€˜π΅)
801, 2, 3, 4, 5, 69, 76, 79, 77mirbtwn 27642 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐡 ∈ (((π‘†β€˜π΅)β€˜π‘ )𝐼𝑠))
81 simpr 486 . . . . . . . . . . 11 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ ))
8269ad2antrr 725 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝐺 ∈ TarskiG)
8373ad2antrr 725 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝐴 ∈ 𝑃)
8476ad2antrr 725 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝐡 ∈ 𝑃)
8547ad4antr 731 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝐴 β‰  𝐡)
86 mideulem.2 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑄 ∈ 𝑃)
8786ad5antr 733 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑄 ∈ 𝑃)
8874ad2antrr 725 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑂 ∈ 𝑃)
8956ad4antr 731 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑇 ∈ 𝑃)
90 mideulem.5 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐴𝐿𝐡)(βŸ‚Gβ€˜πΊ)(𝑄𝐿𝐡))
9190ad5antr 733 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (𝐴𝐿𝐡)(βŸ‚Gβ€˜πΊ)(𝑄𝐿𝐡))
9222ad5antr 733 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (𝐴𝐿𝐡)(βŸ‚Gβ€˜πΊ)(𝐴𝐿𝑂))
9358ad4antr 731 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑇 ∈ (𝐴𝐿𝐡))
94 mideulem.8 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑇 ∈ (𝑄𝐼𝑂))
9594ad5antr 733 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑇 ∈ (𝑄𝐼𝑂))
9675ad2antrr 725 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑅 ∈ 𝑃)
97 opphllem.2 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑅 ∈ (𝐡𝐼𝑄))
9897ad5antr 733 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑅 ∈ (𝐡𝐼𝑄))
99 opphllem.3 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐴 βˆ’ 𝑂) = (𝐡 βˆ’ 𝑅))
10099ad5antr 733 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (𝐴 βˆ’ 𝑂) = (𝐡 βˆ’ 𝑅))
10117ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ π‘₯ ∈ 𝑃)
102101ad2antrr 725 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ π‘₯ ∈ 𝑃)
103 simp-5r 785 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂))))
104103simprd 497 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))
105104simpld 496 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ π‘₯ ∈ (𝑇𝐼𝐡))
106104simprd 497 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ π‘₯ ∈ (𝑅𝐼𝑂))
10777ad2antrr 725 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑠 ∈ 𝑃)
108 simpllr 775 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅)))
109108simpld 496 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠))
110 simprr 772 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))
111110ad2antrr 725 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))
112 simplr 768 . . . . . . . . . . . . . . 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 27718 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝐡 = π‘š)
114113eqcomd 2739 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ π‘š = 𝐡)
115114fveq2d 6847 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (π‘†β€˜π‘š) = (π‘†β€˜π΅))
116115fveq1d 6845 . . . . . . . . . . 11 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ ((π‘†β€˜π‘š)β€˜π‘ ) = ((π‘†β€˜π΅)β€˜π‘ ))
11781, 116eqtrd 2773 . . . . . . . . . 10 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑅 = ((π‘†β€˜π΅)β€˜π‘ ))
118 eqid 2733 . . . . . . . . . . 11 (π‘†β€˜π‘š) = (π‘†β€˜π‘š)
1191, 2, 3, 4, 5, 69, 118, 77, 75, 101, 110midexlem 27676 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ βˆƒπ‘š ∈ 𝑃 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ ))
120117, 119r19.29a 3156 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝑅 = ((π‘†β€˜π΅)β€˜π‘ ))
121120oveq1d 7373 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑅𝐼𝑠) = (((π‘†β€˜π΅)β€˜π‘ )𝐼𝑠))
12280, 121eleqtrrd 2837 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐡 ∈ (𝑅𝐼𝑠))
1231, 2, 3, 4, 5, 69, 73, 70, 74mircgr 27641 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐴 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)) = (𝐴 βˆ’ 𝑂))
12499ad3antrrr 729 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐴 βˆ’ 𝑂) = (𝐡 βˆ’ 𝑅))
125123, 124eqtrd 2773 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐴 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)) = (𝐡 βˆ’ 𝑅))
1261, 2, 3, 69, 73, 72, 76, 75, 125tgcgrcomlr 27464 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (((π‘†β€˜π΄)β€˜π‘‚) βˆ’ 𝐴) = (𝑅 βˆ’ 𝐡))
127120oveq2d 7374 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐡 βˆ’ 𝑅) = (𝐡 βˆ’ ((π‘†β€˜π΅)β€˜π‘ )))
1281, 2, 3, 4, 5, 69, 76, 79, 77mircgr 27641 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐡 βˆ’ ((π‘†β€˜π΅)β€˜π‘ )) = (𝐡 βˆ’ 𝑠))
129124, 127, 1283eqtrd 2777 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐴 βˆ’ 𝑂) = (𝐡 βˆ’ 𝑠))
1301, 2, 3, 69, 72, 73, 74, 75, 76, 77, 78, 122, 126, 129tgcgrextend 27469 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (((π‘†β€˜π΄)β€˜π‘‚) βˆ’ 𝑂) = (𝑅 βˆ’ 𝑠))
1311, 2, 3, 69, 72, 75axtgcgrrflx 27446 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (((π‘†β€˜π΄)β€˜π‘‚) βˆ’ 𝑅) = (𝑅 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
1321, 2, 3, 69, 74, 75axtgcgrrflx 27446 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑂 βˆ’ 𝑅) = (𝑅 βˆ’ 𝑂))
13353ad2antrr 725 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ π‘₯ ∈ (𝑅𝐼𝑂))
134 simprl 770 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠))
1351, 2, 3, 69, 72, 101, 77, 134tgbtwncom 27472 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ π‘₯ ∈ (𝑠𝐼((π‘†β€˜π΄)β€˜π‘‚)))
1361, 2, 3, 69, 101, 77, 101, 75, 110tgcgrcomlr 27464 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑠 βˆ’ π‘₯) = (𝑅 βˆ’ π‘₯))
137136eqcomd 2739 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑅 βˆ’ π‘₯) = (𝑠 βˆ’ π‘₯))
13836ad3antrrr 729 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ βŸ¨β€œπ΅π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ))
13947necomd 2996 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐡 β‰  𝐴)
140139ad2antrr 725 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐡 β‰  𝐴)
14160ad2antrr 725 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ π‘₯ ∈ (𝐴𝐿𝐡))
142141orcd 872 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (π‘₯ ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
1431, 4, 3, 69, 73, 76, 101, 142colcom 27542 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (π‘₯ ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴))
1441, 4, 3, 69, 76, 73, 101, 143colrot1 27543 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐡 ∈ (𝐴𝐿π‘₯) ∨ 𝐴 = π‘₯))
1451, 2, 3, 4, 5, 69, 76, 73, 74, 101, 138, 140, 144ragcol 27683 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ βŸ¨β€œπ‘₯π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ))
1461, 2, 3, 4, 5, 69, 101, 73, 74israg 27681 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (βŸ¨β€œπ‘₯π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ) ↔ (π‘₯ βˆ’ 𝑂) = (π‘₯ βˆ’ ((π‘†β€˜π΄)β€˜π‘‚))))
147145, 146mpbid 231 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (π‘₯ βˆ’ 𝑂) = (π‘₯ βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
1481, 2, 3, 69, 75, 101, 74, 77, 101, 72, 133, 135, 137, 147tgcgrextend 27469 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑅 βˆ’ 𝑂) = (𝑠 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
149132, 148eqtrd 2773 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑂 βˆ’ 𝑅) = (𝑠 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
1501, 2, 3, 69, 72, 73, 74, 75, 75, 76, 77, 72, 78, 122, 130, 129, 131, 149tgifscgr 27492 . . . . . 6 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐴 βˆ’ 𝑅) = (𝐡 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
15168, 150eqtr4d 2776 . . . . 5 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐡 βˆ’ 𝑂) = (𝐴 βˆ’ 𝑅))
1521, 2, 3, 7, 71, 17, 17, 16axtgsegcon 27448 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ βˆƒπ‘  ∈ 𝑃 (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅)))
153151, 152r19.29a 3156 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐡 βˆ’ 𝑂) = (𝐴 βˆ’ 𝑅))
15499adantr 482 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐴 βˆ’ 𝑂) = (𝐡 βˆ’ 𝑅))
1551, 2, 3, 7, 14, 12, 10, 16, 154tgcgrcomlr 27464 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝑂 βˆ’ 𝐴) = (𝑅 βˆ’ 𝐡))
156143, 152r19.29a 3156 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴))
1571, 4, 3, 7, 12, 16, 17, 54btwncolg1 27539 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ ∈ (𝑂𝐿𝑅) ∨ 𝑂 = 𝑅))
1581, 2, 3, 4, 5, 7, 8, 10, 12, 14, 16, 17, 52, 65, 153, 155, 156, 157symquadlem 27673 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐡 = ((π‘†β€˜π‘₯)β€˜π΄))
1591, 2, 3, 4, 5, 7, 17, 8, 14mirbtwn 27642 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (((π‘†β€˜π‘₯)β€˜π΄)𝐼𝐴))
160158oveq1d 7373 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐡𝐼𝐴) = (((π‘†β€˜π‘₯)β€˜π΄)𝐼𝐴))
161159, 160eleqtrrd 2837 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝐡𝐼𝐴))
1621, 2, 3, 7, 10, 17, 14, 161tgbtwncom 27472 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝐴𝐼𝐡))
1631, 2, 3, 7, 14, 10axtgcgrrflx 27446 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐴 βˆ’ 𝐡) = (𝐡 βˆ’ 𝐴))
164158oveq2d 7374 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ βˆ’ 𝐡) = (π‘₯ βˆ’ ((π‘†β€˜π‘₯)β€˜π΄)))
1651, 2, 3, 4, 5, 7, 17, 8, 14mircgr 27641 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ βˆ’ ((π‘†β€˜π‘₯)β€˜π΄)) = (π‘₯ βˆ’ 𝐴))
166164, 165eqtrd 2773 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ βˆ’ 𝐡) = (π‘₯ βˆ’ 𝐴))
1671, 2, 3, 7, 14, 17, 10, 12, 10, 17, 14, 16, 162, 161, 163, 166, 154, 153tgifscgr 27492 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ βˆ’ 𝑂) = (π‘₯ βˆ’ 𝑅))
1681, 2, 3, 4, 5, 7, 17, 8, 16, 12, 167, 54ismir 27643 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑂 = ((π‘†β€˜π‘₯)β€˜π‘…))
169158, 168jca 513 . 2 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐡 = ((π‘†β€˜π‘₯)β€˜π΄) ∧ 𝑂 = ((π‘†β€˜π‘₯)β€˜π‘…)))
1701, 2, 3, 6, 86, 55, 11, 94tgbtwncom 27472 . . 3 (πœ‘ β†’ 𝑇 ∈ (𝑂𝐼𝑄))
1711, 2, 3, 6, 11, 9, 86, 55, 15, 170, 97axtgpasch 27451 . 2 (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝑃 (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))
172169, 171reximddv 3165 1 (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝑃 (𝐡 = ((π‘†β€˜π‘₯)β€˜π΄) ∧ 𝑂 = ((π‘†β€˜π‘₯)β€˜π‘…)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆƒwrex 3070   class class class wbr 5106  β€˜cfv 6497  (class class class)co 7358  βŸ¨β€œcs3 14737  Basecbs 17088  distcds 17147  TarskiGcstrkg 27411  Itvcitv 27417  LineGclng 27418  pInvGcmir 27636  βˆŸGcrag 27677  βŸ‚Gcperpg 27679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-oadd 8417  df-er 8651  df-map 8770  df-pm 8771  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-dju 9842  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-nn 12159  df-2 12221  df-3 12222  df-n0 12419  df-xnn0 12491  df-z 12505  df-uz 12769  df-fz 13431  df-fzo 13574  df-hash 14237  df-word 14409  df-concat 14465  df-s1 14490  df-s2 14743  df-s3 14744  df-trkgc 27432  df-trkgb 27433  df-trkgcb 27434  df-trkg 27437  df-cgrg 27495  df-leg 27567  df-mir 27637  df-rag 27678  df-perpg 27680
This theorem is referenced by:  mideulem  27720  opphllem3  27733
  Copyright terms: Public domain W3C validator