midexlem - Metamath Proof Explorer

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

Theorem midexlem 28776

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 28822 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.

Step	Hyp	Ref	Expression
1		midexlem.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
2		midexlem.m	. . . . . . . 8 ⊢ 𝑀 = (𝑆‘𝑥)
3		fveq2 6842	. . . . . . . 8 ⊢ (𝑥 = 𝐶 → (𝑆‘𝑥) = (𝑆‘𝐶))
4	2, 3	eqtrid 2784	. . . . . . 7 ⊢ (𝑥 = 𝐶 → 𝑀 = (𝑆‘𝐶))
5	4	fveq1d 6844	. . . . . 6 ⊢ (𝑥 = 𝐶 → (𝑀‘𝐴) = ((𝑆‘𝐶)‘𝐴))
6	5	rspceeqv 3601	. . . . 5 ⊢ ((𝐶 ∈ 𝑃 ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
7	1, 6	sylan 581	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
8	7	adantlr 716	. . 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 2737	. . . . . . . 8 ⊢ (𝑆‘𝐴) = (𝑆‘𝐴)
17	10, 11, 12, 13, 14, 15, 9, 16	mircinv 28752	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝐴)‘𝐴) = 𝐴)
18	17	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ((𝑆‘𝐴)‘𝐴) = 𝐴)
19		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵)
20	18, 19	eqtr2d 2773	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐵 = ((𝑆‘𝐴)‘𝐴))
21		fveq2 6842	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑆‘𝑥) = (𝑆‘𝐴))
22	2, 21	eqtrid 2784	. . . . . . 7 ⊢ (𝑥 = 𝐴 → 𝑀 = (𝑆‘𝐴))
23	22	fveq1d 6844	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑀‘𝐴) = ((𝑆‘𝐴)‘𝐴))
24	23	rspceeqv 3601	. . . . 5 ⊢ ((𝐴 ∈ 𝑃 ∧ 𝐵 = ((𝑆‘𝐴)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
25	9, 20, 24	syl2an2r 686	. . . 4 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
26	25	adantlr 716	. . 3 ⊢ (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐴 = 𝐵) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
27	15	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
28		eqid 2737	. . . 4 ⊢ (𝑆‘𝐶) = (𝑆‘𝐶)
29	9	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴 ∈ 𝑃)
30		midexlem.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
31	30	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵 ∈ 𝑃)
32	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ∈ 𝑃)
33		simpr 484	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
34		midexlem.1	. . . . 5 ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵))
35	34	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 − 𝐴) = (𝐶 − 𝐵))
36	10, 11, 12, 13, 14, 27, 28, 29, 31, 32, 33, 35	colmid 28772	. . 3 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐵 = ((𝑆‘𝐶)‘𝐴) ∨ 𝐴 = 𝐵))
37	8, 26, 36	mpjaodan 961	. 2 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
38	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
39	38	ad2antrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐺 ∈ TarskiG)
40	39	ad2antrr 727	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐺 ∈ TarskiG)
41	40	ad2antrr 727	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐺 ∈ TarskiG)
42	41	adantr 480	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐺 ∈ TarskiG)
43		simprl 771	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ 𝑃)
44	9	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴 ∈ 𝑃)
45	44	ad2antrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ 𝑃)
46	45	ad2antrr 727	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ 𝑃)
47	46	ad2antrr 727	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ 𝑃)
48	47	adantr 480	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ 𝑃)
49	30	ad3antrrr 731	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐵 ∈ 𝑃)
50	49	ad2antrr 727	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ 𝑃)
51	50	ad2antrr 727	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐵 ∈ 𝑃)
52	51	adantr 480	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ 𝑃)
53	42	ad2antrr 727	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐺 ∈ TarskiG)
54		simpllr 776	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ 𝑃)
55	54	ad2antrr 727	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ 𝑃)
56	1	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ∈ 𝑃)
57	56	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐶 ∈ 𝑃)
58	57	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐶 ∈ 𝑃)
59	58	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐶 ∈ 𝑃)
60	59	adantr 480	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶 ∈ 𝑃)
61	60	ad2antrr 727	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ∈ 𝑃)
62	43	ad2antrr 727	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ 𝑃)
63		eqid 2737	. . . . . . . . 9 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
64	52	ad2antrr 727	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ 𝑃)
65	48	ad2antrr 727	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ 𝑃)
66		simpr 484	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 = 𝐴)
67	30	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵 ∈ 𝑃)
68		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
69	10, 12, 13, 38, 56, 44, 67, 68	ncolne1 28709	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ≠ 𝐴)
70	69	ad7antr 739	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶 ≠ 𝐴)
71	70	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ≠ 𝐴)
72	71	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐶 ≠ 𝐴)
73	72	necomd 2988	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐴 ≠ 𝐶)
74	66, 73	eqnetrd 3000	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 ≠ 𝐶)
75	53	adantr 480	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐺 ∈ TarskiG)
76	55	adantr 480	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ∈ 𝑃)
77	65	adantr 480	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐴 ∈ 𝑃)
78	61	adantr 480	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐶 ∈ 𝑃)
79		simplr 769	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝑞 ∈ 𝑃)
80	79	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑞 ∈ 𝑃)
81	80	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ 𝑃)
82	81	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑞 ∈ 𝑃)
83	68	ad9antr 743	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
84	10, 13, 12, 53, 65, 64, 61, 83	ncolrot2 28647	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
85	15	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐺 ∈ TarskiG)
86	30	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐵 ∈ 𝑃)
87	9	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐴 ∈ 𝑃)
88	1	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐶 ∈ 𝑃)
89		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
90	10, 13, 12, 85, 86, 87, 88, 89	colcom 28642	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
91	90	stoic1a 1774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
92	91	ad9antr 743	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
93	10, 12, 13, 53, 61, 64, 65, 92	ncolne1 28709	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ≠ 𝐵)
94	93	necomd 2988	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ≠ 𝐶)
95		simprl 771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ (𝐶𝐼𝑞))
96	95	ad3antrrr 731	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ (𝐶𝐼𝑞))
97	96	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ (𝐶𝐼𝑞))
98	10, 12, 13, 53, 61, 64, 81, 93, 97	btwnlng3 28705	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐶𝐿𝐵))
99	10, 12, 13, 53, 64, 61, 81, 94, 98	lncom 28706	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐵𝐿𝐶))
100	53	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐺 ∈ TarskiG)
101	61	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 ∈ 𝑃)
102	64	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ 𝑃)
103	97	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝑞))
104		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝑞 = 𝐶)
105	104	oveq2d 7384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → (𝐶𝐼𝑞) = (𝐶𝐼𝐶))
106	103, 105	eleqtrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶))
107	10, 11, 12, 100, 101, 102, 106	axtgbtwnid 28550	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 = 𝐵)
108	93	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 ≠ 𝐵)
109	108	neneqd 2938	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → ¬ 𝐶 = 𝐵)
110	107, 109	pm2.65da 817	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝑞 = 𝐶)
111	110	neqned 2940	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐶)
112	10, 12, 13, 53, 64, 61, 65, 81, 84, 99, 111	ncolncol 28730	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
113	10, 13, 12, 53, 61, 65, 81, 112	ncolcom 28645	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
114	113	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
115		simp-4r 784	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝑝 ∈ 𝑃)
116	115	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑝 ∈ 𝑃)
117	116	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑝 ∈ 𝑃)
118	117	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ 𝑃)
119		simp-4r 784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝)))
120	119	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 − 𝑞) = (𝐴 − 𝑝))
121	120	eqcomd 2743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 − 𝑝) = (𝐵 − 𝑞))
122	121	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑝) = (𝐵 − 𝑞))
123	10, 11, 12, 53, 65, 118, 64, 81, 122	tgcgrcomlr 28564	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 − 𝐴) = (𝑞 − 𝐵))
124		simpllr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
125	124	ad5antr 735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
126	125	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ≠ 𝑝)
127	126	necomd 2988	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ≠ 𝐴)
128	10, 11, 12, 53, 118, 65, 81, 64, 123, 127	tgcgrneq 28567	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐵)
129	10, 12, 13, 53, 61, 64, 65, 81, 92, 98, 128	ncolncol 28730	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
130	10, 12, 13, 53, 81, 64, 65, 129	ncolne2 28710	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐴)
131	130	necomd 2988	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ≠ 𝑞)
132		simp-4r 784	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
133	132	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐼𝑞))
134	10, 12, 13, 53, 65, 81, 55, 131, 133	btwnlng1 28703	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐿𝑞))
135	10, 12, 13, 53, 81, 65, 55, 130, 134	lncom 28706	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑞𝐿𝐴))
136	135	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ∈ (𝑞𝐿𝐴))
137		simpr 484	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ≠ 𝐴)
138	10, 12, 13, 75, 82, 77, 78, 76, 114, 136, 137	ncolncol 28730	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → ¬ (𝑟 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
139	10, 12, 13, 75, 76, 77, 78, 138	ncolne2 28710	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ≠ 𝐶)
140	74, 139	pm2.61dane 3020	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ≠ 𝐶)
141		simpllr 776	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶))))
142	141	simprd 495	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
143	142	simprd 495	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ (𝑟𝐼𝐶))
144	10, 13, 12, 53, 55, 62, 61, 143	btwncolg3 28641	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 ∈ (𝑟𝐿𝑥) ∨ 𝑟 = 𝑥))
145		simplr 769	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ 𝑃)
146		simplr 769	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
147	146	simprd 495	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝐵𝐼𝑝))
148	147	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐼𝑝))
149		simprl 771	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐼𝑞))
150	124	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
151	150	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
152	151	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ (𝐶𝐼𝑝))
153	34	ad8antr 741	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 − 𝐴) = (𝐶 − 𝐵))
154	153	eqcomd 2743	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 − 𝐵) = (𝐶 − 𝐴))
155	10, 11, 12, 42, 48, 52	axtgcgrrflx 28546	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 − 𝐵) = (𝐵 − 𝐴))
156	10, 11, 12, 42, 60, 48, 117, 60, 52, 80, 52, 48, 70, 152, 96, 153, 121, 154, 155	axtg5seg 28549	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑝 − 𝐵) = (𝑞 − 𝐴))
157	10, 11, 12, 42, 117, 52, 80, 48, 156	tgcgrcomlr 28564	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 − 𝑝) = (𝐴 − 𝑞))
158	157	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑝) = (𝐴 − 𝑞))
159		simprr 773	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)
160	10, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159	cgr3simp2 28605	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝑝) = (𝑠 − 𝑞))
161	10, 11, 12, 53, 64, 65	axtgcgrrflx 28546	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝐴) = (𝐴 − 𝐵))
162	10, 11, 12, 53, 64, 55, 118, 65, 65, 145, 81, 64, 148, 149, 158, 160, 161, 123	tgifscgr 28592	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝐴) = (𝑠 − 𝐵))
163		simp-10l 795	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝜑)
164	125	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ (𝐶𝐼𝑝))
165	10, 12, 13, 53, 61, 65, 118, 71, 164	btwnlng3 28705	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ (𝐶𝐿𝐴))
166	10, 12, 13, 53, 61, 65, 64, 118, 83, 165, 127	ncolncol 28730	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
167	15	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐺 ∈ TarskiG)
168		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝑝 ∈ 𝑃)
169	9	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐴 ∈ 𝑃)
170	30	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐵 ∈ 𝑃)
171		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
172	10, 13, 12, 167, 168, 169, 170, 171	colrot1 28643	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
173	172	stoic1a 1774	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
174	163, 118, 166, 173	syl21anc 838	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
175	10, 12, 13, 53, 118, 65, 64, 166	ncolne2 28710	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ≠ 𝐵)
176	175	necomd 2988	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ≠ 𝑝)
177	176	neneqd 2938	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝐵 = 𝑝)
178	10, 13, 12, 53, 65, 81, 55, 133	btwncolg1 28639	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐿𝑞) ∨ 𝐴 = 𝑞))
179	10, 11, 12, 53, 55, 65, 145, 64, 162	tgcgrcomlr 28564	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑟) = (𝐵 − 𝑠))
180	120	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑞) = (𝐴 − 𝑝))
181	10, 11, 12, 53, 118, 81	axtgcgrrflx 28546	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 − 𝑞) = (𝑞 − 𝑝))
182	10, 11, 12, 53, 64, 55, 118, 81, 65, 145, 81, 118, 148, 149, 158, 160, 180, 181	tgifscgr 28592	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝑞) = (𝑠 − 𝑝))
183	10, 11, 12, 53, 65, 145, 81, 149	tgbtwncom 28572	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝑞𝐼𝐴))
184	10, 11, 12, 42, 52, 54, 117, 147	tgbtwncom 28572	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝑝𝐼𝐵))
185	184	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑝𝐼𝐵))
186	160	eqcomd 2743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝑞) = (𝑟 − 𝑝))
187	10, 11, 12, 53, 145, 81, 55, 118, 186	tgcgrcomlr 28564	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 − 𝑠) = (𝑝 − 𝑟))
188	10, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159	cgr3simp1 28604	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑟) = (𝐴 − 𝑠))
189	188	eqcomd 2743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑠) = (𝐵 − 𝑟))
190	10, 11, 12, 53, 65, 145, 64, 55, 189	tgcgrcomlr 28564	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝐴) = (𝑟 − 𝐵))
191	10, 11, 12, 53, 81, 145, 65, 118, 55, 64, 183, 185, 187, 190	tgcgrextend 28569	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 − 𝐴) = (𝑝 − 𝐵))
192	10, 11, 63, 53, 65, 55, 81, 64, 145, 118, 179, 182, 191	trgcgr 28600	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐴𝑟𝑞”⟩(cgrG‘𝐺)⟨“𝐵𝑠𝑝”⟩)
193	10, 13, 12, 53, 65, 55, 81, 63, 64, 145, 118, 178, 192	lnxfr 28650	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 ∈ (𝐵𝐿𝑝) ∨ 𝐵 = 𝑝))
194	193	orcomd 872	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 = 𝑝 ∨ 𝑠 ∈ (𝐵𝐿𝑝)))
195	194	ord 865	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (¬ 𝐵 = 𝑝 → 𝑠 ∈ (𝐵𝐿𝑝)))
196	177, 195	mpd 15	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐵𝐿𝑝))
197	10, 12, 13, 53, 64, 118, 55, 176, 148	btwnlng1 28703	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐿𝑝))
198	10, 12, 13, 53, 65, 81, 145, 131, 149	btwnlng1 28703	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐿𝑞))
199	10, 12, 13, 53, 64, 118, 65, 81, 174, 196, 197, 198, 134	tglineinteq 28729	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 = 𝑟)
200	199	oveq1d 7383	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝐵) = (𝑟 − 𝐵))
201	162, 200	eqtr2d 2773	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝐵) = (𝑟 − 𝐴))
202	154	ad2antrr 727	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 − 𝐵) = (𝐶 − 𝐴))
203	10, 13, 12, 53, 55, 61, 62, 63, 64, 65, 11, 140, 144, 201, 202	lncgr 28653	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 − 𝐵) = (𝑥 − 𝐴))
204	10, 11, 12, 63, 42, 52, 54, 117, 48, 80, 147, 157	tgcgrxfr 28602	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → ∃𝑠 ∈ 𝑃 (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩))
205	203, 204	r19.29a 3146	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑥 − 𝐵) = (𝑥 − 𝐴))
206		simprrl 781	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐴𝐼𝐵))
207	10, 11, 12, 42, 48, 43, 52, 206	tgbtwncom 28572	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐵𝐼𝐴))
208	10, 11, 12, 13, 14, 42, 43, 2, 48, 52, 205, 207	ismir 28743	. . . . . 6 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 = (𝑀‘𝐴))
209		simplr 769	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ 𝑃)
210		simprr 773	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ (𝐵𝐼𝑝))
211	10, 11, 12, 41, 59, 51, 116, 47, 209, 151, 210	axtgpasch 28551	. . . . . 6 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
212	208, 211	reximddv 3154	. . . . 5 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
213	10, 11, 12, 40, 58, 46, 115, 150	tgbtwncom 28572	. . . . . 6 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ (𝑝𝐼𝐶))
214	10, 11, 12, 40, 58, 50, 79, 95	tgbtwncom 28572	. . . . . 6 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ (𝑞𝐼𝐶))
215	10, 11, 12, 40, 115, 79, 58, 46, 50, 213, 214	axtgpasch 28551	. . . . 5 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → ∃𝑟 ∈ 𝑃 (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
216	212, 215	r19.29a 3146	. . . 4 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
217		simplr 769	. . . . 5 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝑝 ∈ 𝑃)
218	10, 11, 12, 39, 57, 49, 45, 217	axtgsegcon 28548	. . . 4 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → ∃𝑞 ∈ 𝑃 (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝)))
219	216, 218	r19.29a 3146	. . 3 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
220	10	fvexi 6856	. . . . . 6 ⊢ 𝑃 ∈ V
221	220	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝑃 ∈ V)
222	221, 56, 44, 69	nehash2 14409	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 2 ≤ (♯‘𝑃))
223	10, 11, 12, 38, 56, 44, 222	tgbtwndiff 28590	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑝 ∈ 𝑃 (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
224	219, 223	r19.29a 3146	. 2 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
225	37, 224	pm2.61dan 813	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∃wrex 3062 Vcvv 3442 class class class wbr 5100 ‘cfv 6500 (class class class)co 7368 ⟨“cs3 14777 Basecbs 17148 distcds 17198 TarskiGcstrkg 28511 Itvcitv 28517 LineGclng 28518 cgrGccgrg 28594 pInvGcmir 28736

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-oadd 8411 df-er 8645 df-pm 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-dju 9825 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-nn 12158 df-2 12220 df-3 12221 df-n0 12414 df-xnn0 12487 df-z 12501 df-uz 12764 df-fz 13436 df-fzo 13583 df-hash 14266 df-word 14449 df-concat 14506 df-s1 14532 df-s2 14783 df-s3 14784 df-trkgc 28532 df-trkgb 28533 df-trkgcb 28534 df-trkg 28537 df-cgrg 28595 df-mir 28737

This theorem is referenced by: footexALT 28802 footex 28805 colperpexlem3 28816 opphllem 28819

W3C validator