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

Theorem midexlem 28211
Description: Lemma for the existence of a middle point. Lemma 7.25 of [Schwabhauser] p. 55. This proof of the existence of a midpoint requires the existence of a third point 𝐢 equidistant to 𝐴 and 𝐡 This condition will be removed later. Because the operation notation (𝐴(midGβ€˜πΊ)𝐡) for a midpoint implies its uniqueness, it cannot be used until uniqueness is proven, and until then, an equivalent mirror point notation 𝐡 = (π‘€β€˜π΄) has to be used. See mideu 28257 for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019.)
Hypotheses
Ref Expression
mirval.p 𝑃 = (Baseβ€˜πΊ)
mirval.d βˆ’ = (distβ€˜πΊ)
mirval.i 𝐼 = (Itvβ€˜πΊ)
mirval.l 𝐿 = (LineGβ€˜πΊ)
mirval.s 𝑆 = (pInvGβ€˜πΊ)
mirval.g (πœ‘ β†’ 𝐺 ∈ TarskiG)
midexlem.m 𝑀 = (π‘†β€˜π‘₯)
midexlem.a (πœ‘ β†’ 𝐴 ∈ 𝑃)
midexlem.b (πœ‘ β†’ 𝐡 ∈ 𝑃)
midexlem.c (πœ‘ β†’ 𝐢 ∈ 𝑃)
midexlem.1 (πœ‘ β†’ (𝐢 βˆ’ 𝐴) = (𝐢 βˆ’ 𝐡))
Assertion
Ref Expression
midexlem (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
Distinct variable groups:   π‘₯, βˆ’   π‘₯,𝐴   π‘₯,𝐡   π‘₯,𝐢   π‘₯,𝐼   π‘₯,𝐿   π‘₯,𝑃   π‘₯,𝑆   πœ‘,π‘₯
Allowed substitution hints:   𝐺(π‘₯)   𝑀(π‘₯)

Proof of Theorem midexlem
Dummy variables 𝑝 π‘ž π‘Ÿ 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 midexlem.c . . . . 5 (πœ‘ β†’ 𝐢 ∈ 𝑃)
2 midexlem.m . . . . . . . 8 𝑀 = (π‘†β€˜π‘₯)
3 fveq2 6891 . . . . . . . 8 (π‘₯ = 𝐢 β†’ (π‘†β€˜π‘₯) = (π‘†β€˜πΆ))
42, 3eqtrid 2783 . . . . . . 7 (π‘₯ = 𝐢 β†’ 𝑀 = (π‘†β€˜πΆ))
54fveq1d 6893 . . . . . 6 (π‘₯ = 𝐢 β†’ (π‘€β€˜π΄) = ((π‘†β€˜πΆ)β€˜π΄))
65rspceeqv 3633 . . . . 5 ((𝐢 ∈ 𝑃 ∧ 𝐡 = ((π‘†β€˜πΆ)β€˜π΄)) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
71, 6sylan 579 . . . 4 ((πœ‘ ∧ 𝐡 = ((π‘†β€˜πΆ)β€˜π΄)) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
87adantlr 712 . . 3 (((πœ‘ ∧ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝐡 = ((π‘†β€˜πΆ)β€˜π΄)) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
9 midexlem.a . . . . 5 (πœ‘ β†’ 𝐴 ∈ 𝑃)
10 mirval.p . . . . . . . 8 𝑃 = (Baseβ€˜πΊ)
11 mirval.d . . . . . . . 8 βˆ’ = (distβ€˜πΊ)
12 mirval.i . . . . . . . 8 𝐼 = (Itvβ€˜πΊ)
13 mirval.l . . . . . . . 8 𝐿 = (LineGβ€˜πΊ)
14 mirval.s . . . . . . . 8 𝑆 = (pInvGβ€˜πΊ)
15 mirval.g . . . . . . . 8 (πœ‘ β†’ 𝐺 ∈ TarskiG)
16 eqid 2731 . . . . . . . 8 (π‘†β€˜π΄) = (π‘†β€˜π΄)
1710, 11, 12, 13, 14, 15, 9, 16mircinv 28187 . . . . . . 7 (πœ‘ β†’ ((π‘†β€˜π΄)β€˜π΄) = 𝐴)
1817adantr 480 . . . . . 6 ((πœ‘ ∧ 𝐴 = 𝐡) β†’ ((π‘†β€˜π΄)β€˜π΄) = 𝐴)
19 simpr 484 . . . . . 6 ((πœ‘ ∧ 𝐴 = 𝐡) β†’ 𝐴 = 𝐡)
2018, 19eqtr2d 2772 . . . . 5 ((πœ‘ ∧ 𝐴 = 𝐡) β†’ 𝐡 = ((π‘†β€˜π΄)β€˜π΄))
21 fveq2 6891 . . . . . . . 8 (π‘₯ = 𝐴 β†’ (π‘†β€˜π‘₯) = (π‘†β€˜π΄))
222, 21eqtrid 2783 . . . . . . 7 (π‘₯ = 𝐴 β†’ 𝑀 = (π‘†β€˜π΄))
2322fveq1d 6893 . . . . . 6 (π‘₯ = 𝐴 β†’ (π‘€β€˜π΄) = ((π‘†β€˜π΄)β€˜π΄))
2423rspceeqv 3633 . . . . 5 ((𝐴 ∈ 𝑃 ∧ 𝐡 = ((π‘†β€˜π΄)β€˜π΄)) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
259, 20, 24syl2an2r 682 . . . 4 ((πœ‘ ∧ 𝐴 = 𝐡) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
2625adantlr 712 . . 3 (((πœ‘ ∧ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝐴 = 𝐡) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
2715adantr 480 . . . 4 ((πœ‘ ∧ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 𝐺 ∈ TarskiG)
28 eqid 2731 . . . 4 (π‘†β€˜πΆ) = (π‘†β€˜πΆ)
299adantr 480 . . . 4 ((πœ‘ ∧ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 𝐴 ∈ 𝑃)
30 midexlem.b . . . . 5 (πœ‘ β†’ 𝐡 ∈ 𝑃)
3130adantr 480 . . . 4 ((πœ‘ ∧ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 𝐡 ∈ 𝑃)
321adantr 480 . . . 4 ((πœ‘ ∧ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 𝐢 ∈ 𝑃)
33 simpr 484 . . . 4 ((πœ‘ ∧ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
34 midexlem.1 . . . . 5 (πœ‘ β†’ (𝐢 βˆ’ 𝐴) = (𝐢 βˆ’ 𝐡))
3534adantr 480 . . . 4 ((πœ‘ ∧ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ (𝐢 βˆ’ 𝐴) = (𝐢 βˆ’ 𝐡))
3610, 11, 12, 13, 14, 27, 28, 29, 31, 32, 33, 35colmid 28207 . . 3 ((πœ‘ ∧ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ (𝐡 = ((π‘†β€˜πΆ)β€˜π΄) ∨ 𝐴 = 𝐡))
378, 26, 36mpjaodan 956 . 2 ((πœ‘ ∧ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
3815adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 𝐺 ∈ TarskiG)
3938ad2antrr 723 . . . . . . . . . 10 ((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) β†’ 𝐺 ∈ TarskiG)
4039ad2antrr 723 . . . . . . . . 9 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ 𝐺 ∈ TarskiG)
4140ad2antrr 723 . . . . . . . 8 ((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) β†’ 𝐺 ∈ TarskiG)
4241adantr 480 . . . . . . 7 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ 𝐺 ∈ TarskiG)
43 simprl 768 . . . . . . 7 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ π‘₯ ∈ 𝑃)
449adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 𝐴 ∈ 𝑃)
4544ad2antrr 723 . . . . . . . . . 10 ((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) β†’ 𝐴 ∈ 𝑃)
4645ad2antrr 723 . . . . . . . . 9 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ 𝐴 ∈ 𝑃)
4746ad2antrr 723 . . . . . . . 8 ((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) β†’ 𝐴 ∈ 𝑃)
4847adantr 480 . . . . . . 7 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ 𝐴 ∈ 𝑃)
4930ad3antrrr 727 . . . . . . . . . 10 ((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) β†’ 𝐡 ∈ 𝑃)
5049ad2antrr 723 . . . . . . . . 9 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ 𝐡 ∈ 𝑃)
5150ad2antrr 723 . . . . . . . 8 ((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) β†’ 𝐡 ∈ 𝑃)
5251adantr 480 . . . . . . 7 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ 𝐡 ∈ 𝑃)
5342ad2antrr 723 . . . . . . . . 9 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐺 ∈ TarskiG)
54 simpllr 773 . . . . . . . . . 10 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ π‘Ÿ ∈ 𝑃)
5554ad2antrr 723 . . . . . . . . 9 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘Ÿ ∈ 𝑃)
561adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 𝐢 ∈ 𝑃)
5756ad2antrr 723 . . . . . . . . . . . . 13 ((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) β†’ 𝐢 ∈ 𝑃)
5857ad2antrr 723 . . . . . . . . . . . 12 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ 𝐢 ∈ 𝑃)
5958ad2antrr 723 . . . . . . . . . . 11 ((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) β†’ 𝐢 ∈ 𝑃)
6059adantr 480 . . . . . . . . . 10 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ 𝐢 ∈ 𝑃)
6160ad2antrr 723 . . . . . . . . 9 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐢 ∈ 𝑃)
6243ad2antrr 723 . . . . . . . . 9 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘₯ ∈ 𝑃)
63 eqid 2731 . . . . . . . . 9 (cgrGβ€˜πΊ) = (cgrGβ€˜πΊ)
6452ad2antrr 723 . . . . . . . . 9 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐡 ∈ 𝑃)
6548ad2antrr 723 . . . . . . . . 9 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐴 ∈ 𝑃)
66 simpr 484 . . . . . . . . . . 11 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ = 𝐴) β†’ π‘Ÿ = 𝐴)
6730adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 𝐡 ∈ 𝑃)
68 simpr 484 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
6910, 12, 13, 38, 56, 44, 67, 68ncolne1 28144 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 𝐢 β‰  𝐴)
7069ad7antr 735 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ 𝐢 β‰  𝐴)
7170ad2antrr 723 . . . . . . . . . . . . 13 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐢 β‰  𝐴)
7271adantr 480 . . . . . . . . . . . 12 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ = 𝐴) β†’ 𝐢 β‰  𝐴)
7372necomd 2995 . . . . . . . . . . 11 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ = 𝐴) β†’ 𝐴 β‰  𝐢)
7466, 73eqnetrd 3007 . . . . . . . . . 10 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ = 𝐴) β†’ π‘Ÿ β‰  𝐢)
7553adantr 480 . . . . . . . . . . 11 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ β‰  𝐴) β†’ 𝐺 ∈ TarskiG)
7655adantr 480 . . . . . . . . . . 11 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ β‰  𝐴) β†’ π‘Ÿ ∈ 𝑃)
7765adantr 480 . . . . . . . . . . 11 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ β‰  𝐴) β†’ 𝐴 ∈ 𝑃)
7861adantr 480 . . . . . . . . . . 11 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ β‰  𝐴) β†’ 𝐢 ∈ 𝑃)
79 simplr 766 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ π‘ž ∈ 𝑃)
8079ad3antrrr 727 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ π‘ž ∈ 𝑃)
8180ad2antrr 723 . . . . . . . . . . . . 13 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘ž ∈ 𝑃)
8281adantr 480 . . . . . . . . . . . 12 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ β‰  𝐴) β†’ π‘ž ∈ 𝑃)
8368ad9antr 739 . . . . . . . . . . . . . . . 16 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
8410, 13, 12, 53, 65, 64, 61, 83ncolrot2 28082 . . . . . . . . . . . . . . 15 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ Β¬ (𝐡 ∈ (𝐢𝐿𝐴) ∨ 𝐢 = 𝐴))
8515adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝐢 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴)) β†’ 𝐺 ∈ TarskiG)
8630adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝐢 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴)) β†’ 𝐡 ∈ 𝑃)
879adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝐢 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴)) β†’ 𝐴 ∈ 𝑃)
881adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝐢 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴)) β†’ 𝐢 ∈ 𝑃)
89 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝐢 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴)) β†’ (𝐢 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴))
9010, 13, 12, 85, 86, 87, 88, 89colcom 28077 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝐢 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴)) β†’ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
9190stoic1a 1773 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ Β¬ (𝐢 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴))
9291ad9antr 739 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ Β¬ (𝐢 ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴))
9310, 12, 13, 53, 61, 64, 65, 92ncolne1 28144 . . . . . . . . . . . . . . . . 17 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐢 β‰  𝐡)
9493necomd 2995 . . . . . . . . . . . . . . . 16 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐡 β‰  𝐢)
95 simprl 768 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ 𝐡 ∈ (πΆπΌπ‘ž))
9695ad3antrrr 727 . . . . . . . . . . . . . . . . . 18 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ 𝐡 ∈ (πΆπΌπ‘ž))
9796ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐡 ∈ (πΆπΌπ‘ž))
9810, 12, 13, 53, 61, 64, 81, 93, 97btwnlng3 28140 . . . . . . . . . . . . . . . 16 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘ž ∈ (𝐢𝐿𝐡))
9910, 12, 13, 53, 64, 61, 81, 94, 98lncom 28141 . . . . . . . . . . . . . . 15 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘ž ∈ (𝐡𝐿𝐢))
10053adantr 480 . . . . . . . . . . . . . . . . . 18 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘ž = 𝐢) β†’ 𝐺 ∈ TarskiG)
10161adantr 480 . . . . . . . . . . . . . . . . . 18 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘ž = 𝐢) β†’ 𝐢 ∈ 𝑃)
10264adantr 480 . . . . . . . . . . . . . . . . . 18 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘ž = 𝐢) β†’ 𝐡 ∈ 𝑃)
10397adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘ž = 𝐢) β†’ 𝐡 ∈ (πΆπΌπ‘ž))
104 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘ž = 𝐢) β†’ π‘ž = 𝐢)
105104oveq2d 7428 . . . . . . . . . . . . . . . . . . 19 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘ž = 𝐢) β†’ (πΆπΌπ‘ž) = (𝐢𝐼𝐢))
106103, 105eleqtrd 2834 . . . . . . . . . . . . . . . . . 18 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘ž = 𝐢) β†’ 𝐡 ∈ (𝐢𝐼𝐢))
10710, 11, 12, 100, 101, 102, 106axtgbtwnid 27985 . . . . . . . . . . . . . . . . 17 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘ž = 𝐢) β†’ 𝐢 = 𝐡)
10893adantr 480 . . . . . . . . . . . . . . . . . 18 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘ž = 𝐢) β†’ 𝐢 β‰  𝐡)
109108neneqd 2944 . . . . . . . . . . . . . . . . 17 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘ž = 𝐢) β†’ Β¬ 𝐢 = 𝐡)
110107, 109pm2.65da 814 . . . . . . . . . . . . . . . 16 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ Β¬ π‘ž = 𝐢)
111110neqned 2946 . . . . . . . . . . . . . . 15 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘ž β‰  𝐢)
11210, 12, 13, 53, 64, 61, 65, 81, 84, 99, 111ncolncol 28165 . . . . . . . . . . . . . 14 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ Β¬ (π‘ž ∈ (𝐢𝐿𝐴) ∨ 𝐢 = 𝐴))
11310, 13, 12, 53, 61, 65, 81, 112ncolcom 28080 . . . . . . . . . . . . 13 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ Β¬ (π‘ž ∈ (𝐴𝐿𝐢) ∨ 𝐴 = 𝐢))
114113adantr 480 . . . . . . . . . . . 12 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ β‰  𝐴) β†’ Β¬ (π‘ž ∈ (𝐴𝐿𝐢) ∨ 𝐴 = 𝐢))
115 simp-4r 781 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ 𝑝 ∈ 𝑃)
116115ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 ((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) β†’ 𝑝 ∈ 𝑃)
117116adantr 480 . . . . . . . . . . . . . . . . . 18 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ 𝑝 ∈ 𝑃)
118117ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝑝 ∈ 𝑃)
119 simp-4r 781 . . . . . . . . . . . . . . . . . . . . 21 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝)))
120119simprd 495 . . . . . . . . . . . . . . . . . . . 20 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))
121120eqcomd 2737 . . . . . . . . . . . . . . . . . . 19 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ (𝐴 βˆ’ 𝑝) = (𝐡 βˆ’ π‘ž))
122121ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐴 βˆ’ 𝑝) = (𝐡 βˆ’ π‘ž))
12310, 11, 12, 53, 65, 118, 64, 81, 122tgcgrcomlr 27999 . . . . . . . . . . . . . . . . 17 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝑝 βˆ’ 𝐴) = (π‘ž βˆ’ 𝐡))
124 simpllr 773 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝))
125124ad5antr 731 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝))
126125simprd 495 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐴 β‰  𝑝)
127126necomd 2995 . . . . . . . . . . . . . . . . 17 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝑝 β‰  𝐴)
12810, 11, 12, 53, 118, 65, 81, 64, 123, 127tgcgrneq 28002 . . . . . . . . . . . . . . . 16 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘ž β‰  𝐡)
12910, 12, 13, 53, 61, 64, 65, 81, 92, 98, 128ncolncol 28165 . . . . . . . . . . . . . . 15 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ Β¬ (π‘ž ∈ (𝐡𝐿𝐴) ∨ 𝐡 = 𝐴))
13010, 12, 13, 53, 81, 64, 65, 129ncolne2 28145 . . . . . . . . . . . . . 14 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘ž β‰  𝐴)
131130necomd 2995 . . . . . . . . . . . . . . 15 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐴 β‰  π‘ž)
132 simp-4r 781 . . . . . . . . . . . . . . . 16 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝)))
133132simpld 494 . . . . . . . . . . . . . . 15 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘Ÿ ∈ (π΄πΌπ‘ž))
13410, 12, 13, 53, 65, 81, 55, 131, 133btwnlng1 28138 . . . . . . . . . . . . . 14 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘Ÿ ∈ (π΄πΏπ‘ž))
13510, 12, 13, 53, 81, 65, 55, 130, 134lncom 28141 . . . . . . . . . . . . 13 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘Ÿ ∈ (π‘žπΏπ΄))
136135adantr 480 . . . . . . . . . . . 12 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ β‰  𝐴) β†’ π‘Ÿ ∈ (π‘žπΏπ΄))
137 simpr 484 . . . . . . . . . . . 12 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ β‰  𝐴) β†’ π‘Ÿ β‰  𝐴)
13810, 12, 13, 75, 82, 77, 78, 76, 114, 136, 137ncolncol 28165 . . . . . . . . . . 11 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ β‰  𝐴) β†’ Β¬ (π‘Ÿ ∈ (𝐴𝐿𝐢) ∨ 𝐴 = 𝐢))
13910, 12, 13, 75, 76, 77, 78, 138ncolne2 28145 . . . . . . . . . 10 ((((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) ∧ π‘Ÿ β‰  𝐴) β†’ π‘Ÿ β‰  𝐢)
14074, 139pm2.61dane 3028 . . . . . . . . 9 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘Ÿ β‰  𝐢)
141 simpllr 773 . . . . . . . . . . . 12 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ))))
142141simprd 495 . . . . . . . . . . 11 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))
143142simprd 495 . . . . . . . . . 10 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘₯ ∈ (π‘ŸπΌπΆ))
14410, 13, 12, 53, 55, 62, 61, 143btwncolg3 28076 . . . . . . . . 9 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐢 ∈ (π‘ŸπΏπ‘₯) ∨ π‘Ÿ = π‘₯))
145 simplr 766 . . . . . . . . . . 11 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝑠 ∈ 𝑃)
146 simplr 766 . . . . . . . . . . . . 13 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝)))
147146simprd 495 . . . . . . . . . . . 12 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ π‘Ÿ ∈ (𝐡𝐼𝑝))
148147ad2antrr 723 . . . . . . . . . . 11 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘Ÿ ∈ (𝐡𝐼𝑝))
149 simprl 768 . . . . . . . . . . 11 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝑠 ∈ (π΄πΌπ‘ž))
150124simpld 494 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ 𝐴 ∈ (𝐢𝐼𝑝))
151150ad2antrr 723 . . . . . . . . . . . . . . 15 ((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) β†’ 𝐴 ∈ (𝐢𝐼𝑝))
152151adantr 480 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ 𝐴 ∈ (𝐢𝐼𝑝))
15334ad8antr 737 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ (𝐢 βˆ’ 𝐴) = (𝐢 βˆ’ 𝐡))
154153eqcomd 2737 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ (𝐢 βˆ’ 𝐡) = (𝐢 βˆ’ 𝐴))
15510, 11, 12, 42, 48, 52axtgcgrrflx 27981 . . . . . . . . . . . . . 14 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ (𝐴 βˆ’ 𝐡) = (𝐡 βˆ’ 𝐴))
15610, 11, 12, 42, 60, 48, 117, 60, 52, 80, 52, 48, 70, 152, 96, 153, 121, 154, 155axtg5seg 27984 . . . . . . . . . . . . 13 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ (𝑝 βˆ’ 𝐡) = (π‘ž βˆ’ 𝐴))
15710, 11, 12, 42, 117, 52, 80, 48, 156tgcgrcomlr 27999 . . . . . . . . . . . 12 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ (𝐡 βˆ’ 𝑝) = (𝐴 βˆ’ π‘ž))
158157ad2antrr 723 . . . . . . . . . . 11 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐡 βˆ’ 𝑝) = (𝐴 βˆ’ π‘ž))
159 simprr 770 . . . . . . . . . . . 12 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)
16010, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159cgr3simp2 28040 . . . . . . . . . . 11 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘Ÿ βˆ’ 𝑝) = (𝑠 βˆ’ π‘ž))
16110, 11, 12, 53, 64, 65axtgcgrrflx 27981 . . . . . . . . . . 11 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐡 βˆ’ 𝐴) = (𝐴 βˆ’ 𝐡))
16210, 11, 12, 53, 64, 55, 118, 65, 65, 145, 81, 64, 148, 149, 158, 160, 161, 123tgifscgr 28027 . . . . . . . . . 10 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘Ÿ βˆ’ 𝐴) = (𝑠 βˆ’ 𝐡))
163 simp-10l 792 . . . . . . . . . . . . 13 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ πœ‘)
164125simpld 494 . . . . . . . . . . . . . . 15 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐴 ∈ (𝐢𝐼𝑝))
16510, 12, 13, 53, 61, 65, 118, 71, 164btwnlng3 28140 . . . . . . . . . . . . . 14 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝑝 ∈ (𝐢𝐿𝐴))
16610, 12, 13, 53, 61, 65, 64, 118, 83, 165, 127ncolncol 28165 . . . . . . . . . . . . 13 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ Β¬ (𝑝 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
16715ad2antrr 723 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑝 ∈ 𝑃) ∧ (𝐡 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) β†’ 𝐺 ∈ TarskiG)
168 simplr 766 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑝 ∈ 𝑃) ∧ (𝐡 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) β†’ 𝑝 ∈ 𝑃)
1699ad2antrr 723 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑝 ∈ 𝑃) ∧ (𝐡 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) β†’ 𝐴 ∈ 𝑃)
17030ad2antrr 723 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑝 ∈ 𝑃) ∧ (𝐡 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) β†’ 𝐡 ∈ 𝑃)
171 simpr 484 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑝 ∈ 𝑃) ∧ (𝐡 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) β†’ (𝐡 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
17210, 13, 12, 167, 168, 169, 170, 171colrot1 28078 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑝 ∈ 𝑃) ∧ (𝐡 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) β†’ (𝑝 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
173172stoic1a 1773 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝑃) ∧ Β¬ (𝑝 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ Β¬ (𝐡 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
174163, 118, 166, 173syl21anc 835 . . . . . . . . . . . 12 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ Β¬ (𝐡 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
17510, 12, 13, 53, 118, 65, 64, 166ncolne2 28145 . . . . . . . . . . . . . . 15 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝑝 β‰  𝐡)
176175necomd 2995 . . . . . . . . . . . . . 14 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝐡 β‰  𝑝)
177176neneqd 2944 . . . . . . . . . . . . 13 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ Β¬ 𝐡 = 𝑝)
17810, 13, 12, 53, 65, 81, 55, 133btwncolg1 28074 . . . . . . . . . . . . . . . 16 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘Ÿ ∈ (π΄πΏπ‘ž) ∨ 𝐴 = π‘ž))
17910, 11, 12, 53, 55, 65, 145, 64, 162tgcgrcomlr 27999 . . . . . . . . . . . . . . . . 17 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐴 βˆ’ π‘Ÿ) = (𝐡 βˆ’ 𝑠))
180120ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))
18110, 11, 12, 53, 118, 81axtgcgrrflx 27981 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝑝 βˆ’ π‘ž) = (π‘ž βˆ’ 𝑝))
18210, 11, 12, 53, 64, 55, 118, 81, 65, 145, 81, 118, 148, 149, 158, 160, 180, 181tgifscgr 28027 . . . . . . . . . . . . . . . . 17 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘Ÿ βˆ’ π‘ž) = (𝑠 βˆ’ 𝑝))
18310, 11, 12, 53, 65, 145, 81, 149tgbtwncom 28007 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝑠 ∈ (π‘žπΌπ΄))
18410, 11, 12, 42, 52, 54, 117, 147tgbtwncom 28007 . . . . . . . . . . . . . . . . . . 19 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ π‘Ÿ ∈ (𝑝𝐼𝐡))
185184ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘Ÿ ∈ (𝑝𝐼𝐡))
186160eqcomd 2737 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝑠 βˆ’ π‘ž) = (π‘Ÿ βˆ’ 𝑝))
18710, 11, 12, 53, 145, 81, 55, 118, 186tgcgrcomlr 27999 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘ž βˆ’ 𝑠) = (𝑝 βˆ’ π‘Ÿ))
18810, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159cgr3simp1 28039 . . . . . . . . . . . . . . . . . . . 20 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐡 βˆ’ π‘Ÿ) = (𝐴 βˆ’ 𝑠))
189188eqcomd 2737 . . . . . . . . . . . . . . . . . . 19 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐴 βˆ’ 𝑠) = (𝐡 βˆ’ π‘Ÿ))
19010, 11, 12, 53, 65, 145, 64, 55, 189tgcgrcomlr 27999 . . . . . . . . . . . . . . . . . 18 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝑠 βˆ’ 𝐴) = (π‘Ÿ βˆ’ 𝐡))
19110, 11, 12, 53, 81, 145, 65, 118, 55, 64, 183, 185, 187, 190tgcgrextend 28004 . . . . . . . . . . . . . . . . 17 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘ž βˆ’ 𝐴) = (𝑝 βˆ’ 𝐡))
19210, 11, 63, 53, 65, 55, 81, 64, 145, 118, 179, 182, 191trgcgr 28035 . . . . . . . . . . . . . . . 16 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ βŸ¨β€œπ΄π‘Ÿπ‘žβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΅π‘ π‘β€βŸ©)
19310, 13, 12, 53, 65, 55, 81, 63, 64, 145, 118, 178, 192lnxfr 28085 . . . . . . . . . . . . . . 15 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝑠 ∈ (𝐡𝐿𝑝) ∨ 𝐡 = 𝑝))
194193orcomd 868 . . . . . . . . . . . . . 14 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐡 = 𝑝 ∨ 𝑠 ∈ (𝐡𝐿𝑝)))
195194ord 861 . . . . . . . . . . . . 13 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (Β¬ 𝐡 = 𝑝 β†’ 𝑠 ∈ (𝐡𝐿𝑝)))
196177, 195mpd 15 . . . . . . . . . . . 12 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝑠 ∈ (𝐡𝐿𝑝))
19710, 12, 13, 53, 64, 118, 55, 176, 148btwnlng1 28138 . . . . . . . . . . . 12 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ π‘Ÿ ∈ (𝐡𝐿𝑝))
19810, 12, 13, 53, 65, 81, 145, 131, 149btwnlng1 28138 . . . . . . . . . . . 12 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝑠 ∈ (π΄πΏπ‘ž))
19910, 12, 13, 53, 64, 118, 65, 81, 174, 196, 197, 198, 134tglineinteq 28164 . . . . . . . . . . 11 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ 𝑠 = π‘Ÿ)
200199oveq1d 7427 . . . . . . . . . 10 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝑠 βˆ’ 𝐡) = (π‘Ÿ βˆ’ 𝐡))
201162, 200eqtr2d 2772 . . . . . . . . 9 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘Ÿ βˆ’ 𝐡) = (π‘Ÿ βˆ’ 𝐴))
202154ad2antrr 723 . . . . . . . . 9 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (𝐢 βˆ’ 𝐡) = (𝐢 βˆ’ 𝐴))
20310, 13, 12, 53, 55, 61, 62, 63, 64, 65, 11, 140, 144, 201, 202lncgr 28088 . . . . . . . 8 (((((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©)) β†’ (π‘₯ βˆ’ 𝐡) = (π‘₯ βˆ’ 𝐴))
20410, 11, 12, 63, 42, 52, 54, 117, 48, 80, 147, 157tgcgrxfr 28037 . . . . . . . 8 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ βˆƒπ‘  ∈ 𝑃 (𝑠 ∈ (π΄πΌπ‘ž) ∧ βŸ¨β€œπ΅π‘Ÿπ‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ΄π‘ π‘žβ€βŸ©))
205203, 204r19.29a 3161 . . . . . . 7 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ (π‘₯ βˆ’ 𝐡) = (π‘₯ βˆ’ 𝐴))
206 simprrl 778 . . . . . . . 8 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ π‘₯ ∈ (𝐴𝐼𝐡))
20710, 11, 12, 42, 48, 43, 52, 206tgbtwncom 28007 . . . . . . 7 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ π‘₯ ∈ (𝐡𝐼𝐴))
20810, 11, 12, 13, 14, 42, 43, 2, 48, 52, 205, 207ismir 28178 . . . . . 6 (((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) ∧ (π‘₯ ∈ 𝑃 ∧ (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))) β†’ 𝐡 = (π‘€β€˜π΄))
209 simplr 766 . . . . . . 7 ((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) β†’ π‘Ÿ ∈ 𝑃)
210 simprr 770 . . . . . . 7 ((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) β†’ π‘Ÿ ∈ (𝐡𝐼𝑝))
21110, 11, 12, 41, 59, 51, 116, 47, 209, 151, 210axtgpasch 27986 . . . . . 6 ((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) β†’ βˆƒπ‘₯ ∈ 𝑃 (π‘₯ ∈ (𝐴𝐼𝐡) ∧ π‘₯ ∈ (π‘ŸπΌπΆ)))
212208, 211reximddv 3170 . . . . 5 ((((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) ∧ π‘Ÿ ∈ 𝑃) ∧ (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝))) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
21310, 11, 12, 40, 58, 46, 115, 150tgbtwncom 28007 . . . . . 6 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ 𝐴 ∈ (𝑝𝐼𝐢))
21410, 11, 12, 40, 58, 50, 79, 95tgbtwncom 28007 . . . . . 6 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ 𝐡 ∈ (π‘žπΌπΆ))
21510, 11, 12, 40, 115, 79, 58, 46, 50, 213, 214axtgpasch 27986 . . . . 5 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ βˆƒπ‘Ÿ ∈ 𝑃 (π‘Ÿ ∈ (π΄πΌπ‘ž) ∧ π‘Ÿ ∈ (𝐡𝐼𝑝)))
216212, 215r19.29a 3161 . . . 4 ((((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) ∧ π‘ž ∈ 𝑃) ∧ (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝))) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
217 simplr 766 . . . . 5 ((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) β†’ 𝑝 ∈ 𝑃)
21810, 11, 12, 39, 57, 49, 45, 217axtgsegcon 27983 . . . 4 ((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) β†’ βˆƒπ‘ž ∈ 𝑃 (𝐡 ∈ (πΆπΌπ‘ž) ∧ (𝐡 βˆ’ π‘ž) = (𝐴 βˆ’ 𝑝)))
219216, 218r19.29a 3161 . . 3 ((((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝)) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
22010fvexi 6905 . . . . . 6 𝑃 ∈ V
221220a1i 11 . . . . 5 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 𝑃 ∈ V)
222221, 56, 44, 69nehash2 14440 . . . 4 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ 2 ≀ (β™―β€˜π‘ƒ))
22310, 11, 12, 38, 56, 44, 222tgbtwndiff 28025 . . 3 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ βˆƒπ‘ ∈ 𝑃 (𝐴 ∈ (𝐢𝐼𝑝) ∧ 𝐴 β‰  𝑝))
224219, 223r19.29a 3161 . 2 ((πœ‘ ∧ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡)) β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
22537, 224pm2.61dan 810 1 (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝑃 𝐡 = (π‘€β€˜π΄))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   ∨ wo 844   = wceq 1540   ∈ wcel 2105   β‰  wne 2939  βˆƒwrex 3069  Vcvv 3473   class class class wbr 5148  β€˜cfv 6543  (class class class)co 7412  βŸ¨β€œcs3 14798  Basecbs 17149  distcds 17211  TarskiGcstrkg 27946  Itvcitv 27952  LineGclng 27953  cgrGccgrg 28029  pInvGcmir 28171
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7728  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-1st 7978  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-oadd 8473  df-er 8706  df-pm 8826  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-dju 9899  df-card 9937  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-nn 12218  df-2 12280  df-3 12281  df-n0 12478  df-xnn0 12550  df-z 12564  df-uz 12828  df-fz 13490  df-fzo 13633  df-hash 14296  df-word 14470  df-concat 14526  df-s1 14551  df-s2 14804  df-s3 14805  df-trkgc 27967  df-trkgb 27968  df-trkgcb 27969  df-trkg 27972  df-cgrg 28030  df-mir 28172
This theorem is referenced by:  footexALT  28237  footex  28240  colperpexlem3  28251  opphllem  28254
  Copyright terms: Public domain W3C validator