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 25565

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 477	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 = 𝐴)
2	1	oveq1d 6665	. . 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 481	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐺 ∈ TarskiG)
10		mirval.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
11	10	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ 𝑃)
12		mirfv.m	. . . 4 ⊢ 𝑀 = (𝑆‘𝐴)
13		miriso.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
14	13	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑌 ∈ 𝑃)
15	3, 4, 5, 6, 7, 9, 11, 12, 14	mircgr 25552	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − (𝑀‘𝑌)) = (𝐴 − 𝑌))
16		miriso.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
17	16	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ 𝑃)
18	1	eqcomd 2628	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = 𝑋)
19	18	oveq2d 6666	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − 𝐴) = (𝐴 − 𝑋))
20	3, 4, 5, 9, 11, 17	tgbtwntriv1 25386	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐼𝑋))
21	3, 4, 5, 6, 7, 9, 11, 12, 17, 11, 19, 20	ismir 25554	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = (𝑀‘𝑋))
22	21	oveq1d 6665	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − (𝑀‘𝑌)) = ((𝑀‘𝑋) − (𝑀‘𝑌)))
23	2, 15, 22	3eqtr2rd 2663	. 2 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
24	8	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝐺 ∈ TarskiG)
25	24	ad2antrr 762	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝐺 ∈ TarskiG)
26	25	ad6antr 772	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐺 ∈ TarskiG)
27		simplr 792	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝑥 ∈ 𝑃)
28	27	ad6antr 772	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑥 ∈ 𝑃)
29	16	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝑋 ∈ 𝑃)
30	29	ad8antr 776	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ 𝑃)
31	10	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝐴 ∈ 𝑃)
32	31	ad2antrr 762	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝐴 ∈ 𝑃)
33	32	ad6antr 772	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ 𝑃)
34	13	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝑌 ∈ 𝑃)
35	34	ad2antrr 762	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝑌 ∈ 𝑃)
36	35	ad6antr 772	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ 𝑃)
37		simp-4r 807	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑧 ∈ 𝑃)
38	3, 4, 5, 6, 7, 24, 31, 12, 29	mircl 25556	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → (𝑀‘𝑋) ∈ 𝑃)
39	38	ad2antrr 762	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → (𝑀‘𝑋) ∈ 𝑃)
40	39	ad6antr 772	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ 𝑃)
41	3, 4, 5, 6, 7, 24, 31, 12, 34	mircl 25556	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → (𝑀‘𝑌) ∈ 𝑃)
42	41	ad8antr 776	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ 𝑃)
43	3, 4, 5, 6, 7, 26, 33, 12, 30	mirbtwn 25553	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ ((𝑀‘𝑋)𝐼𝑋))
44		simp-7r 813	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴)))
45	44	simpld 475	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥))
46	3, 4, 5, 26, 40, 33, 30, 28, 43, 45	tgbtwnexch3 25389	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝐴𝐼𝑥))
47	3, 4, 5, 26, 33, 30, 28, 46	tgbtwncom 25383	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝑥𝐼𝐴))
48	3, 4, 5, 26, 40, 30, 28, 45	tgbtwncom 25383	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝑥𝐼(𝑀‘𝑋)))
49	3, 4, 5, 26, 40, 33, 30, 43	tgbtwncom 25383	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑋)))
50	3, 4, 5, 26, 28, 30, 33, 40, 48, 49	tgbtwnexch2 25391	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑥𝐼(𝑀‘𝑋)))
51		simpllr 799	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
52	51	simpld 475	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝑥𝐼𝑧))
53	3, 4, 5, 26, 28, 33, 40, 37, 50, 52	tgbtwnexch3 25389	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝐴𝐼𝑧))
54	3, 4, 5, 26, 33, 40, 37, 53	tgbtwncom 25383	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝑧𝐼𝐴))
55		simp-4r 807	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → 𝑦 ∈ 𝑃)
56	55	ad2antrr 762	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑦 ∈ 𝑃)
57	3, 4, 5, 6, 7, 26, 33, 12, 36	mirbtwn 25553	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ ((𝑀‘𝑌)𝐼𝑌))
58		simp-5r 809	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
59	58	simpld 475	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦))
60	3, 4, 5, 26, 42, 33, 36, 56, 57, 59	tgbtwnexch3 25389	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝐴𝐼𝑦))
61	3, 4, 5, 26, 33, 36, 56, 60	tgbtwncom 25383	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝑦𝐼𝐴))
62	3, 4, 5, 6, 7, 26, 33, 12, 30	mircgr 25552	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑋)) = (𝐴 − 𝑋))
63	58	simprd 479	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝑦) = (𝑋 − 𝐴))
64	3, 4, 5, 26, 36, 56, 30, 33, 63	tgcgrcomlr 25375	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝑌) = (𝐴 − 𝑋))
65	62, 64	eqtr4d 2659	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑋)) = (𝑦 − 𝑌))
66	51	simprd 479	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))
67	3, 4, 5, 26, 33, 40, 37, 56, 36, 33, 53, 61, 65, 66	tgcgrextend 25380	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑧) = (𝑦 − 𝐴))
68	44	simprd 479	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝑥) = (𝑌 − 𝐴))
69	68	eqcomd 2628	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝐴) = (𝑋 − 𝑥))
70	3, 4, 5, 26, 56, 36, 33, 33, 30, 28, 61, 46, 64, 69	tgcgrextend 25380	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝐴 − 𝑥))
71	67, 70	eqtr2d 2657	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑥) = (𝐴 − 𝑧))
72	3, 4, 5, 26, 33, 28, 33, 37, 71	tgcgrcomlr 25375	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝑧 − 𝐴))
73	62	eqcomd 2628	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑋) = (𝐴 − (𝑀‘𝑋)))
74	3, 4, 5, 26, 33, 30, 33, 40, 73	tgcgrcomlr 25375	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝐴) = ((𝑀‘𝑋) − 𝐴))
75		simplr 792	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑡 ∈ 𝑃)
76	3, 4, 5, 26, 42, 36, 56, 59	tgbtwncom 25383	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝑦𝐼(𝑀‘𝑌)))
77	3, 4, 5, 26, 42, 33, 36, 57	tgbtwncom 25383	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑌𝐼(𝑀‘𝑌)))
78	3, 4, 5, 26, 56, 36, 33, 42, 76, 77	tgbtwnexch2 25391	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑦𝐼(𝑀‘𝑌)))
79		simpr 477	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
80	79	simpld 475	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝑦𝐼𝑡))
81	3, 4, 5, 26, 56, 33, 42, 75, 78, 80	tgbtwnexch3 25389	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝐴𝐼𝑡))
82	3, 4, 5, 26, 33, 42, 75, 81	tgbtwncom 25383	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝑡𝐼𝐴))
83	3, 4, 5, 26, 30, 28, 36, 33, 68	tgcgrcomlr 25375	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑋) = (𝐴 − 𝑌))
84	3, 4, 5, 6, 7, 26, 33, 12, 36	mircgr 25552	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑌)) = (𝐴 − 𝑌))
85	83, 84	eqtr4d 2659	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑋) = (𝐴 − (𝑀‘𝑌)))
86	79	simprd 479	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))
87	86	eqcomd 2628	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝐴) = ((𝑀‘𝑌) − 𝑡))
88	3, 4, 5, 26, 28, 30, 33, 33, 42, 75, 47, 81, 85, 87	tgcgrextend 25380	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝐴 − 𝑡))
89	3, 4, 5, 26, 33, 75	axtgcgrrflx 25361	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑡) = (𝑡 − 𝐴))
90	88, 89	eqtrd 2656	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝑡 − 𝐴))
91	3, 4, 5, 26, 28, 33, 75, 33, 90	tgcgrcomlr 25375	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑥) = (𝐴 − 𝑡))
92	70, 91, 89	3eqtrd 2660	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝑡 − 𝐴))
93	3, 4, 5, 26, 33, 42, 33, 36, 84	tgcgrcomlr 25375	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) − 𝐴) = (𝑌 − 𝐴))
94	93	eqcomd 2628	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝐴) = ((𝑀‘𝑌) − 𝐴))
95	3, 4, 5, 26, 75, 37	axtgcgrrflx 25361	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑡 − 𝑧) = (𝑧 − 𝑡))
96		simp-9r 817	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ≠ 𝐴)
97	96	neneqd 2799	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ¬ 𝑋 = 𝐴)
98	26	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐺 ∈ TarskiG)
99	33	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 ∈ 𝑃)
100	30	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ 𝑃)
101	46	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝑥))
102		simpr 477	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
103	102	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → (𝐴𝐼𝑥) = (𝐴𝐼𝐴))
104	101, 103	eleqtrd 2703	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝐴))
105	3, 4, 5, 98, 99, 100, 104	axtgbtwnid 25365	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 = 𝑋)
106	105	eqcomd 2628	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 = 𝐴)
107	97, 106	mtand 691	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ¬ 𝑥 = 𝐴)
108	107	neqned 2801	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑥 ≠ 𝐴)
109	3, 4, 5, 26, 28, 33, 40, 37, 50, 52	tgbtwnexch 25393	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑥𝐼𝑧))
110	3, 4, 5, 26, 56, 33, 42, 75, 78, 80	tgbtwnexch 25393	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑦𝐼𝑡))
111	3, 4, 5, 26, 56, 33, 75, 110	tgbtwncom 25383	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑡𝐼𝑦))
112	3, 4, 5, 26, 56, 33	axtgcgrrflx 25361	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝐴 − 𝑦))
113	67, 112	eqtrd 2656	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑧) = (𝐴 − 𝑦))
114	3, 4, 5, 26, 28, 75	axtgcgrrflx 25361	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑡) = (𝑡 − 𝑥))
115	91	eqcomd 2628	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑡) = (𝐴 − 𝑥))
116	3, 4, 5, 26, 28, 33, 37, 75, 33, 56, 75, 28, 108, 109, 111, 90, 113, 114, 115	axtg5seg 25364	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑧 − 𝑡) = (𝑦 − 𝑥))
117	95, 116	eqtr2d 2657	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝑥) = (𝑡 − 𝑧))
118	3, 4, 5, 26, 56, 36, 33, 28, 75, 42, 33, 37, 61, 82, 92, 94, 117, 71	tgifscgr 25403	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝑥) = ((𝑀‘𝑌) − 𝑧))
119	3, 4, 5, 26, 36, 28, 42, 37, 118	tgcgrcomlr 25375	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑌) = (𝑧 − (𝑀‘𝑌)))
120	84	eqcomd 2628	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑌) = (𝐴 − (𝑀‘𝑌)))
121	3, 4, 5, 26, 28, 30, 33, 36, 37, 40, 33, 42, 47, 54, 72, 74, 119, 120	tgifscgr 25403	. . . . . . 7 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝑌) = ((𝑀‘𝑋) − (𝑀‘𝑌)))
122	121	eqcomd 2628	. . . . . 6 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
123		simp-6l 810	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → (𝜑 ∧ 𝑋 ≠ 𝐴))
124		simpllr 799	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
125	24	ad2antrr 762	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝐺 ∈ TarskiG)
126		simplr 792	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝑦 ∈ 𝑃)
127	41	ad2antrr 762	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ 𝑃)
128	29	ad2antrr 762	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝑋 ∈ 𝑃)
129	31	ad2antrr 762	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝐴 ∈ 𝑃)
130	3, 4, 5, 125, 126, 127, 128, 129	axtgsegcon 25363	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ∃𝑡 ∈ 𝑃 ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
131	123, 55, 124, 130	syl21anc 1325	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → ∃𝑡 ∈ 𝑃 ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
132	122, 131	r19.29a 3078	. . . . 5 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
133	3, 4, 5, 25, 27, 39, 35, 32	axtgsegcon 25363	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ∃𝑧 ∈ 𝑃 ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
134	133	ad2antrr 762	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ∃𝑧 ∈ 𝑃 ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
135	132, 134	r19.29a 3078	. . . 4 ⊢ ((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
136	3, 4, 5, 24, 41, 34, 29, 31	axtgsegcon 25363	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ∃𝑦 ∈ 𝑃 (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
137	136	ad2antrr 762	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ∃𝑦 ∈ 𝑃 (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
138	135, 137	r19.29a 3078	. . 3 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
139	3, 4, 5, 24, 38, 29, 34, 31	axtgsegcon 25363	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ∃𝑥 ∈ 𝑃 (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴)))
140	138, 139	r19.29a 3078	. 2 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
141	23, 140	pm2.61dane 2881	1 ⊢ (𝜑 → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∃wrex 2913 ‘cfv 5888 (class class class)co 6650 Basecbs 15857 distcds 15950 TarskiGcstrkg 25329 Itvcitv 25335 LineGclng 25336 pInvGcmir 25547

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-hash 13118 df-trkgc 25347 df-trkgb 25348 df-trkgcb 25349 df-trkg 25352 df-mir 25548

This theorem is referenced by: mirbtwni 25566 mircgrs 25568 mirmot 25570 miduniq 25580 ragcom 25593 colperpexlem1 25622 lmiisolem 25688 hypcgrlem2 25692 hypcgr 25693

W3C validator