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

Theorem opphllem 28494
Description: Lemma 8.24 of [Schwabhauser] p. 66. This is used later for mideulem 28495 and later for opphl 28513. (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 480 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐺 ∈ TarskiG)
8 eqid 2726 . . . 4 (π‘†β€˜π‘₯) = (π‘†β€˜π‘₯)
9 mideu.2 . . . . 5 (πœ‘ β†’ 𝐡 ∈ 𝑃)
109adantr 480 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐡 ∈ 𝑃)
11 mideulem.3 . . . . 5 (πœ‘ β†’ 𝑂 ∈ 𝑃)
1211adantr 480 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑂 ∈ 𝑃)
13 mideu.1 . . . . 5 (πœ‘ β†’ 𝐴 ∈ 𝑃)
1413adantr 480 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐴 ∈ 𝑃)
15 opphllem.1 . . . . 5 (πœ‘ β†’ 𝑅 ∈ 𝑃)
1615adantr 480 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑅 ∈ 𝑃)
17 simprl 768 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ 𝑃)
18 mideulem.1 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 β‰  𝐡)
1918necomd 2990 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 β‰  𝐴)
2019neneqd 2939 . . . . . . . . . . . 12 (πœ‘ β†’ Β¬ 𝐡 = 𝐴)
2120adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ Β¬ 𝐡 = 𝐴)
22 mideulem.6 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐴𝐿𝐡)(βŸ‚Gβ€˜πΊ)(𝐴𝐿𝑂))
234, 6, 22perpln2 28470 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐴𝐿𝑂) ∈ ran 𝐿)
241, 3, 4, 6, 13, 11, 23tglnne 28387 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 β‰  𝑂)
2524necomd 2990 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑂 β‰  𝐴)
2625neneqd 2939 . . . . . . . . . . . 12 (πœ‘ β†’ Β¬ 𝑂 = 𝐴)
2726adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ Β¬ 𝑂 = 𝐴)
2821, 27jca 511 . . . . . . . . . 10 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ (Β¬ 𝐡 = 𝐴 ∧ Β¬ 𝑂 = 𝐴))
296adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ 𝐺 ∈ TarskiG)
309adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ 𝐡 ∈ 𝑃)
3113adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ 𝐴 ∈ 𝑃)
3211adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ 𝑂 ∈ 𝑃)
331, 3, 4, 6, 9, 13, 19tglinerflx2 28393 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 ∈ (𝐡𝐿𝐴))
341, 3, 4, 6, 13, 9, 18tglinecom 28394 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐴𝐿𝐡) = (𝐡𝐿𝐴))
3534, 22eqbrtrrd 5165 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐡𝐿𝐴)(βŸ‚Gβ€˜πΊ)(𝐴𝐿𝑂))
361, 2, 3, 4, 6, 9, 13, 33, 11, 35perprag 28485 . . . . . . . . . . . . 13 (πœ‘ β†’ βŸ¨β€œπ΅π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ))
3736adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ βŸ¨β€œπ΅π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ))
38 simpr 484 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ 𝑂 ∈ (𝐡𝐿𝐴))
3938orcd 870 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ (𝑂 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴))
401, 2, 3, 4, 5, 29, 30, 31, 32, 37, 39ragflat3 28465 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ (𝐡 = 𝐴 ∨ 𝑂 = 𝐴))
41 oran 986 . . . . . . . . . . 11 ((𝐡 = 𝐴 ∨ 𝑂 = 𝐴) ↔ Β¬ (Β¬ 𝐡 = 𝐴 ∧ Β¬ 𝑂 = 𝐴))
4240, 41sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ 𝑂 ∈ (𝐡𝐿𝐴)) β†’ Β¬ (Β¬ 𝐡 = 𝐴 ∧ Β¬ 𝑂 = 𝐴))
4328, 42pm2.65da 814 . . . . . . . . 9 (πœ‘ β†’ Β¬ 𝑂 ∈ (𝐡𝐿𝐴))
4443adantr 480 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ 𝑂 ∈ (𝐡𝐿𝐴))
4534adantr 480 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐴𝐿𝐡) = (𝐡𝐿𝐴))
4644, 45neleqtrrd 2850 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ 𝑂 ∈ (𝐴𝐿𝐡))
4718adantr 480 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐴 β‰  𝐡)
4847neneqd 2939 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ 𝐴 = 𝐡)
4946, 48jca 511 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (Β¬ 𝑂 ∈ (𝐴𝐿𝐡) ∧ Β¬ 𝐴 = 𝐡))
50 pm4.56 985 . . . . . 6 ((Β¬ 𝑂 ∈ (𝐴𝐿𝐡) ∧ Β¬ 𝐴 = 𝐡) ↔ Β¬ (𝑂 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
5149, 50sylib 217 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ (𝑂 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
521, 4, 3, 7, 14, 10, 12, 51ncolrot2 28322 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ (𝐡 ∈ (𝑂𝐿𝐴) ∨ 𝑂 = 𝐴))
53 simprrr 779 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝑅𝐼𝑂))
541, 2, 3, 7, 16, 17, 12, 53tgbtwncom 28247 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝑂𝐼𝑅))
55 mideulem.4 . . . . . . . 8 (πœ‘ β†’ 𝑇 ∈ 𝑃)
5655adantr 480 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑇 ∈ 𝑃)
57 mideulem.7 . . . . . . . 8 (πœ‘ β†’ 𝑇 ∈ (𝐴𝐿𝐡))
5857adantr 480 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑇 ∈ (𝐴𝐿𝐡))
59 simprrl 778 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝑇𝐼𝐡))
601, 3, 4, 7, 56, 14, 10, 17, 58, 59coltr3 28407 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝐴𝐿𝐡))
6143, 34neleqtrrd 2850 . . . . . . 7 (πœ‘ β†’ Β¬ 𝑂 ∈ (𝐴𝐿𝐡))
6261adantr 480 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ Β¬ 𝑂 ∈ (𝐴𝐿𝐡))
63 nelne2 3034 . . . . . 6 ((π‘₯ ∈ (𝐴𝐿𝐡) ∧ Β¬ 𝑂 ∈ (𝐴𝐿𝐡)) β†’ π‘₯ β‰  𝑂)
6460, 62, 63syl2anc 583 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ β‰  𝑂)
651, 2, 3, 7, 12, 17, 16, 54, 64tgbtwnne 28249 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑂 β‰  𝑅)
661, 2, 3, 4, 5, 6, 9, 13, 11israg 28456 . . . . . . . 8 (πœ‘ β†’ (βŸ¨β€œπ΅π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ) ↔ (𝐡 βˆ’ 𝑂) = (𝐡 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚))))
6736, 66mpbid 231 . . . . . . 7 (πœ‘ β†’ (𝐡 βˆ’ 𝑂) = (𝐡 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
6867ad3antrrr 727 . . . . . 6 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐡 βˆ’ 𝑂) = (𝐡 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
696ad3antrrr 727 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐺 ∈ TarskiG)
70 eqid 2726 . . . . . . . . 9 (π‘†β€˜π΄) = (π‘†β€˜π΄)
711, 2, 3, 4, 5, 7, 14, 70, 12mircl 28420 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ ((π‘†β€˜π΄)β€˜π‘‚) ∈ 𝑃)
7271ad2antrr 723 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ ((π‘†β€˜π΄)β€˜π‘‚) ∈ 𝑃)
7313ad3antrrr 727 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐴 ∈ 𝑃)
7411ad3antrrr 727 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝑂 ∈ 𝑃)
7515ad3antrrr 727 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝑅 ∈ 𝑃)
769ad3antrrr 727 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐡 ∈ 𝑃)
77 simplr 766 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝑠 ∈ 𝑃)
781, 2, 3, 4, 5, 69, 73, 70, 74mirbtwn 28417 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐴 ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑂))
79 eqid 2726 . . . . . . . . 9 (π‘†β€˜π΅) = (π‘†β€˜π΅)
801, 2, 3, 4, 5, 69, 76, 79, 77mirbtwn 28417 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐡 ∈ (((π‘†β€˜π΅)β€˜π‘ )𝐼𝑠))
81 simpr 484 . . . . . . . . . . 11 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ ))
8269ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝐺 ∈ TarskiG)
8373ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝐴 ∈ 𝑃)
8476ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝐡 ∈ 𝑃)
8547ad4antr 729 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝐴 β‰  𝐡)
86 mideulem.2 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑄 ∈ 𝑃)
8786ad5antr 731 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑄 ∈ 𝑃)
8874ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑂 ∈ 𝑃)
8956ad4antr 729 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑇 ∈ 𝑃)
90 mideulem.5 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐴𝐿𝐡)(βŸ‚Gβ€˜πΊ)(𝑄𝐿𝐡))
9190ad5antr 731 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (𝐴𝐿𝐡)(βŸ‚Gβ€˜πΊ)(𝑄𝐿𝐡))
9222ad5antr 731 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (𝐴𝐿𝐡)(βŸ‚Gβ€˜πΊ)(𝐴𝐿𝑂))
9358ad4antr 729 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑇 ∈ (𝐴𝐿𝐡))
94 mideulem.8 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑇 ∈ (𝑄𝐼𝑂))
9594ad5antr 731 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑇 ∈ (𝑄𝐼𝑂))
9675ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑅 ∈ 𝑃)
97 opphllem.2 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑅 ∈ (𝐡𝐼𝑄))
9897ad5antr 731 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑅 ∈ (𝐡𝐼𝑄))
99 opphllem.3 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐴 βˆ’ 𝑂) = (𝐡 βˆ’ 𝑅))
10099ad5antr 731 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (𝐴 βˆ’ 𝑂) = (𝐡 βˆ’ 𝑅))
10117ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ π‘₯ ∈ 𝑃)
102101ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ π‘₯ ∈ 𝑃)
103 simp-5r 783 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂))))
104103simprd 495 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))
105104simpld 494 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ π‘₯ ∈ (𝑇𝐼𝐡))
106104simprd 495 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ π‘₯ ∈ (𝑅𝐼𝑂))
10777ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑠 ∈ 𝑃)
108 simpllr 773 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅)))
109108simpld 494 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠))
110 simprr 770 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))
111110ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))
112 simplr 766 . . . . . . . . . . . . . . 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 28493 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝐡 = π‘š)
114113eqcomd 2732 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ π‘š = 𝐡)
115114fveq2d 6889 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ (π‘†β€˜π‘š) = (π‘†β€˜π΅))
116115fveq1d 6887 . . . . . . . . . . 11 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ ((π‘†β€˜π‘š)β€˜π‘ ) = ((π‘†β€˜π΅)β€˜π‘ ))
11781, 116eqtrd 2766 . . . . . . . . . 10 ((((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) ∧ π‘š ∈ 𝑃) ∧ 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ )) β†’ 𝑅 = ((π‘†β€˜π΅)β€˜π‘ ))
118 eqid 2726 . . . . . . . . . . 11 (π‘†β€˜π‘š) = (π‘†β€˜π‘š)
1191, 2, 3, 4, 5, 69, 118, 77, 75, 101, 110midexlem 28451 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ βˆƒπ‘š ∈ 𝑃 𝑅 = ((π‘†β€˜π‘š)β€˜π‘ ))
120117, 119r19.29a 3156 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝑅 = ((π‘†β€˜π΅)β€˜π‘ ))
121120oveq1d 7420 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑅𝐼𝑠) = (((π‘†β€˜π΅)β€˜π‘ )𝐼𝑠))
12280, 121eleqtrrd 2830 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐡 ∈ (𝑅𝐼𝑠))
1231, 2, 3, 4, 5, 69, 73, 70, 74mircgr 28416 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐴 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)) = (𝐴 βˆ’ 𝑂))
12499ad3antrrr 727 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐴 βˆ’ 𝑂) = (𝐡 βˆ’ 𝑅))
125123, 124eqtrd 2766 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐴 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)) = (𝐡 βˆ’ 𝑅))
1261, 2, 3, 69, 73, 72, 76, 75, 125tgcgrcomlr 28239 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (((π‘†β€˜π΄)β€˜π‘‚) βˆ’ 𝐴) = (𝑅 βˆ’ 𝐡))
127120oveq2d 7421 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐡 βˆ’ 𝑅) = (𝐡 βˆ’ ((π‘†β€˜π΅)β€˜π‘ )))
1281, 2, 3, 4, 5, 69, 76, 79, 77mircgr 28416 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐡 βˆ’ ((π‘†β€˜π΅)β€˜π‘ )) = (𝐡 βˆ’ 𝑠))
129124, 127, 1283eqtrd 2770 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐴 βˆ’ 𝑂) = (𝐡 βˆ’ 𝑠))
1301, 2, 3, 69, 72, 73, 74, 75, 76, 77, 78, 122, 126, 129tgcgrextend 28244 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (((π‘†β€˜π΄)β€˜π‘‚) βˆ’ 𝑂) = (𝑅 βˆ’ 𝑠))
1311, 2, 3, 69, 72, 75axtgcgrrflx 28221 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (((π‘†β€˜π΄)β€˜π‘‚) βˆ’ 𝑅) = (𝑅 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
1321, 2, 3, 69, 74, 75axtgcgrrflx 28221 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑂 βˆ’ 𝑅) = (𝑅 βˆ’ 𝑂))
13353ad2antrr 723 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ π‘₯ ∈ (𝑅𝐼𝑂))
134 simprl 768 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠))
1351, 2, 3, 69, 72, 101, 77, 134tgbtwncom 28247 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ π‘₯ ∈ (𝑠𝐼((π‘†β€˜π΄)β€˜π‘‚)))
1361, 2, 3, 69, 101, 77, 101, 75, 110tgcgrcomlr 28239 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑠 βˆ’ π‘₯) = (𝑅 βˆ’ π‘₯))
137136eqcomd 2732 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑅 βˆ’ π‘₯) = (𝑠 βˆ’ π‘₯))
13836ad3antrrr 727 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ βŸ¨β€œπ΅π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ))
13947necomd 2990 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐡 β‰  𝐴)
140139ad2antrr 723 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ 𝐡 β‰  𝐴)
14160ad2antrr 723 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ π‘₯ ∈ (𝐴𝐿𝐡))
142141orcd 870 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (π‘₯ ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
1431, 4, 3, 69, 73, 76, 101, 142colcom 28317 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (π‘₯ ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴))
1441, 4, 3, 69, 76, 73, 101, 143colrot1 28318 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐡 ∈ (𝐴𝐿π‘₯) ∨ 𝐴 = π‘₯))
1451, 2, 3, 4, 5, 69, 76, 73, 74, 101, 138, 140, 144ragcol 28458 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ βŸ¨β€œπ‘₯π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ))
1461, 2, 3, 4, 5, 69, 101, 73, 74israg 28456 . . . . . . . . . 10 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (βŸ¨β€œπ‘₯π΄π‘‚β€βŸ© ∈ (∟Gβ€˜πΊ) ↔ (π‘₯ βˆ’ 𝑂) = (π‘₯ βˆ’ ((π‘†β€˜π΄)β€˜π‘‚))))
147145, 146mpbid 231 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (π‘₯ βˆ’ 𝑂) = (π‘₯ βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
1481, 2, 3, 69, 75, 101, 74, 77, 101, 72, 133, 135, 137, 147tgcgrextend 28244 . . . . . . . 8 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑅 βˆ’ 𝑂) = (𝑠 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
149132, 148eqtrd 2766 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝑂 βˆ’ 𝑅) = (𝑠 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
1501, 2, 3, 69, 72, 73, 74, 75, 75, 76, 77, 72, 78, 122, 130, 129, 131, 149tgifscgr 28267 . . . . . 6 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐴 βˆ’ 𝑅) = (𝐡 βˆ’ ((π‘†β€˜π΄)β€˜π‘‚)))
15168, 150eqtr4d 2769 . . . . 5 ((((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) ∧ 𝑠 ∈ 𝑃) ∧ (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅))) β†’ (𝐡 βˆ’ 𝑂) = (𝐴 βˆ’ 𝑅))
1521, 2, 3, 7, 71, 17, 17, 16axtgsegcon 28223 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ βˆƒπ‘  ∈ 𝑃 (π‘₯ ∈ (((π‘†β€˜π΄)β€˜π‘‚)𝐼𝑠) ∧ (π‘₯ βˆ’ 𝑠) = (π‘₯ βˆ’ 𝑅)))
153151, 152r19.29a 3156 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐡 βˆ’ 𝑂) = (𝐴 βˆ’ 𝑅))
15499adantr 480 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐴 βˆ’ 𝑂) = (𝐡 βˆ’ 𝑅))
1551, 2, 3, 7, 14, 12, 10, 16, 154tgcgrcomlr 28239 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝑂 βˆ’ 𝐴) = (𝑅 βˆ’ 𝐡))
156143, 152r19.29a 3156 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴))
1571, 4, 3, 7, 12, 16, 17, 54btwncolg1 28314 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ ∈ (𝑂𝐿𝑅) ∨ 𝑂 = 𝑅))
1581, 2, 3, 4, 5, 7, 8, 10, 12, 14, 16, 17, 52, 65, 153, 155, 156, 157symquadlem 28448 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝐡 = ((π‘†β€˜π‘₯)β€˜π΄))
1591, 2, 3, 4, 5, 7, 17, 8, 14mirbtwn 28417 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (((π‘†β€˜π‘₯)β€˜π΄)𝐼𝐴))
160158oveq1d 7420 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐡𝐼𝐴) = (((π‘†β€˜π‘₯)β€˜π΄)𝐼𝐴))
161159, 160eleqtrrd 2830 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝐡𝐼𝐴))
1621, 2, 3, 7, 10, 17, 14, 161tgbtwncom 28247 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ π‘₯ ∈ (𝐴𝐼𝐡))
1631, 2, 3, 7, 14, 10axtgcgrrflx 28221 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐴 βˆ’ 𝐡) = (𝐡 βˆ’ 𝐴))
164158oveq2d 7421 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ βˆ’ 𝐡) = (π‘₯ βˆ’ ((π‘†β€˜π‘₯)β€˜π΄)))
1651, 2, 3, 4, 5, 7, 17, 8, 14mircgr 28416 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ βˆ’ ((π‘†β€˜π‘₯)β€˜π΄)) = (π‘₯ βˆ’ 𝐴))
166164, 165eqtrd 2766 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ βˆ’ 𝐡) = (π‘₯ βˆ’ 𝐴))
1671, 2, 3, 7, 14, 17, 10, 12, 10, 17, 14, 16, 162, 161, 163, 166, 154, 153tgifscgr 28267 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (π‘₯ βˆ’ 𝑂) = (π‘₯ βˆ’ 𝑅))
1681, 2, 3, 4, 5, 7, 17, 8, 16, 12, 167, 54ismir 28418 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ 𝑂 = ((π‘†β€˜π‘₯)β€˜π‘…))
169158, 168jca 511 . 2 ((πœ‘ ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))) β†’ (𝐡 = ((π‘†β€˜π‘₯)β€˜π΄) ∧ 𝑂 = ((π‘†β€˜π‘₯)β€˜π‘…)))
1701, 2, 3, 6, 86, 55, 11, 94tgbtwncom 28247 . . 3 (πœ‘ β†’ 𝑇 ∈ (𝑂𝐼𝑄))
1711, 2, 3, 6, 11, 9, 86, 55, 15, 170, 97axtgpasch 28226 . 2 (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝑃 (π‘₯ ∈ (𝑇𝐼𝐡) ∧ π‘₯ ∈ (𝑅𝐼𝑂)))
172169, 171reximddv 3165 1 (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝑃 (𝐡 = ((π‘†β€˜π‘₯)β€˜π΄) ∧ 𝑂 = ((π‘†β€˜π‘₯)β€˜π‘…)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   ∨ wo 844   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆƒwrex 3064   class class class wbr 5141  β€˜cfv 6537  (class class class)co 7405  βŸ¨β€œcs3 14799  Basecbs 17153  distcds 17215  TarskiGcstrkg 28186  Itvcitv 28192  LineGclng 28193  pInvGcmir 28411  βˆŸGcrag 28452  βŸ‚Gcperpg 28454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-oadd 8471  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-fz 13491  df-fzo 13634  df-hash 14296  df-word 14471  df-concat 14527  df-s1 14552  df-s2 14805  df-s3 14806  df-trkgc 28207  df-trkgb 28208  df-trkgcb 28209  df-trkg 28212  df-cgrg 28270  df-leg 28342  df-mir 28412  df-rag 28453  df-perpg 28455
This theorem is referenced by:  mideulem  28495  opphllem3  28508
  Copyright terms: Public domain W3C validator