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 27053

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 27099 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 6774	. . . . . . . 8 ⊢ (𝑥 = 𝐶 → (𝑆‘𝑥) = (𝑆‘𝐶))
4	2, 3	eqtrid 2790	. . . . . . 7 ⊢ (𝑥 = 𝐶 → 𝑀 = (𝑆‘𝐶))
5	4	fveq1d 6776	. . . . . 6 ⊢ (𝑥 = 𝐶 → (𝑀‘𝐴) = ((𝑆‘𝐶)‘𝐴))
6	5	rspceeqv 3575	. . . . 5 ⊢ ((𝐶 ∈ 𝑃 ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
7	1, 6	sylan 580	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
8	7	adantlr 712	. . 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 2738	. . . . . . . 8 ⊢ (𝑆‘𝐴) = (𝑆‘𝐴)
17	10, 11, 12, 13, 14, 15, 9, 16	mircinv 27029	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝐴)‘𝐴) = 𝐴)
18	17	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ((𝑆‘𝐴)‘𝐴) = 𝐴)
19		simpr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵)
20	18, 19	eqtr2d 2779	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐵 = ((𝑆‘𝐴)‘𝐴))
21		fveq2 6774	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑆‘𝑥) = (𝑆‘𝐴))
22	2, 21	eqtrid 2790	. . . . . . 7 ⊢ (𝑥 = 𝐴 → 𝑀 = (𝑆‘𝐴))
23	22	fveq1d 6776	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑀‘𝐴) = ((𝑆‘𝐴)‘𝐴))
24	23	rspceeqv 3575	. . . . 5 ⊢ ((𝐴 ∈ 𝑃 ∧ 𝐵 = ((𝑆‘𝐴)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
25	9, 20, 24	syl2an2r 682	. . . 4 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
26	25	adantlr 712	. . 3 ⊢ (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐴 = 𝐵) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
27	15	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
28		eqid 2738	. . . 4 ⊢ (𝑆‘𝐶) = (𝑆‘𝐶)
29	9	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴 ∈ 𝑃)
30		midexlem.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
31	30	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵 ∈ 𝑃)
32	1	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ∈ 𝑃)
33		simpr 485	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
34		midexlem.1	. . . . 5 ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵))
35	34	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 − 𝐴) = (𝐶 − 𝐵))
36	10, 11, 12, 13, 14, 27, 28, 29, 31, 32, 33, 35	colmid 27049	. . 3 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐵 = ((𝑆‘𝐶)‘𝐴) ∨ 𝐴 = 𝐵))
37	8, 26, 36	mpjaodan 956	. 2 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
38	15	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
39	38	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐺 ∈ TarskiG)
40	39	ad2antrr 723	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐺 ∈ TarskiG)
41	40	ad2antrr 723	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐺 ∈ TarskiG)
42	41	adantr 481	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐺 ∈ TarskiG)
43		simprl 768	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ 𝑃)
44	9	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴 ∈ 𝑃)
45	44	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ 𝑃)
46	45	ad2antrr 723	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ 𝑃)
47	46	ad2antrr 723	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ 𝑃)
48	47	adantr 481	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ 𝑃)
49	30	ad3antrrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐵 ∈ 𝑃)
50	49	ad2antrr 723	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ 𝑃)
51	50	ad2antrr 723	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐵 ∈ 𝑃)
52	51	adantr 481	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ 𝑃)
53	42	ad2antrr 723	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐺 ∈ TarskiG)
54		simpllr 773	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ 𝑃)
55	54	ad2antrr 723	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ 𝑃)
56	1	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ∈ 𝑃)
57	56	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐶 ∈ 𝑃)
58	57	ad2antrr 723	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐶 ∈ 𝑃)
59	58	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐶 ∈ 𝑃)
60	59	adantr 481	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶 ∈ 𝑃)
61	60	ad2antrr 723	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ∈ 𝑃)
62	43	ad2antrr 723	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ 𝑃)
63		eqid 2738	. . . . . . . . 9 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
64	52	ad2antrr 723	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ 𝑃)
65	48	ad2antrr 723	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ 𝑃)
66		simpr 485	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 = 𝐴)
67	30	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵 ∈ 𝑃)
68		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
69	10, 12, 13, 38, 56, 44, 67, 68	ncolne1 26986	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ≠ 𝐴)
70	69	ad7antr 735	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶 ≠ 𝐴)
71	70	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ≠ 𝐴)
72	71	adantr 481	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐶 ≠ 𝐴)
73	72	necomd 2999	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐴 ≠ 𝐶)
74	66, 73	eqnetrd 3011	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 ≠ 𝐶)
75	53	adantr 481	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐺 ∈ TarskiG)
76	55	adantr 481	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ∈ 𝑃)
77	65	adantr 481	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐴 ∈ 𝑃)
78	61	adantr 481	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐶 ∈ 𝑃)
79		simplr 766	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝑞 ∈ 𝑃)
80	79	ad3antrrr 727	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑞 ∈ 𝑃)
81	80	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ 𝑃)
82	81	adantr 481	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑞 ∈ 𝑃)
83	68	ad9antr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
84	10, 13, 12, 53, 65, 64, 61, 83	ncolrot2 26924	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
85	15	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐺 ∈ TarskiG)
86	30	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐵 ∈ 𝑃)
87	9	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐴 ∈ 𝑃)
88	1	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐶 ∈ 𝑃)
89		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
90	10, 13, 12, 85, 86, 87, 88, 89	colcom 26919	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
91	90	stoic1a 1775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
92	91	ad9antr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
93	10, 12, 13, 53, 61, 64, 65, 92	ncolne1 26986	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ≠ 𝐵)
94	93	necomd 2999	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ≠ 𝐶)
95		simprl 768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ (𝐶𝐼𝑞))
96	95	ad3antrrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ (𝐶𝐼𝑞))
97	96	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ (𝐶𝐼𝑞))
98	10, 12, 13, 53, 61, 64, 81, 93, 97	btwnlng3 26982	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐶𝐿𝐵))
99	10, 12, 13, 53, 64, 61, 81, 94, 98	lncom 26983	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐵𝐿𝐶))
100	53	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐺 ∈ TarskiG)
101	61	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 ∈ 𝑃)
102	64	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ 𝑃)
103	97	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝑞))
104		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝑞 = 𝐶)
105	104	oveq2d 7291	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → (𝐶𝐼𝑞) = (𝐶𝐼𝐶))
106	103, 105	eleqtrd 2841	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶))
107	10, 11, 12, 100, 101, 102, 106	axtgbtwnid 26827	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 = 𝐵)
108	93	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 ≠ 𝐵)
109	108	neneqd 2948	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → ¬ 𝐶 = 𝐵)
110	107, 109	pm2.65da 814	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝑞 = 𝐶)
111	110	neqned 2950	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐶)
112	10, 12, 13, 53, 64, 61, 65, 81, 84, 99, 111	ncolncol 27007	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
113	10, 13, 12, 53, 61, 65, 81, 112	ncolcom 26922	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
114	113	adantr 481	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
115		simp-4r 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝑝 ∈ 𝑃)
116	115	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑝 ∈ 𝑃)
117	116	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑝 ∈ 𝑃)
118	117	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ 𝑃)
119		simp-4r 781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝)))
120	119	simprd 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 − 𝑞) = (𝐴 − 𝑝))
121	120	eqcomd 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 − 𝑝) = (𝐵 − 𝑞))
122	121	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑝) = (𝐵 − 𝑞))
123	10, 11, 12, 53, 65, 118, 64, 81, 122	tgcgrcomlr 26841	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 − 𝐴) = (𝑞 − 𝐵))
124		simpllr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
125	124	ad5antr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
126	125	simprd 496	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ≠ 𝑝)
127	126	necomd 2999	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ≠ 𝐴)
128	10, 11, 12, 53, 118, 65, 81, 64, 123, 127	tgcgrneq 26844	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐵)
129	10, 12, 13, 53, 61, 64, 65, 81, 92, 98, 128	ncolncol 27007	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
130	10, 12, 13, 53, 81, 64, 65, 129	ncolne2 26987	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐴)
131	130	necomd 2999	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ≠ 𝑞)
132		simp-4r 781	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
133	132	simpld 495	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐼𝑞))
134	10, 12, 13, 53, 65, 81, 55, 131, 133	btwnlng1 26980	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐿𝑞))
135	10, 12, 13, 53, 81, 65, 55, 130, 134	lncom 26983	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑞𝐿𝐴))
136	135	adantr 481	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ∈ (𝑞𝐿𝐴))
137		simpr 485	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ≠ 𝐴)
138	10, 12, 13, 75, 82, 77, 78, 76, 114, 136, 137	ncolncol 27007	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → ¬ (𝑟 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
139	10, 12, 13, 75, 76, 77, 78, 138	ncolne2 26987	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ≠ 𝐶)
140	74, 139	pm2.61dane 3032	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ≠ 𝐶)
141		simpllr 773	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶))))
142	141	simprd 496	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
143	142	simprd 496	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ (𝑟𝐼𝐶))
144	10, 13, 12, 53, 55, 62, 61, 143	btwncolg3 26918	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 ∈ (𝑟𝐿𝑥) ∨ 𝑟 = 𝑥))
145		simplr 766	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ 𝑃)
146		simplr 766	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
147	146	simprd 496	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝐵𝐼𝑝))
148	147	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐼𝑝))
149		simprl 768	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐼𝑞))
150	124	simpld 495	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
151	150	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
152	151	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ (𝐶𝐼𝑝))
153	34	ad8antr 737	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 − 𝐴) = (𝐶 − 𝐵))
154	153	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 − 𝐵) = (𝐶 − 𝐴))
155	10, 11, 12, 42, 48, 52	axtgcgrrflx 26823	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 − 𝐵) = (𝐵 − 𝐴))
156	10, 11, 12, 42, 60, 48, 117, 60, 52, 80, 52, 48, 70, 152, 96, 153, 121, 154, 155	axtg5seg 26826	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑝 − 𝐵) = (𝑞 − 𝐴))
157	10, 11, 12, 42, 117, 52, 80, 48, 156	tgcgrcomlr 26841	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 − 𝑝) = (𝐴 − 𝑞))
158	157	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑝) = (𝐴 − 𝑞))
159		simprr 770	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)
160	10, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159	cgr3simp2 26882	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝑝) = (𝑠 − 𝑞))
161	10, 11, 12, 53, 64, 65	axtgcgrrflx 26823	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝐴) = (𝐴 − 𝐵))
162	10, 11, 12, 53, 64, 55, 118, 65, 65, 145, 81, 64, 148, 149, 158, 160, 161, 123	tgifscgr 26869	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝐴) = (𝑠 − 𝐵))
163		simp-10l 792	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝜑)
164	125	simpld 495	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ (𝐶𝐼𝑝))
165	10, 12, 13, 53, 61, 65, 118, 71, 164	btwnlng3 26982	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ (𝐶𝐿𝐴))
166	10, 12, 13, 53, 61, 65, 64, 118, 83, 165, 127	ncolncol 27007	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
167	15	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐺 ∈ TarskiG)
168		simplr 766	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝑝 ∈ 𝑃)
169	9	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐴 ∈ 𝑃)
170	30	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐵 ∈ 𝑃)
171		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
172	10, 13, 12, 167, 168, 169, 170, 171	colrot1 26920	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
173	172	stoic1a 1775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
174	163, 118, 166, 173	syl21anc 835	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
175	10, 12, 13, 53, 118, 65, 64, 166	ncolne2 26987	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ≠ 𝐵)
176	175	necomd 2999	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ≠ 𝑝)
177	176	neneqd 2948	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝐵 = 𝑝)
178	10, 13, 12, 53, 65, 81, 55, 133	btwncolg1 26916	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐿𝑞) ∨ 𝐴 = 𝑞))
179	10, 11, 12, 53, 55, 65, 145, 64, 162	tgcgrcomlr 26841	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑟) = (𝐵 − 𝑠))
180	120	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑞) = (𝐴 − 𝑝))
181	10, 11, 12, 53, 118, 81	axtgcgrrflx 26823	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 − 𝑞) = (𝑞 − 𝑝))
182	10, 11, 12, 53, 64, 55, 118, 81, 65, 145, 81, 118, 148, 149, 158, 160, 180, 181	tgifscgr 26869	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝑞) = (𝑠 − 𝑝))
183	10, 11, 12, 53, 65, 145, 81, 149	tgbtwncom 26849	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝑞𝐼𝐴))
184	10, 11, 12, 42, 52, 54, 117, 147	tgbtwncom 26849	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝑝𝐼𝐵))
185	184	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑝𝐼𝐵))
186	160	eqcomd 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝑞) = (𝑟 − 𝑝))
187	10, 11, 12, 53, 145, 81, 55, 118, 186	tgcgrcomlr 26841	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 − 𝑠) = (𝑝 − 𝑟))
188	10, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159	cgr3simp1 26881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑟) = (𝐴 − 𝑠))
189	188	eqcomd 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑠) = (𝐵 − 𝑟))
190	10, 11, 12, 53, 65, 145, 64, 55, 189	tgcgrcomlr 26841	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝐴) = (𝑟 − 𝐵))
191	10, 11, 12, 53, 81, 145, 65, 118, 55, 64, 183, 185, 187, 190	tgcgrextend 26846	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 − 𝐴) = (𝑝 − 𝐵))
192	10, 11, 63, 53, 65, 55, 81, 64, 145, 118, 179, 182, 191	trgcgr 26877	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐴𝑟𝑞”⟩(cgrG‘𝐺)⟨“𝐵𝑠𝑝”⟩)
193	10, 13, 12, 53, 65, 55, 81, 63, 64, 145, 118, 178, 192	lnxfr 26927	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 ∈ (𝐵𝐿𝑝) ∨ 𝐵 = 𝑝))
194	193	orcomd 868	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 = 𝑝 ∨ 𝑠 ∈ (𝐵𝐿𝑝)))
195	194	ord 861	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (¬ 𝐵 = 𝑝 → 𝑠 ∈ (𝐵𝐿𝑝)))
196	177, 195	mpd 15	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐵𝐿𝑝))
197	10, 12, 13, 53, 64, 118, 55, 176, 148	btwnlng1 26980	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐿𝑝))
198	10, 12, 13, 53, 65, 81, 145, 131, 149	btwnlng1 26980	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐿𝑞))
199	10, 12, 13, 53, 64, 118, 65, 81, 174, 196, 197, 198, 134	tglineinteq 27006	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 = 𝑟)
200	199	oveq1d 7290	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝐵) = (𝑟 − 𝐵))
201	162, 200	eqtr2d 2779	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝐵) = (𝑟 − 𝐴))
202	154	ad2antrr 723	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 − 𝐵) = (𝐶 − 𝐴))
203	10, 13, 12, 53, 55, 61, 62, 63, 64, 65, 11, 140, 144, 201, 202	lncgr 26930	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 − 𝐵) = (𝑥 − 𝐴))
204	10, 11, 12, 63, 42, 52, 54, 117, 48, 80, 147, 157	tgcgrxfr 26879	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → ∃𝑠 ∈ 𝑃 (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩))
205	203, 204	r19.29a 3218	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑥 − 𝐵) = (𝑥 − 𝐴))
206		simprrl 778	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐴𝐼𝐵))
207	10, 11, 12, 42, 48, 43, 52, 206	tgbtwncom 26849	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐵𝐼𝐴))
208	10, 11, 12, 13, 14, 42, 43, 2, 48, 52, 205, 207	ismir 27020	. . . . . 6 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 = (𝑀‘𝐴))
209		simplr 766	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ 𝑃)
210		simprr 770	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ (𝐵𝐼𝑝))
211	10, 11, 12, 41, 59, 51, 116, 47, 209, 151, 210	axtgpasch 26828	. . . . . 6 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
212	208, 211	reximddv 3204	. . . . 5 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
213	10, 11, 12, 40, 58, 46, 115, 150	tgbtwncom 26849	. . . . . 6 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ (𝑝𝐼𝐶))
214	10, 11, 12, 40, 58, 50, 79, 95	tgbtwncom 26849	. . . . . 6 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ (𝑞𝐼𝐶))
215	10, 11, 12, 40, 115, 79, 58, 46, 50, 213, 214	axtgpasch 26828	. . . . 5 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → ∃𝑟 ∈ 𝑃 (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
216	212, 215	r19.29a 3218	. . . 4 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
217		simplr 766	. . . . 5 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝑝 ∈ 𝑃)
218	10, 11, 12, 39, 57, 49, 45, 217	axtgsegcon 26825	. . . 4 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → ∃𝑞 ∈ 𝑃 (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝)))
219	216, 218	r19.29a 3218	. . 3 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
220	10	fvexi 6788	. . . . . 6 ⊢ 𝑃 ∈ V
221	220	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝑃 ∈ V)
222	221, 56, 44, 69	nehash2 14188	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 2 ≤ (♯‘𝑃))
223	10, 11, 12, 38, 56, 44, 222	tgbtwndiff 26867	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑝 ∈ 𝑃 (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
224	219, 223	r19.29a 3218	. 2 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
225	37, 224	pm2.61dan 810	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∨ wo 844 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∃wrex 3065 Vcvv 3432 class class class wbr 5074 ‘cfv 6433 (class class class)co 7275 ⟨“cs3 14555 Basecbs 16912 distcds 16971 TarskiGcstrkg 26788 Itvcitv 26794 LineGclng 26795 cgrGccgrg 26871 pInvGcmir 27013

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-oadd 8301 df-er 8498 df-pm 8618 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-dju 9659 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-xnn0 12306 df-z 12320 df-uz 12583 df-fz 13240 df-fzo 13383 df-hash 14045 df-word 14218 df-concat 14274 df-s1 14301 df-s2 14561 df-s3 14562 df-trkgc 26809 df-trkgb 26810 df-trkgcb 26811 df-trkg 26814 df-cgrg 26872 df-mir 27014

This theorem is referenced by: footexALT 27079 footex 27082 colperpexlem3 27093 opphllem 27096

W3C validator