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

Theorem midexlem 27634
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 27680 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 6842 . . . . . . . 8 (𝑥 = 𝐶 → (𝑆𝑥) = (𝑆𝐶))
42, 3eqtrid 2788 . . . . . . 7 (𝑥 = 𝐶𝑀 = (𝑆𝐶))
54fveq1d 6844 . . . . . 6 (𝑥 = 𝐶 → (𝑀𝐴) = ((𝑆𝐶)‘𝐴))
65rspceeqv 3595 . . . . 5 ((𝐶𝑃𝐵 = ((𝑆𝐶)‘𝐴)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
71, 6sylan 580 . . . 4 ((𝜑𝐵 = ((𝑆𝐶)‘𝐴)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
87adantlr 713 . . 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 2736 . . . . . . . 8 (𝑆𝐴) = (𝑆𝐴)
1710, 11, 12, 13, 14, 15, 9, 16mircinv 27610 . . . . . . 7 (𝜑 → ((𝑆𝐴)‘𝐴) = 𝐴)
1817adantr 481 . . . . . 6 ((𝜑𝐴 = 𝐵) → ((𝑆𝐴)‘𝐴) = 𝐴)
19 simpr 485 . . . . . 6 ((𝜑𝐴 = 𝐵) → 𝐴 = 𝐵)
2018, 19eqtr2d 2777 . . . . 5 ((𝜑𝐴 = 𝐵) → 𝐵 = ((𝑆𝐴)‘𝐴))
21 fveq2 6842 . . . . . . . 8 (𝑥 = 𝐴 → (𝑆𝑥) = (𝑆𝐴))
222, 21eqtrid 2788 . . . . . . 7 (𝑥 = 𝐴𝑀 = (𝑆𝐴))
2322fveq1d 6844 . . . . . 6 (𝑥 = 𝐴 → (𝑀𝐴) = ((𝑆𝐴)‘𝐴))
2423rspceeqv 3595 . . . . 5 ((𝐴𝑃𝐵 = ((𝑆𝐴)‘𝐴)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
259, 20, 24syl2an2r 683 . . . 4 ((𝜑𝐴 = 𝐵) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
2625adantlr 713 . . 3 (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐴 = 𝐵) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
2715adantr 481 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
28 eqid 2736 . . . 4 (𝑆𝐶) = (𝑆𝐶)
299adantr 481 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴𝑃)
30 midexlem.b . . . . 5 (𝜑𝐵𝑃)
3130adantr 481 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵𝑃)
321adantr 481 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶𝑃)
33 simpr 485 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
34 midexlem.1 . . . . 5 (𝜑 → (𝐶 𝐴) = (𝐶 𝐵))
3534adantr 481 . . . 4 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 𝐴) = (𝐶 𝐵))
3610, 11, 12, 13, 14, 27, 28, 29, 31, 32, 33, 35colmid 27630 . . 3 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐵 = ((𝑆𝐶)‘𝐴) ∨ 𝐴 = 𝐵))
378, 26, 36mpjaodan 957 . 2 ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
3815adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
3938ad2antrr 724 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐺 ∈ TarskiG)
4039ad2antrr 724 . . . . . . . . 9 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐺 ∈ TarskiG)
4140ad2antrr 724 . . . . . . . 8 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐺 ∈ TarskiG)
4241adantr 481 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐺 ∈ TarskiG)
43 simprl 769 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥𝑃)
449adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴𝑃)
4544ad2antrr 724 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐴𝑃)
4645ad2antrr 724 . . . . . . . . 9 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐴𝑃)
4746ad2antrr 724 . . . . . . . 8 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴𝑃)
4847adantr 481 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴𝑃)
4930ad3antrrr 728 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐵𝑃)
5049ad2antrr 724 . . . . . . . . 9 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐵𝑃)
5150ad2antrr 724 . . . . . . . 8 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐵𝑃)
5251adantr 481 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵𝑃)
5342ad2antrr 724 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐺 ∈ TarskiG)
54 simpllr 774 . . . . . . . . . 10 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟𝑃)
5554ad2antrr 724 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟𝑃)
561adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶𝑃)
5756ad2antrr 724 . . . . . . . . . . . . 13 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝐶𝑃)
5857ad2antrr 724 . . . . . . . . . . . 12 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐶𝑃)
5958ad2antrr 724 . . . . . . . . . . 11 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐶𝑃)
6059adantr 481 . . . . . . . . . 10 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶𝑃)
6160ad2antrr 724 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶𝑃)
6243ad2antrr 724 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥𝑃)
63 eqid 2736 . . . . . . . . 9 (cgrG‘𝐺) = (cgrG‘𝐺)
6452ad2antrr 724 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵𝑃)
6548ad2antrr 724 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴𝑃)
66 simpr 485 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 = 𝐴)
6730adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵𝑃)
68 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
6910, 12, 13, 38, 56, 44, 67, 68ncolne1 27567 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶𝐴)
7069ad7antr 736 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶𝐴)
7170ad2antrr 724 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶𝐴)
7271adantr 481 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐶𝐴)
7372necomd 2999 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐴𝐶)
7466, 73eqnetrd 3011 . . . . . . . . . 10 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟𝐶)
7553adantr 481 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝐺 ∈ TarskiG)
7655adantr 481 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟𝑃)
7765adantr 481 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝐴𝑃)
7861adantr 481 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝐶𝑃)
79 simplr 767 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝑞𝑃)
8079ad3antrrr 728 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑞𝑃)
8180ad2antrr 724 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝑃)
8281adantr 481 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑞𝑃)
8368ad9antr 740 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
8410, 13, 12, 53, 65, 64, 61, 83ncolrot2 27505 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
8515adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐺 ∈ TarskiG)
8630adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐵𝑃)
879adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐴𝑃)
881adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐶𝑃)
89 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
9010, 13, 12, 85, 86, 87, 88, 89colcom 27500 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
9190stoic1a 1774 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
9291ad9antr 740 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
9310, 12, 13, 53, 61, 64, 65, 92ncolne1 27567 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶𝐵)
9493necomd 2999 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵𝐶)
95 simprl 769 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐵 ∈ (𝐶𝐼𝑞))
9695ad3antrrr 728 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ (𝐶𝐼𝑞))
9796ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ (𝐶𝐼𝑞))
9810, 12, 13, 53, 61, 64, 81, 93, 97btwnlng3 27563 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐶𝐿𝐵))
9910, 12, 13, 53, 64, 61, 81, 94, 98lncom 27564 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐵𝐿𝐶))
10053adantr 481 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐺 ∈ TarskiG)
10161adantr 481 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶𝑃)
10264adantr 481 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵𝑃)
10397adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝑞))
104 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝑞 = 𝐶)
105104oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → (𝐶𝐼𝑞) = (𝐶𝐼𝐶))
106103, 105eleqtrd 2840 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶))
10710, 11, 12, 100, 101, 102, 106axtgbtwnid 27408 . . . . . . . . . . . . . . . . 17 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 = 𝐵)
10893adantr 481 . . . . . . . . . . . . . . . . . 18 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶𝐵)
109108neneqd 2948 . . . . . . . . . . . . . . . . 17 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → ¬ 𝐶 = 𝐵)
110107, 109pm2.65da 815 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝑞 = 𝐶)
111110neqned 2950 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝐶)
11210, 12, 13, 53, 64, 61, 65, 81, 84, 99, 111ncolncol 27588 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
11310, 13, 12, 53, 61, 65, 81, 112ncolcom 27503 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
114113adantr 481 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
115 simp-4r 782 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝑝𝑃)
116115ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑝𝑃)
117116adantr 481 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑝𝑃)
118117ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝𝑃)
119 simp-4r 782 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝)))
120119simprd 496 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 𝑞) = (𝐴 𝑝))
121120eqcomd 2742 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 𝑝) = (𝐵 𝑞))
122121ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 𝑝) = (𝐵 𝑞))
12310, 11, 12, 53, 65, 118, 64, 81, 122tgcgrcomlr 27422 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 𝐴) = (𝑞 𝐵))
124 simpllr 774 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝))
125124ad5antr 732 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝))
126125simprd 496 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴𝑝)
127126necomd 2999 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝𝐴)
12810, 11, 12, 53, 118, 65, 81, 64, 123, 127tgcgrneq 27425 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝐵)
12910, 12, 13, 53, 61, 64, 65, 81, 92, 98, 128ncolncol 27588 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
13010, 12, 13, 53, 81, 64, 65, 129ncolne2 27568 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞𝐴)
131130necomd 2999 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴𝑞)
132 simp-4r 782 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
133132simpld 495 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐼𝑞))
13410, 12, 13, 53, 65, 81, 55, 131, 133btwnlng1 27561 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐿𝑞))
13510, 12, 13, 53, 81, 65, 55, 130, 134lncom 27564 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑞𝐿𝐴))
136135adantr 481 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟 ∈ (𝑞𝐿𝐴))
137 simpr 485 . . . . . . . . . . . 12 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟𝐴)
13810, 12, 13, 75, 82, 77, 78, 76, 114, 136, 137ncolncol 27588 . . . . . . . . . . 11 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → ¬ (𝑟 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
13910, 12, 13, 75, 76, 77, 78, 138ncolne2 27568 . . . . . . . . . 10 ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟𝐴) → 𝑟𝐶)
14074, 139pm2.61dane 3032 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟𝐶)
141 simpllr 774 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶))))
142141simprd 496 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
143142simprd 496 . . . . . . . . . 10 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ (𝑟𝐼𝐶))
14410, 13, 12, 53, 55, 62, 61, 143btwncolg3 27499 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 ∈ (𝑟𝐿𝑥) ∨ 𝑟 = 𝑥))
145 simplr 767 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠𝑃)
146 simplr 767 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
147146simprd 496 . . . . . . . . . . . 12 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝐵𝐼𝑝))
148147ad2antrr 724 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐼𝑝))
149 simprl 769 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐼𝑞))
150124simpld 495 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
151150ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
152151adantr 481 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ (𝐶𝐼𝑝))
15334ad8antr 738 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 𝐴) = (𝐶 𝐵))
154153eqcomd 2742 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 𝐵) = (𝐶 𝐴))
15510, 11, 12, 42, 48, 52axtgcgrrflx 27404 . . . . . . . . . . . . . 14 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 𝐵) = (𝐵 𝐴))
15610, 11, 12, 42, 60, 48, 117, 60, 52, 80, 52, 48, 70, 152, 96, 153, 121, 154, 155axtg5seg 27407 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑝 𝐵) = (𝑞 𝐴))
15710, 11, 12, 42, 117, 52, 80, 48, 156tgcgrcomlr 27422 . . . . . . . . . . . 12 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 𝑝) = (𝐴 𝑞))
158157ad2antrr 724 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝑝) = (𝐴 𝑞))
159 simprr 771 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)
16010, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159cgr3simp2 27463 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝑝) = (𝑠 𝑞))
16110, 11, 12, 53, 64, 65axtgcgrrflx 27404 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝐴) = (𝐴 𝐵))
16210, 11, 12, 53, 64, 55, 118, 65, 65, 145, 81, 64, 148, 149, 158, 160, 161, 123tgifscgr 27450 . . . . . . . . . 10 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝐴) = (𝑠 𝐵))
163 simp-10l 793 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝜑)
164125simpld 495 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ (𝐶𝐼𝑝))
16510, 12, 13, 53, 61, 65, 118, 71, 164btwnlng3 27563 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ (𝐶𝐿𝐴))
16610, 12, 13, 53, 61, 65, 64, 118, 83, 165, 127ncolncol 27588 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
16715ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐺 ∈ TarskiG)
168 simplr 767 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝑝𝑃)
1699ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐴𝑃)
17030ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐵𝑃)
171 simpr 485 . . . . . . . . . . . . . . 15 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
17210, 13, 12, 167, 168, 169, 170, 171colrot1 27501 . . . . . . . . . . . . . 14 (((𝜑𝑝𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
173172stoic1a 1774 . . . . . . . . . . . . 13 (((𝜑𝑝𝑃) ∧ ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
174163, 118, 166, 173syl21anc 836 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
17510, 12, 13, 53, 118, 65, 64, 166ncolne2 27568 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝𝐵)
176175necomd 2999 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵𝑝)
177176neneqd 2948 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝐵 = 𝑝)
17810, 13, 12, 53, 65, 81, 55, 133btwncolg1 27497 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐿𝑞) ∨ 𝐴 = 𝑞))
17910, 11, 12, 53, 55, 65, 145, 64, 162tgcgrcomlr 27422 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 𝑟) = (𝐵 𝑠))
180120ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝑞) = (𝐴 𝑝))
18110, 11, 12, 53, 118, 81axtgcgrrflx 27404 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 𝑞) = (𝑞 𝑝))
18210, 11, 12, 53, 64, 55, 118, 81, 65, 145, 81, 118, 148, 149, 158, 160, 180, 181tgifscgr 27450 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝑞) = (𝑠 𝑝))
18310, 11, 12, 53, 65, 145, 81, 149tgbtwncom 27430 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝑞𝐼𝐴))
18410, 11, 12, 42, 52, 54, 117, 147tgbtwncom 27430 . . . . . . . . . . . . . . . . . . 19 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝑝𝐼𝐵))
185184ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑝𝐼𝐵))
186160eqcomd 2742 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 𝑞) = (𝑟 𝑝))
18710, 11, 12, 53, 145, 81, 55, 118, 186tgcgrcomlr 27422 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 𝑠) = (𝑝 𝑟))
18810, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159cgr3simp1 27462 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 𝑟) = (𝐴 𝑠))
189188eqcomd 2742 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 𝑠) = (𝐵 𝑟))
19010, 11, 12, 53, 65, 145, 64, 55, 189tgcgrcomlr 27422 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 𝐴) = (𝑟 𝐵))
19110, 11, 12, 53, 81, 145, 65, 118, 55, 64, 183, 185, 187, 190tgcgrextend 27427 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 𝐴) = (𝑝 𝐵))
19210, 11, 63, 53, 65, 55, 81, 64, 145, 118, 179, 182, 191trgcgr 27458 . . . . . . . . . . . . . . . 16 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐴𝑟𝑞”⟩(cgrG‘𝐺)⟨“𝐵𝑠𝑝”⟩)
19310, 13, 12, 53, 65, 55, 81, 63, 64, 145, 118, 178, 192lnxfr 27508 . . . . . . . . . . . . . . 15 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 ∈ (𝐵𝐿𝑝) ∨ 𝐵 = 𝑝))
194193orcomd 869 . . . . . . . . . . . . . 14 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 = 𝑝𝑠 ∈ (𝐵𝐿𝑝)))
195194ord 862 . . . . . . . . . . . . 13 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (¬ 𝐵 = 𝑝𝑠 ∈ (𝐵𝐿𝑝)))
196177, 195mpd 15 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐵𝐿𝑝))
19710, 12, 13, 53, 64, 118, 55, 176, 148btwnlng1 27561 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐿𝑝))
19810, 12, 13, 53, 65, 81, 145, 131, 149btwnlng1 27561 . . . . . . . . . . . 12 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐿𝑞))
19910, 12, 13, 53, 64, 118, 65, 81, 174, 196, 197, 198, 134tglineinteq 27587 . . . . . . . . . . 11 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 = 𝑟)
200199oveq1d 7372 . . . . . . . . . 10 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 𝐵) = (𝑟 𝐵))
201162, 200eqtr2d 2777 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 𝐵) = (𝑟 𝐴))
202154ad2antrr 724 . . . . . . . . 9 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 𝐵) = (𝐶 𝐴))
20310, 13, 12, 53, 55, 61, 62, 63, 64, 65, 11, 140, 144, 201, 202lncgr 27511 . . . . . . . 8 (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 𝐵) = (𝑥 𝐴))
20410, 11, 12, 63, 42, 52, 54, 117, 48, 80, 147, 157tgcgrxfr 27460 . . . . . . . 8 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → ∃𝑠𝑃 (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩))
205203, 204r19.29a 3159 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑥 𝐵) = (𝑥 𝐴))
206 simprrl 779 . . . . . . . 8 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐴𝐼𝐵))
20710, 11, 12, 42, 48, 43, 52, 206tgbtwncom 27430 . . . . . . 7 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐵𝐼𝐴))
20810, 11, 12, 13, 14, 42, 43, 2, 48, 52, 205, 207ismir 27601 . . . . . 6 (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 = (𝑀𝐴))
209 simplr 767 . . . . . . 7 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟𝑃)
210 simprr 771 . . . . . . 7 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ (𝐵𝐼𝑝))
21110, 11, 12, 41, 59, 51, 116, 47, 209, 151, 210axtgpasch 27409 . . . . . 6 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
212208, 211reximddv 3168 . . . . 5 ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) ∧ 𝑟𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
21310, 11, 12, 40, 58, 46, 115, 150tgbtwncom 27430 . . . . . 6 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐴 ∈ (𝑝𝐼𝐶))
21410, 11, 12, 40, 58, 50, 79, 95tgbtwncom 27430 . . . . . 6 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → 𝐵 ∈ (𝑞𝐼𝐶))
21510, 11, 12, 40, 115, 79, 58, 46, 50, 213, 214axtgpasch 27409 . . . . 5 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → ∃𝑟𝑃 (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
216212, 215r19.29a 3159 . . . 4 ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) ∧ 𝑞𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝))) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
217 simplr 767 . . . . 5 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → 𝑝𝑃)
21810, 11, 12, 39, 57, 49, 45, 217axtgsegcon 27406 . . . 4 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → ∃𝑞𝑃 (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 𝑞) = (𝐴 𝑝)))
219216, 218r19.29a 3159 . . 3 ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
22010fvexi 6856 . . . . . 6 𝑃 ∈ V
221220a1i 11 . . . . 5 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝑃 ∈ V)
222221, 56, 44, 69nehash2 14373 . . . 4 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 2 ≤ (♯‘𝑃))
22310, 11, 12, 38, 56, 44, 222tgbtwndiff 27448 . . 3 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑝𝑃 (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴𝑝))
224219, 223r19.29a 3159 . 2 ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
22537, 224pm2.61dan 811 1 (𝜑 → ∃𝑥𝑃 𝐵 = (𝑀𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2943  wrex 3073  Vcvv 3445   class class class wbr 5105  cfv 6496  (class class class)co 7357  ⟨“cs3 14731  Basecbs 17083  distcds 17142  TarskiGcstrkg 27369  Itvcitv 27375  LineGclng 27376  cgrGccgrg 27452  pInvGcmir 27594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-hash 14231  df-word 14403  df-concat 14459  df-s1 14484  df-s2 14737  df-s3 14738  df-trkgc 27390  df-trkgb 27391  df-trkgcb 27392  df-trkg 27395  df-cgrg 27453  df-mir 27595
This theorem is referenced by:  footexALT  27660  footex  27663  colperpexlem3  27674  opphllem  27677
  Copyright terms: Public domain W3C validator