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 29197

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 29247 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 6911	. . . . . . . 8 ⊢ (𝑥 = 𝐶 → (𝑆‘𝑥) = (𝑆‘𝐶))
4	2, 3	eqtrid 2810	. . . . . . 7 ⊢ (𝑥 = 𝐶 → 𝑀 = (𝑆‘𝐶))
5	4	fveq1d 6913	. . . . . 6 ⊢ (𝑥 = 𝐶 → (𝑀‘𝐴) = ((𝑆‘𝐶)‘𝐴))
6	5	rspceeqv 3602	. . . . 5 ⊢ ((𝐶 ∈ 𝑃 ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
7	1, 6	sylan 592	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = ((𝑆‘𝐶)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
8	7	adantlr 728	. . 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 2763	. . . . . . . 8 ⊢ (𝑆‘𝐴) = (𝑆‘𝐴)
17	10, 11, 12, 13, 14, 15, 9, 16	mircinv 29173	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘𝐴)‘𝐴) = 𝐴)
18	17	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ((𝑆‘𝐴)‘𝐴) = 𝐴)
19		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵)
20	18, 19	eqtr2d 2799	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐵 = ((𝑆‘𝐴)‘𝐴))
21		fveq2 6911	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑆‘𝑥) = (𝑆‘𝐴))
22	2, 21	eqtrid 2810	. . . . . . 7 ⊢ (𝑥 = 𝐴 → 𝑀 = (𝑆‘𝐴))
23	22	fveq1d 6913	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑀‘𝐴) = ((𝑆‘𝐴)‘𝐴))
24	23	rspceeqv 3602	. . . . 5 ⊢ ((𝐴 ∈ 𝑃 ∧ 𝐵 = ((𝑆‘𝐴)‘𝐴)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
25	9, 20, 24	syl2an2r 698	. . . 4 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
26	25	adantlr 728	. . 3 ⊢ (((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝐴 = 𝐵) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
27	15	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
28		eqid 2763	. . . 4 ⊢ (𝑆‘𝐶) = (𝑆‘𝐶)
29	9	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴 ∈ 𝑃)
30		midexlem.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
31	30	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵 ∈ 𝑃)
32	1	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ∈ 𝑃)
33		simpr 490	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
34		midexlem.1	. . . . 5 ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐶 − 𝐵))
35	34	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐶 − 𝐴) = (𝐶 − 𝐵))
36	10, 11, 12, 13, 14, 27, 28, 29, 31, 32, 33, 35	colmid 29193	. . 3 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → (𝐵 = ((𝑆‘𝐶)‘𝐴) ∨ 𝐴 = 𝐵))
37	8, 26, 36	mpjaodan 973	. 2 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
38	15	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐺 ∈ TarskiG)
39	38	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐺 ∈ TarskiG)
40	39	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐺 ∈ TarskiG)
41	40	ad2antrr 739	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐺 ∈ TarskiG)
42	41	adantr 486	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐺 ∈ TarskiG)
43		simprl 783	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ 𝑃)
44	9	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐴 ∈ 𝑃)
45	44	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ 𝑃)
46	45	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ 𝑃)
47	46	ad2antrr 739	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ 𝑃)
48	47	adantr 486	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ 𝑃)
49	30	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐵 ∈ 𝑃)
50	49	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ 𝑃)
51	50	ad2antrr 739	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐵 ∈ 𝑃)
52	51	adantr 486	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ 𝑃)
53	42	ad2antrr 739	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐺 ∈ TarskiG)
54		simpllr 788	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ 𝑃)
55	54	ad2antrr 739	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ 𝑃)
56	1	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ∈ 𝑃)
57	56	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐶 ∈ 𝑃)
58	57	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐶 ∈ 𝑃)
59	58	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐶 ∈ 𝑃)
60	59	adantr 486	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶 ∈ 𝑃)
61	60	ad2antrr 739	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ∈ 𝑃)
62	43	ad2antrr 739	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ 𝑃)
63		eqid 2763	. . . . . . . . 9 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
64	52	ad2antrr 739	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ 𝑃)
65	48	ad2antrr 739	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ 𝑃)
66		simpr 490	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 = 𝐴)
67	30	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐵 ∈ 𝑃)
68		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
69	10, 12, 13, 38, 56, 44, 67, 68	ncolne1 29126	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝐶 ≠ 𝐴)
70	69	ad7antr 751	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐶 ≠ 𝐴)
71	70	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ≠ 𝐴)
72	71	adantr 486	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐶 ≠ 𝐴)
73	72	necomd 3014	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝐴 ≠ 𝐶)
74	66, 73	eqnetrd 3026	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 = 𝐴) → 𝑟 ≠ 𝐶)
75	53	adantr 486	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐺 ∈ TarskiG)
76	55	adantr 486	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ∈ 𝑃)
77	65	adantr 486	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐴 ∈ 𝑃)
78	61	adantr 486	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝐶 ∈ 𝑃)
79		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝑞 ∈ 𝑃)
80	79	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑞 ∈ 𝑃)
81	80	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ 𝑃)
82	81	adantr 486	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑞 ∈ 𝑃)
83	68	ad9antr 755	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
84	10, 13, 12, 53, 65, 64, 61, 83	ncolrot2 29059	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
85	15	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐺 ∈ TarskiG)
86	30	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐵 ∈ 𝑃)
87	9	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐴 ∈ 𝑃)
88	1	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → 𝐶 ∈ 𝑃)
89		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
90	10, 13, 12, 85, 86, 87, 88, 89	colcom 29054	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
91	90	stoic1a 1805	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
92	91	ad9antr 755	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
93	10, 12, 13, 53, 61, 64, 65, 92	ncolne1 29126	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐶 ≠ 𝐵)
94	93	necomd 3014	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ≠ 𝐶)
95		simprl 783	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ (𝐶𝐼𝑞))
96	95	ad3antrrr 743	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 ∈ (𝐶𝐼𝑞))
97	96	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ∈ (𝐶𝐼𝑞))
98	10, 12, 13, 53, 61, 64, 81, 93, 97	btwnlng3 29122	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐶𝐿𝐵))
99	10, 12, 13, 53, 64, 61, 81, 94, 98	lncom 29123	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ∈ (𝐵𝐿𝐶))
100	53	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐺 ∈ TarskiG)
101	61	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 ∈ 𝑃)
102	64	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ 𝑃)
103	97	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝑞))
104		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝑞 = 𝐶)
105	104	oveq2d 7462	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → (𝐶𝐼𝑞) = (𝐶𝐼𝐶))
106	103, 105	eleqtrd 2866	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶))
107	10, 11, 12, 100, 101, 102, 106	axtgbtwnid 28961	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 = 𝐵)
108	93	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → 𝐶 ≠ 𝐵)
109	108	neneqd 2964	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑞 = 𝐶) → ¬ 𝐶 = 𝐵)
110	107, 109	pm2.65da 829	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝑞 = 𝐶)
111	110	neqned 2966	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐶)
112	10, 12, 13, 53, 64, 61, 65, 81, 84, 99, 111	ncolncol 29148	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐶𝐿𝐴) ∨ 𝐶 = 𝐴))
113	10, 13, 12, 53, 61, 65, 81, 112	ncolcom 29057	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
114	113	adantr 486	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → ¬ (𝑞 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
115		simp-4r 796	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝑝 ∈ 𝑃)
116	115	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑝 ∈ 𝑃)
117	116	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑝 ∈ 𝑃)
118	117	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ 𝑃)
119		simp-4r 796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝)))
120	119	simprd 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 − 𝑞) = (𝐴 − 𝑝))
121	120	eqcomd 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 − 𝑝) = (𝐵 − 𝑞))
122	121	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑝) = (𝐵 − 𝑞))
123	10, 11, 12, 53, 65, 118, 64, 81, 122	tgcgrcomlr 28975	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 − 𝐴) = (𝑞 − 𝐵))
124		simpllr 788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
125	124	ad5antr 747	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
126	125	simprd 501	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ≠ 𝑝)
127	126	necomd 3014	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ≠ 𝐴)
128	10, 11, 12, 53, 118, 65, 81, 64, 123, 127	tgcgrneq 28978	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐵)
129	10, 12, 13, 53, 61, 64, 65, 81, 92, 98, 128	ncolncol 29148	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑞 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
130	10, 12, 13, 53, 81, 64, 65, 129	ncolne2 29127	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑞 ≠ 𝐴)
131	130	necomd 3014	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ≠ 𝑞)
132		simp-4r 796	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
133	132	simpld 500	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐼𝑞))
134	10, 12, 13, 53, 65, 81, 55, 131, 133	btwnlng1 29120	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐴𝐿𝑞))
135	10, 12, 13, 53, 81, 65, 55, 130, 134	lncom 29123	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑞𝐿𝐴))
136	135	adantr 486	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ∈ (𝑞𝐿𝐴))
137		simpr 490	. . . . . . . . . . . 12 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ≠ 𝐴)
138	10, 12, 13, 75, 82, 77, 78, 76, 114, 136, 137	ncolncol 29148	. . . . . . . . . . 11 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → ¬ (𝑟 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
139	10, 12, 13, 75, 76, 77, 78, 138	ncolne2 29127	. . . . . . . . . 10 ⊢ ((((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) ∧ 𝑟 ≠ 𝐴) → 𝑟 ≠ 𝐶)
140	74, 139	pm2.61dane 3046	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ≠ 𝐶)
141		simpllr 788	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶))))
142	141	simprd 501	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
143	142	simprd 501	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑥 ∈ (𝑟𝐼𝐶))
144	10, 13, 12, 53, 55, 62, 61, 143	btwncolg3 29053	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 ∈ (𝑟𝐿𝑥) ∨ 𝑟 = 𝑥))
145		simplr 781	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ 𝑃)
146		simplr 781	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
147	146	simprd 501	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝐵𝐼𝑝))
148	147	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐼𝑝))
149		simprl 783	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐼𝑞))
150	124	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
151	150	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝐴 ∈ (𝐶𝐼𝑝))
152	151	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐴 ∈ (𝐶𝐼𝑝))
153	34	ad8antr 753	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 − 𝐴) = (𝐶 − 𝐵))
154	153	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐶 − 𝐵) = (𝐶 − 𝐴))
155	10, 11, 12, 42, 48, 52	axtgcgrrflx 28957	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐴 − 𝐵) = (𝐵 − 𝐴))
156	10, 11, 12, 42, 60, 48, 117, 60, 52, 80, 52, 48, 70, 152, 96, 153, 121, 154, 155	axtg5seg 28960	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑝 − 𝐵) = (𝑞 − 𝐴))
157	10, 11, 12, 42, 117, 52, 80, 48, 156	tgcgrcomlr 28975	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝐵 − 𝑝) = (𝐴 − 𝑞))
158	157	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑝) = (𝐴 − 𝑞))
159		simprr 785	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)
160	10, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159	cgr3simp2 29017	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝑝) = (𝑠 − 𝑞))
161	10, 11, 12, 53, 64, 65	axtgcgrrflx 28957	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝐴) = (𝐴 − 𝐵))
162	10, 11, 12, 53, 64, 55, 118, 65, 65, 145, 81, 64, 148, 149, 158, 160, 161, 123	tgifscgr 29004	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝐴) = (𝑠 − 𝐵))
163		simp-10l 807	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝜑)
164	125	simpld 500	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐴 ∈ (𝐶𝐼𝑝))
165	10, 12, 13, 53, 61, 65, 118, 71, 164	btwnlng3 29122	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ∈ (𝐶𝐿𝐴))
166	10, 12, 13, 53, 61, 65, 64, 118, 83, 165, 127	ncolncol 29148	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
167	15	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐺 ∈ TarskiG)
168		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝑝 ∈ 𝑃)
169	9	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐴 ∈ 𝑃)
170	30	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → 𝐵 ∈ 𝑃)
171		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
172	10, 13, 12, 167, 168, 169, 170, 171	colrot1 29055	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴)) → (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
173	172	stoic1a 1805	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ ¬ (𝑝 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
174	163, 118, 166, 173	syl21anc 851	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ (𝐵 ∈ (𝑝𝐿𝐴) ∨ 𝑝 = 𝐴))
175	10, 12, 13, 53, 118, 65, 64, 166	ncolne2 29127	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑝 ≠ 𝐵)
176	175	necomd 3014	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝐵 ≠ 𝑝)
177	176	neneqd 2964	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ¬ 𝐵 = 𝑝)
178	10, 13, 12, 53, 65, 81, 55, 133	btwncolg1 29051	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 ∈ (𝐴𝐿𝑞) ∨ 𝐴 = 𝑞))
179	10, 11, 12, 53, 55, 65, 145, 64, 162	tgcgrcomlr 28975	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑟) = (𝐵 − 𝑠))
180	120	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑞) = (𝐴 − 𝑝))
181	10, 11, 12, 53, 118, 81	axtgcgrrflx 28957	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑝 − 𝑞) = (𝑞 − 𝑝))
182	10, 11, 12, 53, 64, 55, 118, 81, 65, 145, 81, 118, 148, 149, 158, 160, 180, 181	tgifscgr 29004	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝑞) = (𝑠 − 𝑝))
183	10, 11, 12, 53, 65, 145, 81, 149	tgbtwncom 28984	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝑞𝐼𝐴))
184	10, 11, 12, 42, 52, 54, 117, 147	tgbtwncom 28984	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑟 ∈ (𝑝𝐼𝐵))
185	184	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝑝𝐼𝐵))
186	160	eqcomd 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝑞) = (𝑟 − 𝑝))
187	10, 11, 12, 53, 145, 81, 55, 118, 186	tgcgrcomlr 28975	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 − 𝑠) = (𝑝 − 𝑟))
188	10, 11, 12, 63, 53, 64, 55, 118, 65, 145, 81, 159	cgr3simp1 29016	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 − 𝑟) = (𝐴 − 𝑠))
189	188	eqcomd 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐴 − 𝑠) = (𝐵 − 𝑟))
190	10, 11, 12, 53, 65, 145, 64, 55, 189	tgcgrcomlr 28975	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝐴) = (𝑟 − 𝐵))
191	10, 11, 12, 53, 81, 145, 65, 118, 55, 64, 183, 185, 187, 190	tgcgrextend 28980	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑞 − 𝐴) = (𝑝 − 𝐵))
192	10, 11, 63, 53, 65, 55, 81, 64, 145, 118, 179, 182, 191	trgcgr 29012	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → ⟨“𝐴𝑟𝑞”⟩(cgrG‘𝐺)⟨“𝐵𝑠𝑝”⟩)
193	10, 13, 12, 53, 65, 55, 81, 63, 64, 145, 118, 178, 192	lnxfr 29062	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 ∈ (𝐵𝐿𝑝) ∨ 𝐵 = 𝑝))
194	193	orcomd 885	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐵 = 𝑝 ∨ 𝑠 ∈ (𝐵𝐿𝑝)))
195	194	ord 878	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (¬ 𝐵 = 𝑝 → 𝑠 ∈ (𝐵𝐿𝑝)))
196	177, 195	mpd 16	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐵𝐿𝑝))
197	10, 12, 13, 53, 64, 118, 55, 176, 148	btwnlng1 29120	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑟 ∈ (𝐵𝐿𝑝))
198	10, 12, 13, 53, 65, 81, 145, 131, 149	btwnlng1 29120	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 ∈ (𝐴𝐿𝑞))
199	10, 12, 13, 53, 64, 118, 65, 81, 174, 196, 197, 198, 134	tglineinteq 29147	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → 𝑠 = 𝑟)
200	199	oveq1d 7461	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑠 − 𝐵) = (𝑟 − 𝐵))
201	162, 200	eqtr2d 2799	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑟 − 𝐵) = (𝑟 − 𝐴))
202	154	ad2antrr 739	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝐶 − 𝐵) = (𝐶 − 𝐴))
203	10, 13, 12, 53, 55, 61, 62, 63, 64, 65, 11, 140, 144, 201, 202	lncgr 29065	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) ∧ 𝑠 ∈ 𝑃) ∧ (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩)) → (𝑥 − 𝐵) = (𝑥 − 𝐴))
204	10, 11, 12, 63, 42, 52, 54, 117, 48, 80, 147, 157	tgcgrxfr 29014	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → ∃𝑠 ∈ 𝑃 (𝑠 ∈ (𝐴𝐼𝑞) ∧ ⟨“𝐵𝑟𝑝”⟩(cgrG‘𝐺)⟨“𝐴𝑠𝑞”⟩))
205	203, 204	r19.29a 3174	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → (𝑥 − 𝐵) = (𝑥 − 𝐴))
206		simprrl 793	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐴𝐼𝐵))
207	10, 11, 12, 42, 48, 43, 52, 206	tgbtwncom 28984	. . . . . . 7 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝑥 ∈ (𝐵𝐼𝐴))
208	10, 11, 12, 13, 14, 42, 43, 2, 48, 52, 205, 207	ismir 29164	. . . . . 6 ⊢ (((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) ∧ (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))) → 𝐵 = (𝑀‘𝐴))
209		simplr 781	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ 𝑃)
210		simprr 785	. . . . . . 7 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → 𝑟 ∈ (𝐵𝐼𝑝))
211	10, 11, 12, 41, 59, 51, 116, 47, 209, 151, 210	axtgpasch 28962	. . . . . 6 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑥 ∈ (𝑟𝐼𝐶)))
212	208, 211	reximddv 3182	. . . . 5 ⊢ ((((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) ∧ 𝑟 ∈ 𝑃) ∧ (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝))) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
213	10, 11, 12, 40, 58, 46, 115, 150	tgbtwncom 28984	. . . . . 6 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐴 ∈ (𝑝𝐼𝐶))
214	10, 11, 12, 40, 58, 50, 79, 95	tgbtwncom 28984	. . . . . 6 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → 𝐵 ∈ (𝑞𝐼𝐶))
215	10, 11, 12, 40, 115, 79, 58, 46, 50, 213, 214	axtgpasch 28962	. . . . 5 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → ∃𝑟 ∈ 𝑃 (𝑟 ∈ (𝐴𝐼𝑞) ∧ 𝑟 ∈ (𝐵𝐼𝑝)))
216	212, 215	r19.29a 3174	. . . 4 ⊢ ((((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) ∧ 𝑞 ∈ 𝑃) ∧ (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝))) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
217		simplr 781	. . . . 5 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝑝 ∈ 𝑃)
218	10, 11, 12, 39, 57, 49, 45, 217	axtgsegcon 28959	. . . 4 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → ∃𝑞 ∈ 𝑃 (𝐵 ∈ (𝐶𝐼𝑞) ∧ (𝐵 − 𝑞) = (𝐴 − 𝑝)))
219	216, 218	r19.29a 3174	. . 3 ⊢ ((((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
220	10	fvexi 6925	. . . . . 6 ⊢ 𝑃 ∈ V
221	220	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 𝑃 ∈ V)
222	221, 56, 44, 69	nehash2 14649	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → 2 ≤ (♯‘𝑃))
223	10, 11, 12, 38, 56, 44, 222	tgbtwndiff 29002	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑝 ∈ 𝑃 (𝐴 ∈ (𝐶𝐼𝑝) ∧ 𝐴 ≠ 𝑝))
224	219, 223	r19.29a 3174	. 2 ⊢ ((𝜑 ∧ ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))
225	37, 224	pm2.61dan 825	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 𝐵 = (𝑀‘𝐴))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∃wrex 3090 Vcvv 3454 class class class wbr 5106 ‘cfv 6561 (class class class)co 7446 ⟨“cs3 15024 Basecbs 17419 distcds 17469 TarskiGcstrkg 28922 Itvcitv 28928 LineGclng 28929 cgrGccgrg 29006 pInvGcmir 29157

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-oadd 8511 df-er 8748 df-pm 8881 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-dju 10012 df-card 10050 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-nn 12366 df-2 12435 df-3 12436 df-n0 12637 df-xnn0 12710 df-z 12724 df-uz 12996 df-fz 13670 df-fzo 13819 df-hash 14505 df-word 14689 df-concat 14746 df-s1 14773 df-s2 15030 df-s3 15031 df-trkgc 28943 df-trkgb 28944 df-trkgcb 28945 df-trkg 28948 df-cgrg 29007 df-mir 29158

This theorem is used by: footexALT 29226 footex 29229 colperpexlem3 29241 opphllem 29244

W3C validator