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 28595

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 484	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 = 𝐴)
2	1	oveq1d 7418	. . 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 480	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐺 ∈ TarskiG)
10		mirval.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
11	10	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ 𝑃)
12		mirfv.m	. . . 4 ⊢ 𝑀 = (𝑆‘𝐴)
13		miriso.2	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
14	13	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑌 ∈ 𝑃)
15	3, 4, 5, 6, 7, 9, 11, 12, 14	mircgr 28582	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − (𝑀‘𝑌)) = (𝐴 − 𝑌))
16		miriso.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
17	16	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ 𝑃)
18	1	eqcomd 2741	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = 𝑋)
19	18	oveq2d 7419	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − 𝐴) = (𝐴 − 𝑋))
20	3, 4, 5, 9, 11, 17	tgbtwntriv1 28416	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐼𝑋))
21	3, 4, 5, 6, 7, 9, 11, 12, 17, 11, 19, 20	ismir 28584	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = (𝑀‘𝑋))
22	21	oveq1d 7418	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − (𝑀‘𝑌)) = ((𝑀‘𝑋) − (𝑀‘𝑌)))
23	2, 15, 22	3eqtr2rd 2777	. 2 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
24	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝐺 ∈ TarskiG)
25	24	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝐺 ∈ TarskiG)
26	25	ad6antr 736	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐺 ∈ TarskiG)
27		simplr 768	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝑥 ∈ 𝑃)
28	27	ad6antr 736	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑥 ∈ 𝑃)
29	16	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝑋 ∈ 𝑃)
30	29	ad8antr 740	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ 𝑃)
31	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝐴 ∈ 𝑃)
32	31	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝐴 ∈ 𝑃)
33	32	ad6antr 736	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ 𝑃)
34	13	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝑌 ∈ 𝑃)
35	34	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝑌 ∈ 𝑃)
36	35	ad6antr 736	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ 𝑃)
37		simp-4r 783	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑧 ∈ 𝑃)
38	3, 4, 5, 6, 7, 24, 31, 12, 29	mircl 28586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → (𝑀‘𝑋) ∈ 𝑃)
39	38	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → (𝑀‘𝑋) ∈ 𝑃)
40	39	ad6antr 736	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ 𝑃)
41	3, 4, 5, 6, 7, 24, 31, 12, 34	mircl 28586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → (𝑀‘𝑌) ∈ 𝑃)
42	41	ad8antr 740	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ 𝑃)
43	3, 4, 5, 6, 7, 26, 33, 12, 30	mirbtwn 28583	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ ((𝑀‘𝑋)𝐼𝑋))
44		simp-7r 789	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴)))
45	44	simpld 494	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥))
46	3, 4, 5, 26, 40, 33, 30, 28, 43, 45	tgbtwnexch3 28419	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝐴𝐼𝑥))
47	3, 4, 5, 26, 33, 30, 28, 46	tgbtwncom 28413	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝑥𝐼𝐴))
48	3, 4, 5, 26, 40, 30, 28, 45	tgbtwncom 28413	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝑥𝐼(𝑀‘𝑋)))
49	3, 4, 5, 26, 40, 33, 30, 43	tgbtwncom 28413	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑋)))
50	3, 4, 5, 26, 28, 30, 33, 40, 48, 49	tgbtwnexch2 28421	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑥𝐼(𝑀‘𝑋)))
51		simpllr 775	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
52	51	simpld 494	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝑥𝐼𝑧))
53	3, 4, 5, 26, 28, 33, 40, 37, 50, 52	tgbtwnexch3 28419	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝐴𝐼𝑧))
54	3, 4, 5, 26, 33, 40, 37, 53	tgbtwncom 28413	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝑧𝐼𝐴))
55		simp-4r 783	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → 𝑦 ∈ 𝑃)
56	55	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑦 ∈ 𝑃)
57	3, 4, 5, 6, 7, 26, 33, 12, 36	mirbtwn 28583	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ ((𝑀‘𝑌)𝐼𝑌))
58		simp-5r 785	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
59	58	simpld 494	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦))
60	3, 4, 5, 26, 42, 33, 36, 56, 57, 59	tgbtwnexch3 28419	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝐴𝐼𝑦))
61	3, 4, 5, 26, 33, 36, 56, 60	tgbtwncom 28413	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝑦𝐼𝐴))
62	3, 4, 5, 6, 7, 26, 33, 12, 30	mircgr 28582	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑋)) = (𝐴 − 𝑋))
63	58	simprd 495	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝑦) = (𝑋 − 𝐴))
64	3, 4, 5, 26, 36, 56, 30, 33, 63	tgcgrcomlr 28405	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝑌) = (𝐴 − 𝑋))
65	62, 64	eqtr4d 2773	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑋)) = (𝑦 − 𝑌))
66	51	simprd 495	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))
67	3, 4, 5, 26, 33, 40, 37, 56, 36, 33, 53, 61, 65, 66	tgcgrextend 28410	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑧) = (𝑦 − 𝐴))
68	44	simprd 495	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝑥) = (𝑌 − 𝐴))
69	68	eqcomd 2741	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝐴) = (𝑋 − 𝑥))
70	3, 4, 5, 26, 56, 36, 33, 33, 30, 28, 61, 46, 64, 69	tgcgrextend 28410	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝐴 − 𝑥))
71	67, 70	eqtr2d 2771	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑥) = (𝐴 − 𝑧))
72	3, 4, 5, 26, 33, 28, 33, 37, 71	tgcgrcomlr 28405	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝑧 − 𝐴))
73	62	eqcomd 2741	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑋) = (𝐴 − (𝑀‘𝑋)))
74	3, 4, 5, 26, 33, 30, 33, 40, 73	tgcgrcomlr 28405	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝐴) = ((𝑀‘𝑋) − 𝐴))
75		simplr 768	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑡 ∈ 𝑃)
76	3, 4, 5, 26, 42, 36, 56, 59	tgbtwncom 28413	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝑦𝐼(𝑀‘𝑌)))
77	3, 4, 5, 26, 42, 33, 36, 57	tgbtwncom 28413	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑌𝐼(𝑀‘𝑌)))
78	3, 4, 5, 26, 56, 36, 33, 42, 76, 77	tgbtwnexch2 28421	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑦𝐼(𝑀‘𝑌)))
79		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
80	79	simpld 494	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝑦𝐼𝑡))
81	3, 4, 5, 26, 56, 33, 42, 75, 78, 80	tgbtwnexch3 28419	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝐴𝐼𝑡))
82	3, 4, 5, 26, 33, 42, 75, 81	tgbtwncom 28413	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝑡𝐼𝐴))
83	3, 4, 5, 26, 30, 28, 36, 33, 68	tgcgrcomlr 28405	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑋) = (𝐴 − 𝑌))
84	3, 4, 5, 6, 7, 26, 33, 12, 36	mircgr 28582	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑌)) = (𝐴 − 𝑌))
85	83, 84	eqtr4d 2773	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑋) = (𝐴 − (𝑀‘𝑌)))
86	79	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))
87	86	eqcomd 2741	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝐴) = ((𝑀‘𝑌) − 𝑡))
88	3, 4, 5, 26, 28, 30, 33, 33, 42, 75, 47, 81, 85, 87	tgcgrextend 28410	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝐴 − 𝑡))
89	3, 4, 5, 26, 33, 75	axtgcgrrflx 28387	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑡) = (𝑡 − 𝐴))
90	88, 89	eqtrd 2770	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝑡 − 𝐴))
91	3, 4, 5, 26, 28, 33, 75, 33, 90	tgcgrcomlr 28405	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑥) = (𝐴 − 𝑡))
92	70, 91, 89	3eqtrd 2774	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝑡 − 𝐴))
93	3, 4, 5, 26, 33, 42, 33, 36, 84	tgcgrcomlr 28405	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) − 𝐴) = (𝑌 − 𝐴))
94	93	eqcomd 2741	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝐴) = ((𝑀‘𝑌) − 𝐴))
95	3, 4, 5, 26, 75, 37	axtgcgrrflx 28387	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑡 − 𝑧) = (𝑧 − 𝑡))
96		simp-9r 793	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ≠ 𝐴)
97	96	neneqd 2937	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ¬ 𝑋 = 𝐴)
98	26	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐺 ∈ TarskiG)
99	33	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 ∈ 𝑃)
100	30	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ 𝑃)
101	46	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝑥))
102		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
103	102	oveq2d 7419	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → (𝐴𝐼𝑥) = (𝐴𝐼𝐴))
104	101, 103	eleqtrd 2836	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝐴))
105	3, 4, 5, 98, 99, 100, 104	axtgbtwnid 28391	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 = 𝑋)
106	105	eqcomd 2741	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 = 𝐴)
107	97, 106	mtand 815	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ¬ 𝑥 = 𝐴)
108	107	neqned 2939	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑥 ≠ 𝐴)
109	3, 4, 5, 26, 28, 33, 40, 37, 50, 52	tgbtwnexch 28423	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑥𝐼𝑧))
110	3, 4, 5, 26, 56, 33, 42, 75, 78, 80	tgbtwnexch 28423	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑦𝐼𝑡))
111	3, 4, 5, 26, 56, 33, 75, 110	tgbtwncom 28413	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑡𝐼𝑦))
112	3, 4, 5, 26, 56, 33	axtgcgrrflx 28387	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝐴 − 𝑦))
113	67, 112	eqtrd 2770	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑧) = (𝐴 − 𝑦))
114	3, 4, 5, 26, 28, 75	axtgcgrrflx 28387	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑡) = (𝑡 − 𝑥))
115	91	eqcomd 2741	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑡) = (𝐴 − 𝑥))
116	3, 4, 5, 26, 28, 33, 37, 75, 33, 56, 75, 28, 108, 109, 111, 90, 113, 114, 115	axtg5seg 28390	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑧 − 𝑡) = (𝑦 − 𝑥))
117	95, 116	eqtr2d 2771	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝑥) = (𝑡 − 𝑧))
118	3, 4, 5, 26, 56, 36, 33, 28, 75, 42, 33, 37, 61, 82, 92, 94, 117, 71	tgifscgr 28433	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝑥) = ((𝑀‘𝑌) − 𝑧))
119	3, 4, 5, 26, 36, 28, 42, 37, 118	tgcgrcomlr 28405	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑌) = (𝑧 − (𝑀‘𝑌)))
120	84	eqcomd 2741	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑌) = (𝐴 − (𝑀‘𝑌)))
121	3, 4, 5, 26, 28, 30, 33, 36, 37, 40, 33, 42, 47, 54, 72, 74, 119, 120	tgifscgr 28433	. . . . . . 7 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝑌) = ((𝑀‘𝑋) − (𝑀‘𝑌)))
122	121	eqcomd 2741	. . . . . 6 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
123		simp-6l 786	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → (𝜑 ∧ 𝑋 ≠ 𝐴))
124		simpllr 775	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
125	24	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝐺 ∈ TarskiG)
126		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝑦 ∈ 𝑃)
127	41	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ 𝑃)
128	29	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝑋 ∈ 𝑃)
129	31	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝐴 ∈ 𝑃)
130	3, 4, 5, 125, 126, 127, 128, 129	axtgsegcon 28389	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ∃𝑡 ∈ 𝑃 ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
131	123, 55, 124, 130	syl21anc 837	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → ∃𝑡 ∈ 𝑃 ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
132	122, 131	r19.29a 3148	. . . . 5 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
133	3, 4, 5, 25, 27, 39, 35, 32	axtgsegcon 28389	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ∃𝑧 ∈ 𝑃 ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
134	133	ad2antrr 726	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ∃𝑧 ∈ 𝑃 ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
135	132, 134	r19.29a 3148	. . . 4 ⊢ ((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
136	3, 4, 5, 24, 41, 34, 29, 31	axtgsegcon 28389	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ∃𝑦 ∈ 𝑃 (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
137	136	ad2antrr 726	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ∃𝑦 ∈ 𝑃 (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
138	135, 137	r19.29a 3148	. . 3 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
139	3, 4, 5, 24, 38, 29, 34, 31	axtgsegcon 28389	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ∃𝑥 ∈ 𝑃 (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴)))
140	138, 139	r19.29a 3148	. 2 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
141	23, 140	pm2.61dane 3019	1 ⊢ (𝜑 → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ≠ wne 2932 ∃wrex 3060 ‘cfv 6530 (class class class)co 7403 Basecbs 17226 distcds 17278 TarskiGcstrkg 28352 Itvcitv 28358 LineGclng 28359 pInvGcmir 28577

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7727 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 theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6483 df-fun 6532 df-fn 6533 df-f 6534 df-f1 6535 df-fo 6536 df-f1o 6537 df-fv 6538 df-riota 7360 df-ov 7406 df-oprab 7407 df-mpo 7408 df-om 7860 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8383 df-rdg 8422 df-1o 8478 df-oadd 8482 df-er 8717 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-dju 9913 df-card 9951 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11466 df-neg 11467 df-nn 12239 df-2 12301 df-n0 12500 df-xnn0 12573 df-z 12587 df-uz 12851 df-fz 13523 df-hash 14347 df-trkgc 28373 df-trkgb 28374 df-trkgcb 28375 df-trkg 28378 df-mir 28578

This theorem is referenced by: mirbtwni 28596 mircgrs 28598 mirmot 28600 miduniq 28610 ragcom 28623 colperpexlem1 28655 lmiisolem 28721 hypcgrlem2 28725 hypcgr 28726

W3C validator