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 28619

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 28665 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 6858	. . . . . . . 8 ⊢ (𝑥 = 𝐶 → (𝑆‘𝑥) = (𝑆‘𝐶))
4	2, 3	eqtrid 2776	. . . . . . 7 ⊢ (𝑥 = 𝐶 → 𝑀 = (𝑆‘𝐶))
5	4	fveq1d 6860	. . . . . 6 ⊢ (𝑥 = 𝐶 → (𝑀‘𝐴) = ((𝑆‘𝐶)‘𝐴))
6	5	rspceeqv 3611	. . . . 5 ⊢ ((𝐶 ∈ 𝑃 ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
7	1, 6	sylan 580	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
8	7	adantlr 715	. . 3 ⊢ (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
9		midexlem.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
10		mirval.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
11		mirval.d	. . . . . . . 8 ⊢ − = (dist‘𝐺)
12		mirval.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
13		mirval.l	. . . . . . . 8 ⊢ 𝐿 = (LineG‘𝐺)
14		mirval.s	. . . . . . . 8 ⊢ 𝑆 = (pInvG‘𝐺)
15		mirval.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
16		eqid 2729	. . . . . . . 8 ⊢ (𝑆‘𝐴) = (𝑆‘𝐴)
17	10, 11, 12, 13, 14, 15, 9, 16	mircinv 28595	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝐴)‘𝐴) = 𝐴)
18	17	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ((𝑆‘𝐴)‘𝐴) = 𝐴)
19		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵)
20	18, 19	eqtr2d 2765	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐵 = ((𝑆‘𝐴)‘𝐴))
21		fveq2 6858	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑆‘𝑥) = (𝑆‘𝐴))
22	2, 21	eqtrid 2776	. . . . . . 7 ⊢ (𝑥 = 𝐴 → 𝑀 = (𝑆‘𝐴))
23	22	fveq1d 6860	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑀‘𝐴) = ((𝑆‘𝐴)‘𝐴))
24	23	rspceeqv 3611	. . . . 5 ⊢ ((𝐴 ∈ 𝑃 ∧ 𝐵 = ((𝑆‘𝐴)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
25	9, 20, 24	syl2an2r 685	. . . 4 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
26	25	adantlr 715	. . 3 ⊢ (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐴 = 𝐵) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
27	15	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
28		eqid 2729	. . . 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 28615	. . 3 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐵 = ((𝑆‘𝐶)‘𝐴) ∨ 𝐴 = 𝐵))
37	8, 26, 36	mpjaodan 960	. 2 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
38	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
39	38	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐺 ∈ TarskiG)
40	39	ad2antrr 726	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐺 ∈ TarskiG)
41	40	ad2antrr 726	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐺 ∈ TarskiG)
42	41	adantr 480	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐺 ∈ TarskiG)
43		simprl 770	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ 𝑃)
44	9	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴 ∈ 𝑃)
45	44	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ 𝑃)
46	45	ad2antrr 726	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ 𝑃)
47	46	ad2antrr 726	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ 𝑃)
48	47	adantr 480	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ 𝑃)
49	30	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐵 ∈ 𝑃)
50	49	ad2antrr 726	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ 𝑃)
51	50	ad2antrr 726	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐵 ∈ 𝑃)
52	51	adantr 480	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ 𝑃)
53	42	ad2antrr 726	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐺 ∈ TarskiG)
54		simpllr 775	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ 𝑃)
55	54	ad2antrr 726	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ 𝑃)
56	1	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ∈ 𝑃)
57	56	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐶 ∈ 𝑃)
58	57	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐶 ∈ 𝑃)
59	58	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐶 ∈ 𝑃)
60	59	adantr 480	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶 ∈ 𝑃)
61	60	ad2antrr 726	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ∈ 𝑃)
62	43	ad2antrr 726	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ 𝑃)
63		eqid 2729	. . . . . . . . 9 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
64	52	ad2antrr 726	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ 𝑃)
65	48	ad2antrr 726	. . . . . . . . 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 28552	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ≠ 𝐴)
70	69	ad7antr 738	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶 ≠ 𝐴)
71	70	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ≠ 𝐴)
72	71	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐶 ≠ 𝐴)
73	72	necomd 2980	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐴 ≠ 𝐶)
74	66, 73	eqnetrd 2992	. . . . . . . . . 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 768	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝑞 ∈ 𝑃)
80	79	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑞 ∈ 𝑃)
81	80	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ 𝑃)
82	81	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑞 ∈ 𝑃)
83	68	ad9antr 742	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
84	10, 13, 12, 53, 65, 64, 61, 83	ncolrot2 28490	. . . . . . . . . . . . . . 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 28485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
91	90	stoic1a 1772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
92	91	ad9antr 742	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
93	10, 12, 13, 53, 61, 64, 65, 92	ncolne1 28552	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ≠ 𝐵)
94	93	necomd 2980	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ≠ 𝐶)
95		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ (𝐶𝐼𝑞))
96	95	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ (𝐶𝐼𝑞))
97	96	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ (𝐶𝐼𝑞))
98	10, 12, 13, 53, 61, 64, 81, 93, 97	btwnlng3 28548	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐶𝐿𝐵))
99	10, 12, 13, 53, 64, 61, 81, 94, 98	lncom 28549	. . . . . . . . . . . . . . 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 7403	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → (𝐶𝐼𝑞) = (𝐶𝐼𝐶))
106	103, 105	eleqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶))
107	10, 11, 12, 100, 101, 102, 106	axtgbtwnid 28393	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 = 𝐵)
108	93	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 ≠ 𝐵)
109	108	neneqd 2930	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → ¬ 𝐶 = 𝐵)
110	107, 109	pm2.65da 816	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝑞 = 𝐶)
111	110	neqned 2932	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐶)
112	10, 12, 13, 53, 64, 61, 65, 81, 84, 99, 111	ncolncol 28573	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
113	10, 13, 12, 53, 61, 65, 81, 112	ncolcom 28488	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
114	113	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
115		simp-4r 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝑝 ∈ 𝑃)
116	115	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑝 ∈ 𝑃)
117	116	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑝 ∈ 𝑃)
118	117	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ 𝑃)
119		simp-4r 783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝)))
120	119	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 − 𝑞) = (𝐴 − 𝑝))
121	120	eqcomd 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 − 𝑝) = (𝐵 − 𝑞))
122	121	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑝) = (𝐵 − 𝑞))
123	10, 11, 12, 53, 65, 118, 64, 81, 122	tgcgrcomlr 28407	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 − 𝐴) = (𝑞 − 𝐵))
124		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
125	124	ad5antr 734	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
126	125	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ≠ 𝑝)
127	126	necomd 2980	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ≠ 𝐴)
128	10, 11, 12, 53, 118, 65, 81, 64, 123, 127	tgcgrneq 28410	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐵)
129	10, 12, 13, 53, 61, 64, 65, 81, 92, 98, 128	ncolncol 28573	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
130	10, 12, 13, 53, 81, 64, 65, 129	ncolne2 28553	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐴)
131	130	necomd 2980	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ≠ 𝑞)
132		simp-4r 783	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
133	132	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐼𝑞))
134	10, 12, 13, 53, 65, 81, 55, 131, 133	btwnlng1 28546	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐿𝑞))
135	10, 12, 13, 53, 81, 65, 55, 130, 134	lncom 28549	. . . . . . . . . . . . 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 28573	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → ¬ (𝑟 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
139	10, 12, 13, 75, 76, 77, 78, 138	ncolne2 28553	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ≠ 𝐶)
140	74, 139	pm2.61dane 3012	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ≠ 𝐶)
141		simpllr 775	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶))))
142	141	simprd 495	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
143	142	simprd 495	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ (𝑟𝐼𝐶))
144	10, 13, 12, 53, 55, 62, 61, 143	btwncolg3 28484	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 ∈ (𝑟𝐿𝑥) ∨ 𝑟 = 𝑥))
145		simplr 768	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ 𝑃)
146		simplr 768	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
147	146	simprd 495	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝐵𝐼𝑝))
148	147	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐼𝑝))
149		simprl 770	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐼𝑞))
150	124	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
151	150	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
152	151	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ (𝐶𝐼𝑝))
153	34	ad8antr 740	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 − 𝐴) = (𝐶 − 𝐵))
154	153	eqcomd 2735	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 − 𝐵) = (𝐶 − 𝐴))
155	10, 11, 12, 42, 48, 52	axtgcgrrflx 28389	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 − 𝐵) = (𝐵 − 𝐴))
156	10, 11, 12, 42, 60, 48, 117, 60, 52, 80, 52, 48, 70, 152, 96, 153, 121, 154, 155	axtg5seg 28392	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑝 − 𝐵) = (𝑞 − 𝐴))
157	10, 11, 12, 42, 117, 52, 80, 48, 156	tgcgrcomlr 28407	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 − 𝑝) = (𝐴 − 𝑞))
158	157	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑝) = (𝐴 − 𝑞))
159		simprr 772	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)
160	10, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159	cgr3simp2 28448	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝑝) = (𝑠 − 𝑞))
161	10, 11, 12, 53, 64, 65	axtgcgrrflx 28389	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝐴) = (𝐴 − 𝐵))
162	10, 11, 12, 53, 64, 55, 118, 65, 65, 145, 81, 64, 148, 149, 158, 160, 161, 123	tgifscgr 28435	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝐴) = (𝑠 − 𝐵))
163		simp-10l 794	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝜑)
164	125	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ (𝐶𝐼𝑝))
165	10, 12, 13, 53, 61, 65, 118, 71, 164	btwnlng3 28548	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ (𝐶𝐿𝐴))
166	10, 12, 13, 53, 61, 65, 64, 118, 83, 165, 127	ncolncol 28573	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
167	15	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐺 ∈ TarskiG)
168		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝑝 ∈ 𝑃)
169	9	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐴 ∈ 𝑃)
170	30	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐵 ∈ 𝑃)
171		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
172	10, 13, 12, 167, 168, 169, 170, 171	colrot1 28486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
173	172	stoic1a 1772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
174	163, 118, 166, 173	syl21anc 837	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
175	10, 12, 13, 53, 118, 65, 64, 166	ncolne2 28553	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ≠ 𝐵)
176	175	necomd 2980	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ≠ 𝑝)
177	176	neneqd 2930	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝐵 = 𝑝)
178	10, 13, 12, 53, 65, 81, 55, 133	btwncolg1 28482	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐿𝑞) ∨ 𝐴 = 𝑞))
179	10, 11, 12, 53, 55, 65, 145, 64, 162	tgcgrcomlr 28407	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑟) = (𝐵 − 𝑠))
180	120	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑞) = (𝐴 − 𝑝))
181	10, 11, 12, 53, 118, 81	axtgcgrrflx 28389	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 − 𝑞) = (𝑞 − 𝑝))
182	10, 11, 12, 53, 64, 55, 118, 81, 65, 145, 81, 118, 148, 149, 158, 160, 180, 181	tgifscgr 28435	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝑞) = (𝑠 − 𝑝))
183	10, 11, 12, 53, 65, 145, 81, 149	tgbtwncom 28415	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝑞𝐼𝐴))
184	10, 11, 12, 42, 52, 54, 117, 147	tgbtwncom 28415	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝑝𝐼𝐵))
185	184	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑝𝐼𝐵))
186	160	eqcomd 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝑞) = (𝑟 − 𝑝))
187	10, 11, 12, 53, 145, 81, 55, 118, 186	tgcgrcomlr 28407	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 − 𝑠) = (𝑝 − 𝑟))
188	10, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159	cgr3simp1 28447	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑟) = (𝐴 − 𝑠))
189	188	eqcomd 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑠) = (𝐵 − 𝑟))
190	10, 11, 12, 53, 65, 145, 64, 55, 189	tgcgrcomlr 28407	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝐴) = (𝑟 − 𝐵))
191	10, 11, 12, 53, 81, 145, 65, 118, 55, 64, 183, 185, 187, 190	tgcgrextend 28412	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 − 𝐴) = (𝑝 − 𝐵))
192	10, 11, 63, 53, 65, 55, 81, 64, 145, 118, 179, 182, 191	trgcgr 28443	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐴𝑟𝑞”⟩(cgrG‘𝐺)⟨“𝐵𝑠𝑝”⟩)
193	10, 13, 12, 53, 65, 55, 81, 63, 64, 145, 118, 178, 192	lnxfr 28493	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 ∈ (𝐵𝐿𝑝) ∨ 𝐵 = 𝑝))
194	193	orcomd 871	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 = 𝑝 ∨ 𝑠 ∈ (𝐵𝐿𝑝)))
195	194	ord 864	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (¬ 𝐵 = 𝑝 → 𝑠 ∈ (𝐵𝐿𝑝)))
196	177, 195	mpd 15	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐵𝐿𝑝))
197	10, 12, 13, 53, 64, 118, 55, 176, 148	btwnlng1 28546	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐿𝑝))
198	10, 12, 13, 53, 65, 81, 145, 131, 149	btwnlng1 28546	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐿𝑞))
199	10, 12, 13, 53, 64, 118, 65, 81, 174, 196, 197, 198, 134	tglineinteq 28572	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 = 𝑟)
200	199	oveq1d 7402	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝐵) = (𝑟 − 𝐵))
201	162, 200	eqtr2d 2765	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝐵) = (𝑟 − 𝐴))
202	154	ad2antrr 726	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 − 𝐵) = (𝐶 − 𝐴))
203	10, 13, 12, 53, 55, 61, 62, 63, 64, 65, 11, 140, 144, 201, 202	lncgr 28496	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 − 𝐵) = (𝑥 − 𝐴))
204	10, 11, 12, 63, 42, 52, 54, 117, 48, 80, 147, 157	tgcgrxfr 28445	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → ∃𝑠 ∈ 𝑃 (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩))
205	203, 204	r19.29a 3141	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑥 − 𝐵) = (𝑥 − 𝐴))
206		simprrl 780	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐴𝐼𝐵))
207	10, 11, 12, 42, 48, 43, 52, 206	tgbtwncom 28415	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐵𝐼𝐴))
208	10, 11, 12, 13, 14, 42, 43, 2, 48, 52, 205, 207	ismir 28586	. . . . . 6 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 = (𝑀‘𝐴))
209		simplr 768	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ 𝑃)
210		simprr 772	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ (𝐵𝐼𝑝))
211	10, 11, 12, 41, 59, 51, 116, 47, 209, 151, 210	axtgpasch 28394	. . . . . 6 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
212	208, 211	reximddv 3149	. . . . 5 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
213	10, 11, 12, 40, 58, 46, 115, 150	tgbtwncom 28415	. . . . . 6 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ (𝑝𝐼𝐶))
214	10, 11, 12, 40, 58, 50, 79, 95	tgbtwncom 28415	. . . . . 6 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ (𝑞𝐼𝐶))
215	10, 11, 12, 40, 115, 79, 58, 46, 50, 213, 214	axtgpasch 28394	. . . . 5 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → ∃𝑟 ∈ 𝑃 (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
216	212, 215	r19.29a 3141	. . . 4 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
217		simplr 768	. . . . 5 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝑝 ∈ 𝑃)
218	10, 11, 12, 39, 57, 49, 45, 217	axtgsegcon 28391	. . . 4 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → ∃𝑞 ∈ 𝑃 (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝)))
219	216, 218	r19.29a 3141	. . 3 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
220	10	fvexi 6872	. . . . . 6 ⊢ 𝑃 ∈ V
221	220	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝑃 ∈ V)
222	221, 56, 44, 69	nehash2 14439	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 2 ≤ (♯‘𝑃))
223	10, 11, 12, 38, 56, 44, 222	tgbtwndiff 28433	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑝 ∈ 𝑃 (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
224	219, 223	r19.29a 3141	. 2 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
225	37, 224	pm2.61dan 812	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 Vcvv 3447 class class class wbr 5107 ‘cfv 6511 (class class class)co 7387 ⟨“cs3 14808 Basecbs 17179 distcds 17229 TarskiGcstrkg 28354 Itvcitv 28360 LineGclng 28361 cgrGccgrg 28437 pInvGcmir 28579

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-oadd 8438 df-er 8671 df-pm 8802 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-dju 9854 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-nn 12187 df-2 12249 df-3 12250 df-n0 12443 df-xnn0 12516 df-z 12530 df-uz 12794 df-fz 13469 df-fzo 13616 df-hash 14296 df-word 14479 df-concat 14536 df-s1 14561 df-s2 14814 df-s3 14815 df-trkgc 28375 df-trkgb 28376 df-trkgcb 28377 df-trkg 28380 df-cgrg 28438 df-mir 28580

This theorem is referenced by: footexALT 28645 footex 28648 colperpexlem3 28659 opphllem 28662

W3C validator