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 26472

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 26518 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 6664	. . . . . . . 8 ⊢ (𝑥 = 𝐶 → (𝑆‘𝑥) = (𝑆‘𝐶))
4	2, 3	syl5eq 2868	. . . . . . 7 ⊢ (𝑥 = 𝐶 → 𝑀 = (𝑆‘𝐶))
5	4	fveq1d 6666	. . . . . 6 ⊢ (𝑥 = 𝐶 → (𝑀‘𝐴) = ((𝑆‘𝐶)‘𝐴))
6	5	rspceeqv 3637	. . . . 5 ⊢ ((𝐶 ∈ 𝑃 ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
7	1, 6	sylan 582	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
8	7	adantlr 713	. . 3 ⊢ (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
9		midexlem.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
10		mirval.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
11		mirval.d	. . . . . . . 8 ⊢ − = (dist‘𝐺)
12		mirval.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
13		mirval.l	. . . . . . . 8 ⊢ 𝐿 = (LineG‘𝐺)
14		mirval.s	. . . . . . . 8 ⊢ 𝑆 = (pInvG‘𝐺)
15		mirval.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
16		eqid 2821	. . . . . . . 8 ⊢ (𝑆‘𝐴) = (𝑆‘𝐴)
17	10, 11, 12, 13, 14, 15, 9, 16	mircinv 26448	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝐴)‘𝐴) = 𝐴)
18	17	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ((𝑆‘𝐴)‘𝐴) = 𝐴)
19		simpr 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵)
20	18, 19	eqtr2d 2857	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐵 = ((𝑆‘𝐴)‘𝐴))
21		fveq2 6664	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑆‘𝑥) = (𝑆‘𝐴))
22	2, 21	syl5eq 2868	. . . . . . 7 ⊢ (𝑥 = 𝐴 → 𝑀 = (𝑆‘𝐴))
23	22	fveq1d 6666	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑀‘𝐴) = ((𝑆‘𝐴)‘𝐴))
24	23	rspceeqv 3637	. . . . 5 ⊢ ((𝐴 ∈ 𝑃 ∧ 𝐵 = ((𝑆‘𝐴)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
25	9, 20, 24	syl2an2r 683	. . . 4 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
26	25	adantlr 713	. . 3 ⊢ (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐴 = 𝐵) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
27	15	adantr 483	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
28		eqid 2821	. . . 4 ⊢ (𝑆‘𝐶) = (𝑆‘𝐶)
29	9	adantr 483	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴 ∈ 𝑃)
30		midexlem.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
31	30	adantr 483	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵 ∈ 𝑃)
32	1	adantr 483	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ∈ 𝑃)
33		simpr 487	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
34		midexlem.1	. . . . 5 ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵))
35	34	adantr 483	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 − 𝐴) = (𝐶 − 𝐵))
36	10, 11, 12, 13, 14, 27, 28, 29, 31, 32, 33, 35	colmid 26468	. . 3 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐵 = ((𝑆‘𝐶)‘𝐴) ∨ 𝐴 = 𝐵))
37	8, 26, 36	mpjaodan 955	. 2 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
38	15	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
39	38	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐺 ∈ TarskiG)
40	39	ad2antrr 724	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐺 ∈ TarskiG)
41	40	ad2antrr 724	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐺 ∈ TarskiG)
42	41	adantr 483	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐺 ∈ TarskiG)
43		simprl 769	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ 𝑃)
44	9	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴 ∈ 𝑃)
45	44	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ 𝑃)
46	45	ad2antrr 724	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ 𝑃)
47	46	ad2antrr 724	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ 𝑃)
48	47	adantr 483	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ 𝑃)
49	30	ad3antrrr 728	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐵 ∈ 𝑃)
50	49	ad2antrr 724	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ 𝑃)
51	50	ad2antrr 724	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐵 ∈ 𝑃)
52	51	adantr 483	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ 𝑃)
53	42	ad2antrr 724	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐺 ∈ TarskiG)
54		simpllr 774	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ 𝑃)
55	54	ad2antrr 724	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ 𝑃)
56	1	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ∈ 𝑃)
57	56	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐶 ∈ 𝑃)
58	57	ad2antrr 724	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐶 ∈ 𝑃)
59	58	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐶 ∈ 𝑃)
60	59	adantr 483	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶 ∈ 𝑃)
61	60	ad2antrr 724	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ∈ 𝑃)
62	43	ad2antrr 724	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ 𝑃)
63		eqid 2821	. . . . . . . . 9 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
64	52	ad2antrr 724	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ 𝑃)
65	48	ad2antrr 724	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ 𝑃)
66		simpr 487	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 = 𝐴)
67	30	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵 ∈ 𝑃)
68		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
69	10, 12, 13, 38, 56, 44, 67, 68	ncolne1 26405	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ≠ 𝐴)
70	69	ad7antr 736	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶 ≠ 𝐴)
71	70	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ≠ 𝐴)
72	71	adantr 483	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐶 ≠ 𝐴)
73	72	necomd 3071	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐴 ≠ 𝐶)
74	66, 73	eqnetrd 3083	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 ≠ 𝐶)
75	53	adantr 483	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐺 ∈ TarskiG)
76	55	adantr 483	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ∈ 𝑃)
77	65	adantr 483	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐴 ∈ 𝑃)
78	61	adantr 483	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐶 ∈ 𝑃)
79		simplr 767	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝑞 ∈ 𝑃)
80	79	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑞 ∈ 𝑃)
81	80	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ 𝑃)
82	81	adantr 483	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑞 ∈ 𝑃)
83	68	ad9antr 740	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
84	10, 13, 12, 53, 65, 64, 61, 83	ncolrot2 26343	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
85	15	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐺 ∈ TarskiG)
86	30	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐵 ∈ 𝑃)
87	9	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐴 ∈ 𝑃)
88	1	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐶 ∈ 𝑃)
89		simpr 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
90	10, 13, 12, 85, 86, 87, 88, 89	colcom 26338	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
91	90	stoic1a 1769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
92	91	ad9antr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
93	10, 12, 13, 53, 61, 64, 65, 92	ncolne1 26405	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ≠ 𝐵)
94	93	necomd 3071	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ≠ 𝐶)
95		simprl 769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ (𝐶𝐼𝑞))
96	95	ad3antrrr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ (𝐶𝐼𝑞))
97	96	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ (𝐶𝐼𝑞))
98	10, 12, 13, 53, 61, 64, 81, 93, 97	btwnlng3 26401	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐶𝐿𝐵))
99	10, 12, 13, 53, 64, 61, 81, 94, 98	lncom 26402	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐵𝐿𝐶))
100	53	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐺 ∈ TarskiG)
101	61	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 ∈ 𝑃)
102	64	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ 𝑃)
103	97	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝑞))
104		simpr 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝑞 = 𝐶)
105	104	oveq2d 7166	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → (𝐶𝐼𝑞) = (𝐶𝐼𝐶))
106	103, 105	eleqtrd 2915	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶))
107	10, 11, 12, 100, 101, 102, 106	axtgbtwnid 26246	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 = 𝐵)
108	93	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 ≠ 𝐵)
109	108	neneqd 3021	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → ¬ 𝐶 = 𝐵)
110	107, 109	pm2.65da 815	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝑞 = 𝐶)
111	110	neqned 3023	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐶)
112	10, 12, 13, 53, 64, 61, 65, 81, 84, 99, 111	ncolncol 26426	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
113	10, 13, 12, 53, 61, 65, 81, 112	ncolcom 26341	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
114	113	adantr 483	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
115		simp-4r 782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝑝 ∈ 𝑃)
116	115	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑝 ∈ 𝑃)
117	116	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑝 ∈ 𝑃)
118	117	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ 𝑃)
119		simp-4r 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝)))
120	119	simprd 498	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 − 𝑞) = (𝐴 − 𝑝))
121	120	eqcomd 2827	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 − 𝑝) = (𝐵 − 𝑞))
122	121	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑝) = (𝐵 − 𝑞))
123	10, 11, 12, 53, 65, 118, 64, 81, 122	tgcgrcomlr 26260	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 − 𝐴) = (𝑞 − 𝐵))
124		simpllr 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
125	124	ad5antr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
126	125	simprd 498	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ≠ 𝑝)
127	126	necomd 3071	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ≠ 𝐴)
128	10, 11, 12, 53, 118, 65, 81, 64, 123, 127	tgcgrneq 26263	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐵)
129	10, 12, 13, 53, 61, 64, 65, 81, 92, 98, 128	ncolncol 26426	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
130	10, 12, 13, 53, 81, 64, 65, 129	ncolne2 26406	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐴)
131	130	necomd 3071	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ≠ 𝑞)
132		simp-4r 782	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
133	132	simpld 497	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐼𝑞))
134	10, 12, 13, 53, 65, 81, 55, 131, 133	btwnlng1 26399	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐿𝑞))
135	10, 12, 13, 53, 81, 65, 55, 130, 134	lncom 26402	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑞𝐿𝐴))
136	135	adantr 483	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ∈ (𝑞𝐿𝐴))
137		simpr 487	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ≠ 𝐴)
138	10, 12, 13, 75, 82, 77, 78, 76, 114, 136, 137	ncolncol 26426	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → ¬ (𝑟 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
139	10, 12, 13, 75, 76, 77, 78, 138	ncolne2 26406	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ≠ 𝐶)
140	74, 139	pm2.61dane 3104	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ≠ 𝐶)
141		simpllr 774	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶))))
142	141	simprd 498	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
143	142	simprd 498	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ (𝑟𝐼𝐶))
144	10, 13, 12, 53, 55, 62, 61, 143	btwncolg3 26337	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 ∈ (𝑟𝐿𝑥) ∨ 𝑟 = 𝑥))
145		simplr 767	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ 𝑃)
146		simplr 767	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
147	146	simprd 498	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝐵𝐼𝑝))
148	147	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐼𝑝))
149		simprl 769	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐼𝑞))
150	124	simpld 497	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
151	150	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
152	151	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ (𝐶𝐼𝑝))
153	34	ad8antr 738	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 − 𝐴) = (𝐶 − 𝐵))
154	153	eqcomd 2827	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 − 𝐵) = (𝐶 − 𝐴))
155	10, 11, 12, 42, 48, 52	axtgcgrrflx 26242	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 − 𝐵) = (𝐵 − 𝐴))
156	10, 11, 12, 42, 60, 48, 117, 60, 52, 80, 52, 48, 70, 152, 96, 153, 121, 154, 155	axtg5seg 26245	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑝 − 𝐵) = (𝑞 − 𝐴))
157	10, 11, 12, 42, 117, 52, 80, 48, 156	tgcgrcomlr 26260	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 − 𝑝) = (𝐴 − 𝑞))
158	157	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑝) = (𝐴 − 𝑞))
159		simprr 771	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)
160	10, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159	cgr3simp2 26301	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝑝) = (𝑠 − 𝑞))
161	10, 11, 12, 53, 64, 65	axtgcgrrflx 26242	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝐴) = (𝐴 − 𝐵))
162	10, 11, 12, 53, 64, 55, 118, 65, 65, 145, 81, 64, 148, 149, 158, 160, 161, 123	tgifscgr 26288	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝐴) = (𝑠 − 𝐵))
163		simp-10l 793	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝜑)
164	125	simpld 497	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ (𝐶𝐼𝑝))
165	10, 12, 13, 53, 61, 65, 118, 71, 164	btwnlng3 26401	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ (𝐶𝐿𝐴))
166	10, 12, 13, 53, 61, 65, 64, 118, 83, 165, 127	ncolncol 26426	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
167	15	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐺 ∈ TarskiG)
168		simplr 767	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝑝 ∈ 𝑃)
169	9	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐴 ∈ 𝑃)
170	30	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐵 ∈ 𝑃)
171		simpr 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
172	10, 13, 12, 167, 168, 169, 170, 171	colrot1 26339	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
173	172	stoic1a 1769	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
174	163, 118, 166, 173	syl21anc 835	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
175	10, 12, 13, 53, 118, 65, 64, 166	ncolne2 26406	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ≠ 𝐵)
176	175	necomd 3071	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ≠ 𝑝)
177	176	neneqd 3021	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝐵 = 𝑝)
178	10, 13, 12, 53, 65, 81, 55, 133	btwncolg1 26335	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐿𝑞) ∨ 𝐴 = 𝑞))
179	10, 11, 12, 53, 55, 65, 145, 64, 162	tgcgrcomlr 26260	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑟) = (𝐵 − 𝑠))
180	120	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑞) = (𝐴 − 𝑝))
181	10, 11, 12, 53, 118, 81	axtgcgrrflx 26242	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 − 𝑞) = (𝑞 − 𝑝))
182	10, 11, 12, 53, 64, 55, 118, 81, 65, 145, 81, 118, 148, 149, 158, 160, 180, 181	tgifscgr 26288	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝑞) = (𝑠 − 𝑝))
183	10, 11, 12, 53, 65, 145, 81, 149	tgbtwncom 26268	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝑞𝐼𝐴))
184	10, 11, 12, 42, 52, 54, 117, 147	tgbtwncom 26268	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝑝𝐼𝐵))
185	184	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑝𝐼𝐵))
186	160	eqcomd 2827	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝑞) = (𝑟 − 𝑝))
187	10, 11, 12, 53, 145, 81, 55, 118, 186	tgcgrcomlr 26260	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 − 𝑠) = (𝑝 − 𝑟))
188	10, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159	cgr3simp1 26300	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑟) = (𝐴 − 𝑠))
189	188	eqcomd 2827	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑠) = (𝐵 − 𝑟))
190	10, 11, 12, 53, 65, 145, 64, 55, 189	tgcgrcomlr 26260	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝐴) = (𝑟 − 𝐵))
191	10, 11, 12, 53, 81, 145, 65, 118, 55, 64, 183, 185, 187, 190	tgcgrextend 26265	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 − 𝐴) = (𝑝 − 𝐵))
192	10, 11, 63, 53, 65, 55, 81, 64, 145, 118, 179, 182, 191	trgcgr 26296	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐴𝑟𝑞”⟩(cgrG‘𝐺)⟨“𝐵𝑠𝑝”⟩)
193	10, 13, 12, 53, 65, 55, 81, 63, 64, 145, 118, 178, 192	lnxfr 26346	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 ∈ (𝐵𝐿𝑝) ∨ 𝐵 = 𝑝))
194	193	orcomd 867	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 = 𝑝 ∨ 𝑠 ∈ (𝐵𝐿𝑝)))
195	194	ord 860	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (¬ 𝐵 = 𝑝 → 𝑠 ∈ (𝐵𝐿𝑝)))
196	177, 195	mpd 15	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐵𝐿𝑝))
197	10, 12, 13, 53, 64, 118, 55, 176, 148	btwnlng1 26399	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐿𝑝))
198	10, 12, 13, 53, 65, 81, 145, 131, 149	btwnlng1 26399	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐿𝑞))
199	10, 12, 13, 53, 64, 118, 65, 81, 174, 196, 197, 198, 134	tglineinteq 26425	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 = 𝑟)
200	199	oveq1d 7165	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝐵) = (𝑟 − 𝐵))
201	162, 200	eqtr2d 2857	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝐵) = (𝑟 − 𝐴))
202	154	ad2antrr 724	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 − 𝐵) = (𝐶 − 𝐴))
203	10, 13, 12, 53, 55, 61, 62, 63, 64, 65, 11, 140, 144, 201, 202	lncgr 26349	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 − 𝐵) = (𝑥 − 𝐴))
204	10, 11, 12, 63, 42, 52, 54, 117, 48, 80, 147, 157	tgcgrxfr 26298	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → ∃𝑠 ∈ 𝑃 (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩))
205	203, 204	r19.29a 3289	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑥 − 𝐵) = (𝑥 − 𝐴))
206		simprrl 779	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐴𝐼𝐵))
207	10, 11, 12, 42, 48, 43, 52, 206	tgbtwncom 26268	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐵𝐼𝐴))
208	10, 11, 12, 13, 14, 42, 43, 2, 48, 52, 205, 207	ismir 26439	. . . . . 6 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 = (𝑀‘𝐴))
209		simplr 767	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ 𝑃)
210		simprr 771	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ (𝐵𝐼𝑝))
211	10, 11, 12, 41, 59, 51, 116, 47, 209, 151, 210	axtgpasch 26247	. . . . . 6 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
212	208, 211	reximddv 3275	. . . . 5 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
213	10, 11, 12, 40, 58, 46, 115, 150	tgbtwncom 26268	. . . . . 6 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ (𝑝𝐼𝐶))
214	10, 11, 12, 40, 58, 50, 79, 95	tgbtwncom 26268	. . . . . 6 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ (𝑞𝐼𝐶))
215	10, 11, 12, 40, 115, 79, 58, 46, 50, 213, 214	axtgpasch 26247	. . . . 5 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → ∃𝑟 ∈ 𝑃 (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
216	212, 215	r19.29a 3289	. . . 4 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
217		simplr 767	. . . . 5 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝑝 ∈ 𝑃)
218	10, 11, 12, 39, 57, 49, 45, 217	axtgsegcon 26244	. . . 4 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → ∃𝑞 ∈ 𝑃 (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝)))
219	216, 218	r19.29a 3289	. . 3 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
220	10	fvexi 6678	. . . . . 6 ⊢ 𝑃 ∈ V
221	220	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝑃 ∈ V)
222	221, 56, 44, 69	nehash2 13826	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 2 ≤ (♯‘𝑃))
223	10, 11, 12, 38, 56, 44, 222	tgbtwndiff 26286	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑝 ∈ 𝑃 (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
224	219, 223	r19.29a 3289	. 2 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
225	37, 224	pm2.61dan 811	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 ∨ wo 843 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∃wrex 3139 Vcvv 3494 class class class wbr 5058 ‘cfv 6349 (class class class)co 7150 ⟨“cs3 14198 Basecbs 16477 distcds 16568 TarskiGcstrkg 26210 Itvcitv 26216 LineGclng 26217 cgrGccgrg 26290 pInvGcmir 26432

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4869 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-oadd 8100 df-er 8283 df-pm 8403 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-dju 9324 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-xnn0 11962 df-z 11976 df-uz 12238 df-fz 12887 df-fzo 13028 df-hash 13685 df-word 13856 df-concat 13917 df-s1 13944 df-s2 14204 df-s3 14205 df-trkgc 26228 df-trkgb 26229 df-trkgcb 26230 df-trkg 26233 df-cgrg 26291 df-mir 26433

This theorem is referenced by: footexALT 26498 footex 26501 colperpexlem3 26512 opphllem 26515

W3C validator