miriso - Metamath Proof Explorer

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

Theorem miriso 29024

Description: The point inversion function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 7.13 of [Schwabhauser] p. 50. (Contributed by Thierry Arnoux, 6-Jun-2019.)

**Hypotheses**
Ref	Expression
mirval.p	⊢ 𝑃 = (Base‘𝐺)
mirval.d	⊢ − = (dist‘𝐺)
mirval.i	⊢ 𝐼 = (Itv‘𝐺)
mirval.l	⊢ 𝐿 = (LineG‘𝐺)
mirval.s	⊢ 𝑆 = (pInvG‘𝐺)
mirval.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
mirval.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
mirfv.m	⊢ 𝑀 = (𝑆‘𝐴)
miriso.1	⊢ (𝜑 → 𝑋 ∈ 𝑃)
miriso.2	⊢ (𝜑 → 𝑌 ∈ 𝑃)

**Assertion**
Ref	Expression
miriso	⊢ (𝜑 → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))

Proof of Theorem miriso Dummy variables 𝑥 𝑦 𝑧 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 = 𝐴)
2	1	oveq1d 7429	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝑋 − 𝑌) = (𝐴 − 𝑌))
3		mirval.p	. . . 4 ⊢ 𝑃 = (Base‘𝐺)
4		mirval.d	. . . 4 ⊢ − = (dist‘𝐺)
5		mirval.i	. . . 4 ⊢ 𝐼 = (Itv‘𝐺)
6		mirval.l	. . . 4 ⊢ 𝐿 = (LineG‘𝐺)
7		mirval.s	. . . 4 ⊢ 𝑆 = (pInvG‘𝐺)
8		mirval.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
9	8	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐺 ∈ TarskiG)
10		mirval.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
11	10	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ 𝑃)
12		mirfv.m	. . . 4 ⊢ 𝑀 = (𝑆‘𝐴)
13		miriso.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
14	13	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑌 ∈ 𝑃)
15	3, 4, 5, 6, 7, 9, 11, 12, 14	mircgr 29011	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − (𝑀‘𝑌)) = (𝐴 − 𝑌))
16		miriso.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
17	16	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ 𝑃)
18	1	eqcomd 2766	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = 𝑋)
19	18	oveq2d 7430	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − 𝐴) = (𝐴 − 𝑋))
20	3, 4, 5, 9, 11, 17	tgbtwntriv1 28836	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐼𝑋))
21	3, 4, 5, 6, 7, 9, 11, 12, 17, 11, 19, 20	ismir 29013	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = (𝑀‘𝑋))
22	21	oveq1d 7429	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − (𝑀‘𝑌)) = ((𝑀‘𝑋) − (𝑀‘𝑌)))
23	2, 15, 22	3eqtr2rd 2802	. 2 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
24	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝐺 ∈ TarskiG)
25	24	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝐺 ∈ TarskiG)
26	25	ad6antr 749	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐺 ∈ TarskiG)
27		simplr 781	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝑥 ∈ 𝑃)
28	27	ad6antr 749	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑥 ∈ 𝑃)
29	16	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝑋 ∈ 𝑃)
30	29	ad8antr 753	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ 𝑃)
31	10	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝐴 ∈ 𝑃)
32	31	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝐴 ∈ 𝑃)
33	32	ad6antr 749	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ 𝑃)
34	13	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝑌 ∈ 𝑃)
35	34	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝑌 ∈ 𝑃)
36	35	ad6antr 749	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ 𝑃)
37		simp-4r 796	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑧 ∈ 𝑃)
38	3, 4, 5, 6, 7, 24, 31, 12, 29	mircl 29015	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → (𝑀‘𝑋) ∈ 𝑃)
39	38	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → (𝑀‘𝑋) ∈ 𝑃)
40	39	ad6antr 749	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ 𝑃)
41	3, 4, 5, 6, 7, 24, 31, 12, 34	mircl 29015	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → (𝑀‘𝑌) ∈ 𝑃)
42	41	ad8antr 753	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ 𝑃)
43	3, 4, 5, 6, 7, 26, 33, 12, 30	mirbtwn 29012	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ ((𝑀‘𝑋)𝐼𝑋))
44		simp-7r 802	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴)))
45	44	simpld 500	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥))
46	3, 4, 5, 26, 40, 33, 30, 28, 43, 45	tgbtwnexch3 28839	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝐴𝐼𝑥))
47	3, 4, 5, 26, 33, 30, 28, 46	tgbtwncom 28833	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝑥𝐼𝐴))
48	3, 4, 5, 26, 40, 30, 28, 45	tgbtwncom 28833	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝑥𝐼(𝑀‘𝑋)))
49	3, 4, 5, 26, 40, 33, 30, 43	tgbtwncom 28833	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑋)))
50	3, 4, 5, 26, 28, 30, 33, 40, 48, 49	tgbtwnexch2 28841	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑥𝐼(𝑀‘𝑋)))
51		simpllr 788	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
52	51	simpld 500	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝑥𝐼𝑧))
53	3, 4, 5, 26, 28, 33, 40, 37, 50, 52	tgbtwnexch3 28839	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝐴𝐼𝑧))
54	3, 4, 5, 26, 33, 40, 37, 53	tgbtwncom 28833	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝑧𝐼𝐴))
55		simp-4r 796	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → 𝑦 ∈ 𝑃)
56	55	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑦 ∈ 𝑃)
57	3, 4, 5, 6, 7, 26, 33, 12, 36	mirbtwn 29012	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ ((𝑀‘𝑌)𝐼𝑌))
58		simp-5r 798	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
59	58	simpld 500	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦))
60	3, 4, 5, 26, 42, 33, 36, 56, 57, 59	tgbtwnexch3 28839	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝐴𝐼𝑦))
61	3, 4, 5, 26, 33, 36, 56, 60	tgbtwncom 28833	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝑦𝐼𝐴))
62	3, 4, 5, 6, 7, 26, 33, 12, 30	mircgr 29011	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑋)) = (𝐴 − 𝑋))
63	58	simprd 501	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝑦) = (𝑋 − 𝐴))
64	3, 4, 5, 26, 36, 56, 30, 33, 63	tgcgrcomlr 28824	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝑌) = (𝐴 − 𝑋))
65	62, 64	eqtr4d 2798	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑋)) = (𝑦 − 𝑌))
66	51	simprd 501	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))
67	3, 4, 5, 26, 33, 40, 37, 56, 36, 33, 53, 61, 65, 66	tgcgrextend 28829	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑧) = (𝑦 − 𝐴))
68	44	simprd 501	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝑥) = (𝑌 − 𝐴))
69	68	eqcomd 2766	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝐴) = (𝑋 − 𝑥))
70	3, 4, 5, 26, 56, 36, 33, 33, 30, 28, 61, 46, 64, 69	tgcgrextend 28829	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝐴 − 𝑥))
71	67, 70	eqtr2d 2796	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑥) = (𝐴 − 𝑧))
72	3, 4, 5, 26, 33, 28, 33, 37, 71	tgcgrcomlr 28824	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝑧 − 𝐴))
73	62	eqcomd 2766	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑋) = (𝐴 − (𝑀‘𝑋)))
74	3, 4, 5, 26, 33, 30, 33, 40, 73	tgcgrcomlr 28824	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝐴) = ((𝑀‘𝑋) − 𝐴))
75		simplr 781	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑡 ∈ 𝑃)
76	3, 4, 5, 26, 42, 36, 56, 59	tgbtwncom 28833	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝑦𝐼(𝑀‘𝑌)))
77	3, 4, 5, 26, 42, 33, 36, 57	tgbtwncom 28833	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑌𝐼(𝑀‘𝑌)))
78	3, 4, 5, 26, 56, 36, 33, 42, 76, 77	tgbtwnexch2 28841	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑦𝐼(𝑀‘𝑌)))
79		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
80	79	simpld 500	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝑦𝐼𝑡))
81	3, 4, 5, 26, 56, 33, 42, 75, 78, 80	tgbtwnexch3 28839	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝐴𝐼𝑡))
82	3, 4, 5, 26, 33, 42, 75, 81	tgbtwncom 28833	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝑡𝐼𝐴))
83	3, 4, 5, 26, 30, 28, 36, 33, 68	tgcgrcomlr 28824	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑋) = (𝐴 − 𝑌))
84	3, 4, 5, 6, 7, 26, 33, 12, 36	mircgr 29011	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑌)) = (𝐴 − 𝑌))
85	83, 84	eqtr4d 2798	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑋) = (𝐴 − (𝑀‘𝑌)))
86	79	simprd 501	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))
87	86	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝐴) = ((𝑀‘𝑌) − 𝑡))
88	3, 4, 5, 26, 28, 30, 33, 33, 42, 75, 47, 81, 85, 87	tgcgrextend 28829	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝐴 − 𝑡))
89	3, 4, 5, 26, 33, 75	axtgcgrrflx 28806	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑡) = (𝑡 − 𝐴))
90	88, 89	eqtrd 2795	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝑡 − 𝐴))
91	3, 4, 5, 26, 28, 33, 75, 33, 90	tgcgrcomlr 28824	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑥) = (𝐴 − 𝑡))
92	70, 91, 89	3eqtrd 2799	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝑡 − 𝐴))
93	3, 4, 5, 26, 33, 42, 33, 36, 84	tgcgrcomlr 28824	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) − 𝐴) = (𝑌 − 𝐴))
94	93	eqcomd 2766	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝐴) = ((𝑀‘𝑌) − 𝐴))
95	3, 4, 5, 26, 75, 37	axtgcgrrflx 28806	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑡 − 𝑧) = (𝑧 − 𝑡))
96		simp-9r 806	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ≠ 𝐴)
97	96	neneqd 2960	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ¬ 𝑋 = 𝐴)
98	26	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐺 ∈ TarskiG)
99	33	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 ∈ 𝑃)
100	30	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ 𝑃)
101	46	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝑥))
102		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
103	102	oveq2d 7430	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → (𝐴𝐼𝑥) = (𝐴𝐼𝐴))
104	101, 103	eleqtrd 2862	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝐴))
105	3, 4, 5, 98, 99, 100, 104	axtgbtwnid 28810	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 = 𝑋)
106	105	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 = 𝐴)
107	97, 106	mtand 828	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ¬ 𝑥 = 𝐴)
108	107	neqned 2962	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑥 ≠ 𝐴)
109	3, 4, 5, 26, 28, 33, 40, 37, 50, 52	tgbtwnexch 28843	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑥𝐼𝑧))
110	3, 4, 5, 26, 56, 33, 42, 75, 78, 80	tgbtwnexch 28843	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑦𝐼𝑡))
111	3, 4, 5, 26, 56, 33, 75, 110	tgbtwncom 28833	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑡𝐼𝑦))
112	3, 4, 5, 26, 56, 33	axtgcgrrflx 28806	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝐴 − 𝑦))
113	67, 112	eqtrd 2795	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑧) = (𝐴 − 𝑦))
114	3, 4, 5, 26, 28, 75	axtgcgrrflx 28806	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑡) = (𝑡 − 𝑥))
115	91	eqcomd 2766	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑡) = (𝐴 − 𝑥))
116	3, 4, 5, 26, 28, 33, 37, 75, 33, 56, 75, 28, 108, 109, 111, 90, 113, 114, 115	axtg5seg 28809	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑧 − 𝑡) = (𝑦 − 𝑥))
117	95, 116	eqtr2d 2796	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝑥) = (𝑡 − 𝑧))
118	3, 4, 5, 26, 56, 36, 33, 28, 75, 42, 33, 37, 61, 82, 92, 94, 117, 71	tgifscgr 28853	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝑥) = ((𝑀‘𝑌) − 𝑧))
119	3, 4, 5, 26, 36, 28, 42, 37, 118	tgcgrcomlr 28824	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑌) = (𝑧 − (𝑀‘𝑌)))
120	84	eqcomd 2766	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑌) = (𝐴 − (𝑀‘𝑌)))
121	3, 4, 5, 26, 28, 30, 33, 36, 37, 40, 33, 42, 47, 54, 72, 74, 119, 120	tgifscgr 28853	. . . . . . 7 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝑌) = ((𝑀‘𝑋) − (𝑀‘𝑌)))
122	121	eqcomd 2766	. . . . . 6 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
123		simp-6l 799	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → (𝜑 ∧ 𝑋 ≠ 𝐴))
124		simpllr 788	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
125	24	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝐺 ∈ TarskiG)
126		simplr 781	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝑦 ∈ 𝑃)
127	41	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ 𝑃)
128	29	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝑋 ∈ 𝑃)
129	31	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝐴 ∈ 𝑃)
130	3, 4, 5, 125, 126, 127, 128, 129	axtgsegcon 28808	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ∃𝑡 ∈ 𝑃 ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
131	123, 55, 124, 130	syl21anc 851	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → ∃𝑡 ∈ 𝑃 ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
132	122, 131	r19.29a 3170	. . . . 5 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
133	3, 4, 5, 25, 27, 39, 35, 32	axtgsegcon 28808	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ∃𝑧 ∈ 𝑃 ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
134	133	ad2antrr 739	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ∃𝑧 ∈ 𝑃 ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
135	132, 134	r19.29a 3170	. . . 4 ⊢ ((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
136	3, 4, 5, 24, 41, 34, 29, 31	axtgsegcon 28808	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ∃𝑦 ∈ 𝑃 (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
137	136	ad2antrr 739	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ∃𝑦 ∈ 𝑃 (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
138	135, 137	r19.29a 3170	. . 3 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
139	3, 4, 5, 24, 38, 29, 34, 31	axtgsegcon 28808	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ∃𝑥 ∈ 𝑃 (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴)))
140	138, 139	r19.29a 3170	. 2 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
141	23, 140	pm2.61dane 3042	1 ⊢ (𝜑 → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∃wrex 3086 ‘cfv 6533 (class class class)co 7414 Basecbs 17304 distcds 17354 TarskiGcstrkg 28771 Itvcitv 28777 LineGclng 28778 pInvGcmir 29006

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

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 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8458 df-oadd 8462 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-dju 9909 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-nn 12261 df-2 12330 df-n0 12532 df-xnn0 12605 df-z 12619 df-uz 12891 df-fz 13565 df-hash 14398 df-trkgc 28792 df-trkgb 28793 df-trkgcb 28794 df-trkg 28797 df-mir 29007

This theorem is used by: mirbtwni 29025 mircgrs 29027 mirmot 29029 miduniq 29039 mirleqb 29048 ragcom 29055 colperpexlem1 29088 lmiisolem 29183 hypcgrlem2 29188 hypcgr 29189 prlngsymquad 29324

W3C validator