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

Theorem midexlem 28714
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 28760 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 6906 . . . . . . . 8 (𝑥 = 𝐶 → (𝑆𝑥) = (𝑆𝐶))
42, 3eqtrid 2786 . . . . . . 7 (𝑥 = 𝐶𝑀 = (𝑆𝐶))
54fveq1d 6908 . . . . . 6 (𝑥 = 𝐶 → (𝑀𝐴) = ((𝑆𝐶)‘𝐴))
65rspceeqv 3644 . . . . 5 ((𝐶𝑃𝐵 = ((𝑆𝐶)‘𝐴)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
71, 6sylan 580 . . . 4 ((𝜑𝐵 = ((𝑆𝐶)‘𝐴)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
87adantlr 715 . . 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 2734 . . . . . . . 8 (𝑆𝐴) = (𝑆𝐴)
1710, 11, 12, 13, 14, 15, 9, 16mircinv 28690 . . . . . . 7 (𝜑 → ((𝑆𝐴)‘𝐴) = 𝐴)
1817adantr 480 . . . . . 6 ((𝜑𝐴 = 𝐵) → ((𝑆𝐴)‘𝐴) = 𝐴)
19 simpr 484 . . . . . 6 ((𝜑𝐴 = 𝐵) → 𝐴 = 𝐵)
2018, 19eqtr2d 2775 . . . . 5 ((𝜑𝐴 = 𝐵) → 𝐵 = ((𝑆𝐴)‘𝐴))
21 fveq2 6906 . . . . . . . 8 (𝑥 = 𝐴 → (𝑆𝑥) = (𝑆𝐴))
222, 21eqtrid 2786 . . . . . . 7 (𝑥 = 𝐴𝑀 = (𝑆𝐴))
2322fveq1d 6908 . . . . . 6 (𝑥 = 𝐴 → (𝑀𝐴) = ((𝑆𝐴)‘𝐴))
2423rspceeqv 3644 . . . . 5 ((𝐴𝑃𝐵 = ((𝑆𝐴)‘𝐴)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
259, 20, 24syl2an2r 685 . . . 4 ((𝜑𝐴 = 𝐵) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
2625adantlr 715 . . 3 (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐴 = 𝐵) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
2715adantr 480 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
28 eqid 2734 . . . 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 28710 . . 3 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐵 = ((𝑆𝐶)‘𝐴) ∨ 𝐴 = 𝐵))
378, 26, 36mpjaodan 960 . 2 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
3815adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
3938ad2antrr 726 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐺 ∈ TarskiG)
4039ad2antrr 726 . . . . . . . . 9 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐺 ∈ TarskiG)
4140ad2antrr 726 . . . . . . . 8 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐺 ∈ TarskiG)
4241adantr 480 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐺 ∈ TarskiG)
43 simprl 771 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥𝑃)
449adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴𝑃)
4544ad2antrr 726 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐴𝑃)
4645ad2antrr 726 . . . . . . . . 9 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐴𝑃)
4746ad2antrr 726 . . . . . . . 8 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴𝑃)
4847adantr 480 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴𝑃)
4930ad3antrrr 730 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐵𝑃)
5049ad2antrr 726 . . . . . . . . 9 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐵𝑃)
5150ad2antrr 726 . . . . . . . 8 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐵𝑃)
5251adantr 480 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵𝑃)
5342ad2antrr 726 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐺 ∈ TarskiG)
54 simpllr 776 . . . . . . . . . 10 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟𝑃)
5554ad2antrr 726 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟𝑃)
561adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶𝑃)
5756ad2antrr 726 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐶𝑃)
5857ad2antrr 726 . . . . . . . . . . . 12 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐶𝑃)
5958ad2antrr 726 . . . . . . . . . . 11 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐶𝑃)
6059adantr 480 . . . . . . . . . 10 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶𝑃)
6160ad2antrr 726 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶𝑃)
6243ad2antrr 726 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥𝑃)
63 eqid 2734 . . . . . . . . 9 (cgrG‘𝐺) = (cgrG‘𝐺)
6452ad2antrr 726 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵𝑃)
6548ad2antrr 726 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴𝑃)
66 simpr 484 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 = 𝐴)
6730adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵𝑃)
68 simpr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
6910, 12, 13, 38, 56, 44, 67, 68ncolne1 28647 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶𝐴)
7069ad7antr 738 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶𝐴)
7170ad2antrr 726 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶𝐴)
7271adantr 480 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐶𝐴)
7372necomd 2993 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐴𝐶)
7466, 73eqnetrd 3005 . . . . . . . . . 10 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟𝐶)
7553adantr 480 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝐺 ∈ TarskiG)
7655adantr 480 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟𝑃)
7765adantr 480 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝐴𝑃)
7861adantr 480 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝐶𝑃)
79 simplr 769 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝑞𝑃)
8079ad3antrrr 730 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑞𝑃)
8180ad2antrr 726 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝑃)
8281adantr 480 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑞𝑃)
8368ad9antr 742 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
8410, 13, 12, 53, 65, 64, 61, 83ncolrot2 28585 . . . . . . . . . . . . . . 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 28580 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
9190stoic1a 1768 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
9291ad9antr 742 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
9310, 12, 13, 53, 61, 64, 65, 92ncolne1 28647 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶𝐵)
9493necomd 2993 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵𝐶)
95 simprl 771 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐵 ∈ (𝐶𝐼𝑞))
9695ad3antrrr 730 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ (𝐶𝐼𝑞))
9796ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ (𝐶𝐼𝑞))
9810, 12, 13, 53, 61, 64, 81, 93, 97btwnlng3 28643 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐶𝐿𝐵))
9910, 12, 13, 53, 64, 61, 81, 94, 98lncom 28644 . . . . . . . . . . . . . . 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 7446 . . . . . . . . . . . . . . . . . . 19 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → (𝐶𝐼𝑞) = (𝐶𝐼𝐶))
106103, 105eleqtrd 2840 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶))
10710, 11, 12, 100, 101, 102, 106axtgbtwnid 28488 . . . . . . . . . . . . . . . . 17 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 = 𝐵)
10893adantr 480 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶𝐵)
109108neneqd 2942 . . . . . . . . . . . . . . . . 17 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → ¬ 𝐶 = 𝐵)
110107, 109pm2.65da 817 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝑞 = 𝐶)
111110neqned 2944 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝐶)
11210, 12, 13, 53, 64, 61, 65, 81, 84, 99, 111ncolncol 28668 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
11310, 13, 12, 53, 61, 65, 81, 112ncolcom 28583 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
114113adantr 480 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
115 simp-4r 784 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝑝𝑃)
116115ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑝𝑃)
117116adantr 480 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑝𝑃)
118117ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝𝑃)
119 simp-4r 784 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝)))
120119simprd 495 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 𝑞) = (𝐴 𝑝))
121120eqcomd 2740 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 𝑝) = (𝐵 𝑞))
122121ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 𝑝) = (𝐵 𝑞))
12310, 11, 12, 53, 65, 118, 64, 81, 122tgcgrcomlr 28502 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 𝐴) = (𝑞 𝐵))
124 simpllr 776 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝))
125124ad5antr 734 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝))
126125simprd 495 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴𝑝)
127126necomd 2993 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝𝐴)
12810, 11, 12, 53, 118, 65, 81, 64, 123, 127tgcgrneq 28505 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝐵)
12910, 12, 13, 53, 61, 64, 65, 81, 92, 98, 128ncolncol 28668 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
13010, 12, 13, 53, 81, 64, 65, 129ncolne2 28648 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝐴)
131130necomd 2993 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴𝑞)
132 simp-4r 784 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
133132simpld 494 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐼𝑞))
13410, 12, 13, 53, 65, 81, 55, 131, 133btwnlng1 28641 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐿𝑞))
13510, 12, 13, 53, 81, 65, 55, 130, 134lncom 28644 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑞𝐿𝐴))
136135adantr 480 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟 ∈ (𝑞𝐿𝐴))
137 simpr 484 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟𝐴)
13810, 12, 13, 75, 82, 77, 78, 76, 114, 136, 137ncolncol 28668 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → ¬ (𝑟 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
13910, 12, 13, 75, 76, 77, 78, 138ncolne2 28648 . . . . . . . . . 10 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟𝐶)
14074, 139pm2.61dane 3026 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟𝐶)
141 simpllr 776 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶))))
142141simprd 495 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
143142simprd 495 . . . . . . . . . 10 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ (𝑟𝐼𝐶))
14410, 13, 12, 53, 55, 62, 61, 143btwncolg3 28579 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 ∈ (𝑟𝐿𝑥) ∨ 𝑟 = 𝑥))
145 simplr 769 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠𝑃)
146 simplr 769 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
147146simprd 495 . . . . . . . . . . . 12 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝐵𝐼𝑝))
148147ad2antrr 726 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐼𝑝))
149 simprl 771 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐼𝑞))
150124simpld 494 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
151150ad2antrr 726 . . . . . . . . . . . . . . 15 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
152151adantr 480 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ (𝐶𝐼𝑝))
15334ad8antr 740 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 𝐴) = (𝐶 𝐵))
154153eqcomd 2740 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 𝐵) = (𝐶 𝐴))
15510, 11, 12, 42, 48, 52axtgcgrrflx 28484 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 𝐵) = (𝐵 𝐴))
15610, 11, 12, 42, 60, 48, 117, 60, 52, 80, 52, 48, 70, 152, 96, 153, 121, 154, 155axtg5seg 28487 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑝 𝐵) = (𝑞 𝐴))
15710, 11, 12, 42, 117, 52, 80, 48, 156tgcgrcomlr 28502 . . . . . . . . . . . 12 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 𝑝) = (𝐴 𝑞))
158157ad2antrr 726 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝑝) = (𝐴 𝑞))
159 simprr 773 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)
16010, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159cgr3simp2 28543 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝑝) = (𝑠 𝑞))
16110, 11, 12, 53, 64, 65axtgcgrrflx 28484 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝐴) = (𝐴 𝐵))
16210, 11, 12, 53, 64, 55, 118, 65, 65, 145, 81, 64, 148, 149, 158, 160, 161, 123tgifscgr 28530 . . . . . . . . . 10 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝐴) = (𝑠 𝐵))
163 simp-10l 795 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝜑)
164125simpld 494 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ (𝐶𝐼𝑝))
16510, 12, 13, 53, 61, 65, 118, 71, 164btwnlng3 28643 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ (𝐶𝐿𝐴))
16610, 12, 13, 53, 61, 65, 64, 118, 83, 165, 127ncolncol 28668 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
16715ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐺 ∈ TarskiG)
168 simplr 769 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝑝𝑃)
1699ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐴𝑃)
17030ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐵𝑃)
171 simpr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
17210, 13, 12, 167, 168, 169, 170, 171colrot1 28581 . . . . . . . . . . . . . 14 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
173172stoic1a 1768 . . . . . . . . . . . . 13 (((𝜑𝑝𝑃) ∧ ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
174163, 118, 166, 173syl21anc 838 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
17510, 12, 13, 53, 118, 65, 64, 166ncolne2 28648 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝𝐵)
176175necomd 2993 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵𝑝)
177176neneqd 2942 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝐵 = 𝑝)
17810, 13, 12, 53, 65, 81, 55, 133btwncolg1 28577 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐿𝑞) ∨ 𝐴 = 𝑞))
17910, 11, 12, 53, 55, 65, 145, 64, 162tgcgrcomlr 28502 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 𝑟) = (𝐵 𝑠))
180120ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝑞) = (𝐴 𝑝))
18110, 11, 12, 53, 118, 81axtgcgrrflx 28484 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 𝑞) = (𝑞 𝑝))
18210, 11, 12, 53, 64, 55, 118, 81, 65, 145, 81, 118, 148, 149, 158, 160, 180, 181tgifscgr 28530 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝑞) = (𝑠 𝑝))
18310, 11, 12, 53, 65, 145, 81, 149tgbtwncom 28510 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝑞𝐼𝐴))
18410, 11, 12, 42, 52, 54, 117, 147tgbtwncom 28510 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝑝𝐼𝐵))
185184ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑝𝐼𝐵))
186160eqcomd 2740 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 𝑞) = (𝑟 𝑝))
18710, 11, 12, 53, 145, 81, 55, 118, 186tgcgrcomlr 28502 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 𝑠) = (𝑝 𝑟))
18810, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159cgr3simp1 28542 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝑟) = (𝐴 𝑠))
189188eqcomd 2740 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 𝑠) = (𝐵 𝑟))
19010, 11, 12, 53, 65, 145, 64, 55, 189tgcgrcomlr 28502 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 𝐴) = (𝑟 𝐵))
19110, 11, 12, 53, 81, 145, 65, 118, 55, 64, 183, 185, 187, 190tgcgrextend 28507 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 𝐴) = (𝑝 𝐵))
19210, 11, 63, 53, 65, 55, 81, 64, 145, 118, 179, 182, 191trgcgr 28538 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐴𝑟𝑞”⟩(cgrG‘𝐺)⟨“𝐵𝑠𝑝”⟩)
19310, 13, 12, 53, 65, 55, 81, 63, 64, 145, 118, 178, 192lnxfr 28588 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 ∈ (𝐵𝐿𝑝) ∨ 𝐵 = 𝑝))
194193orcomd 871 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 = 𝑝𝑠 ∈ (𝐵𝐿𝑝)))
195194ord 864 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (¬ 𝐵 = 𝑝𝑠 ∈ (𝐵𝐿𝑝)))
196177, 195mpd 15 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐵𝐿𝑝))
19710, 12, 13, 53, 64, 118, 55, 176, 148btwnlng1 28641 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐿𝑝))
19810, 12, 13, 53, 65, 81, 145, 131, 149btwnlng1 28641 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐿𝑞))
19910, 12, 13, 53, 64, 118, 65, 81, 174, 196, 197, 198, 134tglineinteq 28667 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 = 𝑟)
200199oveq1d 7445 . . . . . . . . . 10 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 𝐵) = (𝑟 𝐵))
201162, 200eqtr2d 2775 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝐵) = (𝑟 𝐴))
202154ad2antrr 726 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 𝐵) = (𝐶 𝐴))
20310, 13, 12, 53, 55, 61, 62, 63, 64, 65, 11, 140, 144, 201, 202lncgr 28591 . . . . . . . 8 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 𝐵) = (𝑥 𝐴))
20410, 11, 12, 63, 42, 52, 54, 117, 48, 80, 147, 157tgcgrxfr 28540 . . . . . . . 8 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → ∃𝑠𝑃 (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩))
205203, 204r19.29a 3159 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑥 𝐵) = (𝑥 𝐴))
206 simprrl 781 . . . . . . . 8 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐴𝐼𝐵))
20710, 11, 12, 42, 48, 43, 52, 206tgbtwncom 28510 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐵𝐼𝐴))
20810, 11, 12, 13, 14, 42, 43, 2, 48, 52, 205, 207ismir 28681 . . . . . 6 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 = (𝑀𝐴))
209 simplr 769 . . . . . . 7 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟𝑃)
210 simprr 773 . . . . . . 7 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ (𝐵𝐼𝑝))
21110, 11, 12, 41, 59, 51, 116, 47, 209, 151, 210axtgpasch 28489 . . . . . 6 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
212208, 211reximddv 3168 . . . . 5 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
21310, 11, 12, 40, 58, 46, 115, 150tgbtwncom 28510 . . . . . 6 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐴 ∈ (𝑝𝐼𝐶))
21410, 11, 12, 40, 58, 50, 79, 95tgbtwncom 28510 . . . . . 6 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐵 ∈ (𝑞𝐼𝐶))
21510, 11, 12, 40, 115, 79, 58, 46, 50, 213, 214axtgpasch 28489 . . . . 5 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → ∃𝑟𝑃 (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
216212, 215r19.29a 3159 . . . 4 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
217 simplr 769 . . . . 5 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝑝𝑃)
21810, 11, 12, 39, 57, 49, 45, 217axtgsegcon 28486 . . . 4 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → ∃𝑞𝑃 (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝)))
219216, 218r19.29a 3159 . . 3 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
22010fvexi 6920 . . . . . 6 𝑃 ∈ V
221220a1i 11 . . . . 5 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝑃 ∈ V)
222221, 56, 44, 69nehash2 14509 . . . 4 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 2 ≤ (♯‘𝑃))
22310, 11, 12, 38, 56, 44, 222tgbtwndiff 28528 . . 3 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑝𝑃 (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝))
224219, 223r19.29a 3159 . 2 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
22537, 224pm2.61dan 813 1 (𝜑 → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 847   = wceq 1536  wcel 2105  wne 2937  wrex 3067  Vcvv 3477   class class class wbr 5147  cfv 6562  (class class class)co 7430  ⟨“cs3 14877  Basecbs 17244  distcds 17306  TarskiGcstrkg 28449  Itvcitv 28455  LineGclng 28456  cgrGccgrg 28532  pInvGcmir 28674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-er 8743  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-fz 13544  df-fzo 13691  df-hash 14366  df-word 14549  df-concat 14605  df-s1 14630  df-s2 14883  df-s3 14884  df-trkgc 28470  df-trkgb 28471  df-trkgcb 28472  df-trkg 28475  df-cgrg 28533  df-mir 28675
This theorem is referenced by:  footexALT  28740  footex  28743  colperpexlem3  28754  opphllem  28757
  Copyright terms: Public domain W3C validator