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

Theorem midexlem 25786
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 25829 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 . . . . . . . . 9 𝑀 = (𝑆𝑥)
3 fveq2 6352 . . . . . . . . 9 (𝑥 = 𝐶 → (𝑆𝑥) = (𝑆𝐶))
42, 3syl5eq 2806 . . . . . . . 8 (𝑥 = 𝐶𝑀 = (𝑆𝐶))
54fveq1d 6354 . . . . . . 7 (𝑥 = 𝐶 → (𝑀𝐴) = ((𝑆𝐶)‘𝐴))
65eqeq2d 2770 . . . . . 6 (𝑥 = 𝐶 → (𝐵 = (𝑀𝐴) ↔ 𝐵 = ((𝑆𝐶)‘𝐴)))
76rspcev 3449 . . . . 5 ((𝐶𝑃𝐵 = ((𝑆𝐶)‘𝐴)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
81, 7sylan 489 . . . 4 ((𝜑𝐵 = ((𝑆𝐶)‘𝐴)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
98adantlr 753 . . 3 (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐵 = ((𝑆𝐶)‘𝐴)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
10 midexlem.a . . . . . 6 (𝜑𝐴𝑃)
1110adantr 472 . . . . 5 ((𝜑𝐴 = 𝐵) → 𝐴𝑃)
12 mirval.p . . . . . . . 8 𝑃 = (Base‘𝐺)
13 mirval.d . . . . . . . 8 = (dist‘𝐺)
14 mirval.i . . . . . . . 8 𝐼 = (Itv‘𝐺)
15 mirval.l . . . . . . . 8 𝐿 = (LineG‘𝐺)
16 mirval.s . . . . . . . 8 𝑆 = (pInvG‘𝐺)
17 mirval.g . . . . . . . 8 (𝜑𝐺 ∈ TarskiG)
18 eqid 2760 . . . . . . . 8 (𝑆𝐴) = (𝑆𝐴)
1912, 13, 14, 15, 16, 17, 10, 18mircinv 25762 . . . . . . 7 (𝜑 → ((𝑆𝐴)‘𝐴) = 𝐴)
2019adantr 472 . . . . . 6 ((𝜑𝐴 = 𝐵) → ((𝑆𝐴)‘𝐴) = 𝐴)
21 simpr 479 . . . . . 6 ((𝜑𝐴 = 𝐵) → 𝐴 = 𝐵)
2220, 21eqtr2d 2795 . . . . 5 ((𝜑𝐴 = 𝐵) → 𝐵 = ((𝑆𝐴)‘𝐴))
23 fveq2 6352 . . . . . . . . 9 (𝑥 = 𝐴 → (𝑆𝑥) = (𝑆𝐴))
242, 23syl5eq 2806 . . . . . . . 8 (𝑥 = 𝐴𝑀 = (𝑆𝐴))
2524fveq1d 6354 . . . . . . 7 (𝑥 = 𝐴 → (𝑀𝐴) = ((𝑆𝐴)‘𝐴))
2625eqeq2d 2770 . . . . . 6 (𝑥 = 𝐴 → (𝐵 = (𝑀𝐴) ↔ 𝐵 = ((𝑆𝐴)‘𝐴)))
2726rspcev 3449 . . . . 5 ((𝐴𝑃𝐵 = ((𝑆𝐴)‘𝐴)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
2811, 22, 27syl2anc 696 . . . 4 ((𝜑𝐴 = 𝐵) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
2928adantlr 753 . . 3 (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐴 = 𝐵) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
3017adantr 472 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
31 eqid 2760 . . . 4 (𝑆𝐶) = (𝑆𝐶)
3210adantr 472 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴𝑃)
33 midexlem.b . . . . 5 (𝜑𝐵𝑃)
3433adantr 472 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵𝑃)
351adantr 472 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶𝑃)
36 simpr 479 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
37 midexlem.1 . . . . 5 (𝜑 → (𝐶 𝐴) = (𝐶 𝐵))
3837adantr 472 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 𝐴) = (𝐶 𝐵))
3912, 13, 14, 15, 16, 30, 31, 32, 34, 35, 36, 38colmid 25782 . . 3 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐵 = ((𝑆𝐶)‘𝐴) ∨ 𝐴 = 𝐵))
409, 29, 39mpjaodan 862 . 2 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
4117adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
4241ad2antrr 764 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐺 ∈ TarskiG)
4342ad2antrr 764 . . . . . . . . 9 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐺 ∈ TarskiG)
4443ad2antrr 764 . . . . . . . 8 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐺 ∈ TarskiG)
4544adantr 472 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐺 ∈ TarskiG)
46 simprl 811 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥𝑃)
4710adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴𝑃)
4847ad2antrr 764 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐴𝑃)
4948ad2antrr 764 . . . . . . . . 9 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐴𝑃)
5049ad2antrr 764 . . . . . . . 8 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴𝑃)
5150adantr 472 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴𝑃)
5233ad3antrrr 768 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐵𝑃)
5352ad2antrr 764 . . . . . . . . 9 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐵𝑃)
5453ad2antrr 764 . . . . . . . 8 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐵𝑃)
5554adantr 472 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵𝑃)
5645ad2antrr 764 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐺 ∈ TarskiG)
57 simpllr 817 . . . . . . . . . 10 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟𝑃)
5857ad2antrr 764 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟𝑃)
591adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶𝑃)
6059ad2antrr 764 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐶𝑃)
6160ad2antrr 764 . . . . . . . . . . . 12 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐶𝑃)
6261ad2antrr 764 . . . . . . . . . . 11 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐶𝑃)
6362adantr 472 . . . . . . . . . 10 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶𝑃)
6463ad2antrr 764 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶𝑃)
6546ad2antrr 764 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥𝑃)
66 eqid 2760 . . . . . . . . 9 (cgrG‘𝐺) = (cgrG‘𝐺)
6755ad2antrr 764 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵𝑃)
6851ad2antrr 764 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴𝑃)
69 simpr 479 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 = 𝐴)
7033adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵𝑃)
71 simpr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
7212, 14, 15, 41, 59, 47, 70, 71ncolne1 25719 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶𝐴)
7372ad7antr 783 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶𝐴)
7473ad2antrr 764 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶𝐴)
7574adantr 472 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐶𝐴)
7675necomd 2987 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐴𝐶)
7769, 76eqnetrd 2999 . . . . . . . . . 10 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟𝐶)
7856adantr 472 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝐺 ∈ TarskiG)
7958adantr 472 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟𝑃)
8068adantr 472 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝐴𝑃)
8164adantr 472 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝐶𝑃)
82 simplr 809 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝑞𝑃)
8382ad3antrrr 768 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑞𝑃)
8483ad2antrr 764 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝑃)
8584adantr 472 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑞𝑃)
8671ad9antr 791 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
8712, 15, 14, 56, 68, 67, 64, 86ncolrot2 25657 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
8817adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐺 ∈ TarskiG)
8933adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐵𝑃)
9010adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐴𝑃)
911adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐶𝑃)
92 simpr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
9312, 15, 14, 88, 89, 90, 91, 92colcom 25652 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
9493stoic1a 1846 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
9594ad9antr 791 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
9612, 14, 15, 56, 64, 67, 68, 95ncolne1 25719 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶𝐵)
9796necomd 2987 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵𝐶)
98 simprl 811 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐵 ∈ (𝐶𝐼𝑞))
9998ad3antrrr 768 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ (𝐶𝐼𝑞))
10099ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ (𝐶𝐼𝑞))
10112, 14, 15, 56, 64, 67, 84, 96, 100btwnlng3 25715 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐶𝐿𝐵))
10212, 14, 15, 56, 67, 64, 84, 97, 101lncom 25716 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐵𝐿𝐶))
10356adantr 472 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐺 ∈ TarskiG)
10464adantr 472 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶𝑃)
10567adantr 472 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵𝑃)
106100adantr 472 . . . . . . . . . . . . . . . . . . 19 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝑞))
107 simpr 479 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝑞 = 𝐶)
108107oveq2d 6829 . . . . . . . . . . . . . . . . . . 19 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → (𝐶𝐼𝑞) = (𝐶𝐼𝐶))
109106, 108eleqtrd 2841 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶))
11012, 13, 14, 103, 104, 105, 109axtgbtwnid 25564 . . . . . . . . . . . . . . . . 17 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 = 𝐵)
11196adantr 472 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶𝐵)
112111neneqd 2937 . . . . . . . . . . . . . . . . 17 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → ¬ 𝐶 = 𝐵)
113110, 112pm2.65da 601 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝑞 = 𝐶)
114113neqned 2939 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝐶)
11512, 14, 15, 56, 67, 64, 68, 84, 87, 102, 114ncolncol 25740 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
11612, 15, 14, 56, 64, 68, 84, 115ncolcom 25655 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
117116adantr 472 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
118 simp-4r 827 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝑝𝑃)
119118ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑝𝑃)
120119adantr 472 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑝𝑃)
121120ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝𝑃)
122 simp-4r 827 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝)))
123122simprd 482 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 𝑞) = (𝐴 𝑝))
124123eqcomd 2766 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 𝑝) = (𝐵 𝑞))
125124ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 𝑝) = (𝐵 𝑞))
12612, 13, 14, 56, 68, 121, 67, 84, 125tgcgrcomlr 25574 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 𝐴) = (𝑞 𝐵))
127 simpllr 817 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝))
128127ad5antr 775 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝))
129128simprd 482 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴𝑝)
130129necomd 2987 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝𝐴)
13112, 13, 14, 56, 121, 68, 84, 67, 126, 130tgcgrneq 25577 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝐵)
13212, 14, 15, 56, 64, 67, 68, 84, 95, 101, 131ncolncol 25740 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
13312, 14, 15, 56, 84, 67, 68, 132ncolne2 25720 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝐴)
134133necomd 2987 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴𝑞)
135 simp-4r 827 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
136135simpld 477 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐼𝑞))
13712, 14, 15, 56, 68, 84, 58, 134, 136btwnlng1 25713 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐿𝑞))
13812, 14, 15, 56, 84, 68, 58, 133, 137lncom 25716 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑞𝐿𝐴))
139138adantr 472 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟 ∈ (𝑞𝐿𝐴))
140 simpr 479 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟𝐴)
14112, 14, 15, 78, 85, 80, 81, 79, 117, 139, 140ncolncol 25740 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → ¬ (𝑟 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
14212, 14, 15, 78, 79, 80, 81, 141ncolne2 25720 . . . . . . . . . 10 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟𝐶)
14377, 142pm2.61dane 3019 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟𝐶)
144 simpllr 817 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶))))
145144simprd 482 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
146145simprd 482 . . . . . . . . . 10 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ (𝑟𝐼𝐶))
14712, 15, 14, 56, 58, 65, 64, 146btwncolg3 25651 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 ∈ (𝑟𝐿𝑥) ∨ 𝑟 = 𝑥))
148 simplr 809 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠𝑃)
149 simplr 809 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
150149simprd 482 . . . . . . . . . . . 12 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝐵𝐼𝑝))
151150ad2antrr 764 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐼𝑝))
152 simprl 811 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐼𝑞))
153127simpld 477 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
154153ad2antrr 764 . . . . . . . . . . . . . . 15 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
155154adantr 472 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ (𝐶𝐼𝑝))
15637ad8antr 787 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 𝐴) = (𝐶 𝐵))
157156eqcomd 2766 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 𝐵) = (𝐶 𝐴))
15812, 13, 14, 45, 51, 55axtgcgrrflx 25560 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 𝐵) = (𝐵 𝐴))
15912, 13, 14, 45, 63, 51, 120, 63, 55, 83, 55, 51, 73, 155, 99, 156, 124, 157, 158axtg5seg 25563 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑝 𝐵) = (𝑞 𝐴))
16012, 13, 14, 45, 120, 55, 83, 51, 159tgcgrcomlr 25574 . . . . . . . . . . . 12 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 𝑝) = (𝐴 𝑞))
161160ad2antrr 764 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝑝) = (𝐴 𝑞))
162 simprr 813 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)
16312, 13, 14, 66, 56, 67, 58, 121, 68, 148, 84, 162cgr3simp2 25615 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝑝) = (𝑠 𝑞))
16412, 13, 14, 56, 67, 68axtgcgrrflx 25560 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝐴) = (𝐴 𝐵))
16512, 13, 14, 56, 67, 58, 121, 68, 68, 148, 84, 67, 151, 152, 161, 163, 164, 126tgifscgr 25602 . . . . . . . . . 10 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝐴) = (𝑠 𝐵))
166 simp-10l 849 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝜑)
167128simpld 477 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ (𝐶𝐼𝑝))
16812, 14, 15, 56, 64, 68, 121, 74, 167btwnlng3 25715 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ (𝐶𝐿𝐴))
16912, 14, 15, 56, 64, 68, 67, 121, 86, 168, 130ncolncol 25740 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
17017ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐺 ∈ TarskiG)
171 simplr 809 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝑝𝑃)
17210ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐴𝑃)
17333ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐵𝑃)
174 simpr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
17512, 15, 14, 170, 171, 172, 173, 174colrot1 25653 . . . . . . . . . . . . . 14 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
176175stoic1a 1846 . . . . . . . . . . . . 13 (((𝜑𝑝𝑃) ∧ ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
177166, 121, 169, 176syl21anc 1476 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
17812, 14, 15, 56, 121, 68, 67, 169ncolne2 25720 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝𝐵)
179178necomd 2987 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵𝑝)
180179neneqd 2937 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝐵 = 𝑝)
18112, 15, 14, 56, 68, 84, 58, 136btwncolg1 25649 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐿𝑞) ∨ 𝐴 = 𝑞))
18212, 13, 14, 56, 58, 68, 148, 67, 165tgcgrcomlr 25574 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 𝑟) = (𝐵 𝑠))
183123ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝑞) = (𝐴 𝑝))
18412, 13, 14, 56, 121, 84axtgcgrrflx 25560 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 𝑞) = (𝑞 𝑝))
18512, 13, 14, 56, 67, 58, 121, 84, 68, 148, 84, 121, 151, 152, 161, 163, 183, 184tgifscgr 25602 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝑞) = (𝑠 𝑝))
18612, 13, 14, 56, 68, 148, 84, 152tgbtwncom 25582 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝑞𝐼𝐴))
18712, 13, 14, 45, 55, 57, 120, 150tgbtwncom 25582 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝑝𝐼𝐵))
188187ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑝𝐼𝐵))
189163eqcomd 2766 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 𝑞) = (𝑟 𝑝))
19012, 13, 14, 56, 148, 84, 58, 121, 189tgcgrcomlr 25574 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 𝑠) = (𝑝 𝑟))
19112, 13, 14, 66, 56, 67, 58, 121, 68, 148, 84, 162cgr3simp1 25614 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝑟) = (𝐴 𝑠))
192191eqcomd 2766 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 𝑠) = (𝐵 𝑟))
19312, 13, 14, 56, 68, 148, 67, 58, 192tgcgrcomlr 25574 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 𝐴) = (𝑟 𝐵))
19412, 13, 14, 56, 84, 148, 68, 121, 58, 67, 186, 188, 190, 193tgcgrextend 25579 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 𝐴) = (𝑝 𝐵))
19512, 13, 66, 56, 68, 58, 84, 67, 148, 121, 182, 185, 194trgcgr 25610 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐴𝑟𝑞”⟩(cgrG‘𝐺)⟨“𝐵𝑠𝑝”⟩)
19612, 15, 14, 56, 68, 58, 84, 66, 67, 148, 121, 181, 195lnxfr 25660 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 ∈ (𝐵𝐿𝑝) ∨ 𝐵 = 𝑝))
197196orcomd 402 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 = 𝑝𝑠 ∈ (𝐵𝐿𝑝)))
198197ord 391 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (¬ 𝐵 = 𝑝𝑠 ∈ (𝐵𝐿𝑝)))
199180, 198mpd 15 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐵𝐿𝑝))
20012, 14, 15, 56, 67, 121, 58, 179, 151btwnlng1 25713 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐿𝑝))
20112, 14, 15, 56, 68, 84, 148, 134, 152btwnlng1 25713 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐿𝑞))
20212, 14, 15, 56, 67, 121, 68, 84, 177, 199, 200, 201, 137tglineinteq 25739 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 = 𝑟)
203202oveq1d 6828 . . . . . . . . . 10 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 𝐵) = (𝑟 𝐵))
204165, 203eqtr2d 2795 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝐵) = (𝑟 𝐴))
205157ad2antrr 764 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 𝐵) = (𝐶 𝐴))
20612, 15, 14, 56, 58, 64, 65, 66, 67, 68, 13, 143, 147, 204, 205lncgr 25663 . . . . . . . 8 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 𝐵) = (𝑥 𝐴))
20712, 13, 14, 66, 45, 55, 57, 120, 51, 83, 150, 160tgcgrxfr 25612 . . . . . . . 8 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → ∃𝑠𝑃 (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩))
208206, 207r19.29a 3216 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑥 𝐵) = (𝑥 𝐴))
209 simprrl 823 . . . . . . . 8 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐴𝐼𝐵))
21012, 13, 14, 45, 51, 46, 55, 209tgbtwncom 25582 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐵𝐼𝐴))
21112, 13, 14, 15, 16, 45, 46, 2, 51, 55, 208, 210ismir 25753 . . . . . 6 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 = (𝑀𝐴))
212 simplr 809 . . . . . . 7 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟𝑃)
213 simprr 813 . . . . . . 7 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ (𝐵𝐼𝑝))
21412, 13, 14, 44, 62, 54, 119, 50, 212, 154, 213axtgpasch 25565 . . . . . 6 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
215211, 214reximddv 3156 . . . . 5 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
21612, 13, 14, 43, 61, 49, 118, 153tgbtwncom 25582 . . . . . 6 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐴 ∈ (𝑝𝐼𝐶))
21712, 13, 14, 43, 61, 53, 82, 98tgbtwncom 25582 . . . . . 6 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐵 ∈ (𝑞𝐼𝐶))
21812, 13, 14, 43, 118, 82, 61, 49, 53, 216, 217axtgpasch 25565 . . . . 5 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → ∃𝑟𝑃 (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
219215, 218r19.29a 3216 . . . 4 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
220 simplr 809 . . . . 5 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝑝𝑃)
22112, 13, 14, 42, 60, 52, 48, 220axtgsegcon 25562 . . . 4 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → ∃𝑞𝑃 (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝)))
222219, 221r19.29a 3216 . . 3 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
223 fvex 6362 . . . . . . 7 (Base‘𝐺) ∈ V
22412, 223eqeltri 2835 . . . . . 6 𝑃 ∈ V
225224a1i 11 . . . . 5 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝑃 ∈ V)
226225, 59, 47, 72nehash2 13448 . . . 4 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 2 ≤ (♯‘𝑃))
22712, 13, 14, 41, 59, 47, 226tgbtwndiff 25600 . . 3 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑝𝑃 (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝))
228222, 227r19.29a 3216 . 2 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
22940, 228pm2.61dan 867 1 (𝜑 → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383   = wceq 1632  wcel 2139  wne 2932  wrex 3051  Vcvv 3340   class class class wbr 4804  cfv 6049  (class class class)co 6813  ⟨“cs3 13787  Basecbs 16059  distcds 16152  TarskiGcstrkg 25528  Itvcitv 25534  LineGclng 25535  cgrGccgrg 25604  pInvGcmir 25746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-pm 8026  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-xnn0 11556  df-z 11570  df-uz 11880  df-fz 12520  df-fzo 12660  df-hash 13312  df-word 13485  df-concat 13487  df-s1 13488  df-s2 13793  df-s3 13794  df-trkgc 25546  df-trkgb 25547  df-trkgcb 25548  df-trkg 25551  df-cgrg 25605  df-mir 25747
This theorem is referenced by:  footex  25812  colperpexlem3  25823  opphllem  25826
  Copyright terms: Public domain W3C validator