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 28744

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 7373	. . 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 28731	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − (𝑀‘𝑌)) = (𝐴 − 𝑌))
16		miriso.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
17	16	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ 𝑃)
18	1	eqcomd 2742	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = 𝑋)
19	18	oveq2d 7374	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − 𝐴) = (𝐴 − 𝑋))
20	3, 4, 5, 9, 11, 17	tgbtwntriv1 28565	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐼𝑋))
21	3, 4, 5, 6, 7, 9, 11, 12, 17, 11, 19, 20	ismir 28733	. . . 4 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = (𝑀‘𝑋))
22	21	oveq1d 7373	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − (𝑀‘𝑌)) = ((𝑀‘𝑋) − (𝑀‘𝑌)))
23	2, 15, 22	3eqtr2rd 2778	. 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 28735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → (𝑀‘𝑋) ∈ 𝑃)
39	38	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → (𝑀‘𝑋) ∈ 𝑃)
40	39	ad6antr 736	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ 𝑃)
41	3, 4, 5, 6, 7, 24, 31, 12, 34	mircl 28735	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → (𝑀‘𝑌) ∈ 𝑃)
42	41	ad8antr 740	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ 𝑃)
43	3, 4, 5, 6, 7, 26, 33, 12, 30	mirbtwn 28732	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ ((𝑀‘𝑋)𝐼𝑋))
44		simp-7r 789	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴)))
45	44	simpld 494	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥))
46	3, 4, 5, 26, 40, 33, 30, 28, 43, 45	tgbtwnexch3 28568	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝐴𝐼𝑥))
47	3, 4, 5, 26, 33, 30, 28, 46	tgbtwncom 28562	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝑥𝐼𝐴))
48	3, 4, 5, 26, 40, 30, 28, 45	tgbtwncom 28562	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝑥𝐼(𝑀‘𝑋)))
49	3, 4, 5, 26, 40, 33, 30, 43	tgbtwncom 28562	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑋)))
50	3, 4, 5, 26, 28, 30, 33, 40, 48, 49	tgbtwnexch2 28570	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑥𝐼(𝑀‘𝑋)))
51		simpllr 775	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
52	51	simpld 494	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝑥𝐼𝑧))
53	3, 4, 5, 26, 28, 33, 40, 37, 50, 52	tgbtwnexch3 28568	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝐴𝐼𝑧))
54	3, 4, 5, 26, 33, 40, 37, 53	tgbtwncom 28562	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝑧𝐼𝐴))
55		simp-4r 783	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → 𝑦 ∈ 𝑃)
56	55	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑦 ∈ 𝑃)
57	3, 4, 5, 6, 7, 26, 33, 12, 36	mirbtwn 28732	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ ((𝑀‘𝑌)𝐼𝑌))
58		simp-5r 785	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
59	58	simpld 494	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦))
60	3, 4, 5, 26, 42, 33, 36, 56, 57, 59	tgbtwnexch3 28568	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝐴𝐼𝑦))
61	3, 4, 5, 26, 33, 36, 56, 60	tgbtwncom 28562	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝑦𝐼𝐴))
62	3, 4, 5, 6, 7, 26, 33, 12, 30	mircgr 28731	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑋)) = (𝐴 − 𝑋))
63	58	simprd 495	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝑦) = (𝑋 − 𝐴))
64	3, 4, 5, 26, 36, 56, 30, 33, 63	tgcgrcomlr 28554	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝑌) = (𝐴 − 𝑋))
65	62, 64	eqtr4d 2774	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑋)) = (𝑦 − 𝑌))
66	51	simprd 495	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))
67	3, 4, 5, 26, 33, 40, 37, 56, 36, 33, 53, 61, 65, 66	tgcgrextend 28559	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑧) = (𝑦 − 𝐴))
68	44	simprd 495	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝑥) = (𝑌 − 𝐴))
69	68	eqcomd 2742	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝐴) = (𝑋 − 𝑥))
70	3, 4, 5, 26, 56, 36, 33, 33, 30, 28, 61, 46, 64, 69	tgcgrextend 28559	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝐴 − 𝑥))
71	67, 70	eqtr2d 2772	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑥) = (𝐴 − 𝑧))
72	3, 4, 5, 26, 33, 28, 33, 37, 71	tgcgrcomlr 28554	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝑧 − 𝐴))
73	62	eqcomd 2742	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑋) = (𝐴 − (𝑀‘𝑋)))
74	3, 4, 5, 26, 33, 30, 33, 40, 73	tgcgrcomlr 28554	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝐴) = ((𝑀‘𝑋) − 𝐴))
75		simplr 768	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑡 ∈ 𝑃)
76	3, 4, 5, 26, 42, 36, 56, 59	tgbtwncom 28562	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝑦𝐼(𝑀‘𝑌)))
77	3, 4, 5, 26, 42, 33, 36, 57	tgbtwncom 28562	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑌𝐼(𝑀‘𝑌)))
78	3, 4, 5, 26, 56, 36, 33, 42, 76, 77	tgbtwnexch2 28570	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑦𝐼(𝑀‘𝑌)))
79		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
80	79	simpld 494	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝑦𝐼𝑡))
81	3, 4, 5, 26, 56, 33, 42, 75, 78, 80	tgbtwnexch3 28568	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝐴𝐼𝑡))
82	3, 4, 5, 26, 33, 42, 75, 81	tgbtwncom 28562	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝑡𝐼𝐴))
83	3, 4, 5, 26, 30, 28, 36, 33, 68	tgcgrcomlr 28554	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑋) = (𝐴 − 𝑌))
84	3, 4, 5, 6, 7, 26, 33, 12, 36	mircgr 28731	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑌)) = (𝐴 − 𝑌))
85	83, 84	eqtr4d 2774	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑋) = (𝐴 − (𝑀‘𝑌)))
86	79	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))
87	86	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝐴) = ((𝑀‘𝑌) − 𝑡))
88	3, 4, 5, 26, 28, 30, 33, 33, 42, 75, 47, 81, 85, 87	tgcgrextend 28559	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝐴 − 𝑡))
89	3, 4, 5, 26, 33, 75	axtgcgrrflx 28536	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑡) = (𝑡 − 𝐴))
90	88, 89	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝑡 − 𝐴))
91	3, 4, 5, 26, 28, 33, 75, 33, 90	tgcgrcomlr 28554	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑥) = (𝐴 − 𝑡))
92	70, 91, 89	3eqtrd 2775	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝑡 − 𝐴))
93	3, 4, 5, 26, 33, 42, 33, 36, 84	tgcgrcomlr 28554	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) − 𝐴) = (𝑌 − 𝐴))
94	93	eqcomd 2742	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝐴) = ((𝑀‘𝑌) − 𝐴))
95	3, 4, 5, 26, 75, 37	axtgcgrrflx 28536	. . . . . . . . . . 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 7374	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → (𝐴𝐼𝑥) = (𝐴𝐼𝐴))
104	101, 103	eleqtrd 2838	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝐴))
105	3, 4, 5, 98, 99, 100, 104	axtgbtwnid 28540	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 = 𝑋)
106	105	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 = 𝐴)
107	97, 106	mtand 815	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ¬ 𝑥 = 𝐴)
108	107	neqned 2939	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑥 ≠ 𝐴)
109	3, 4, 5, 26, 28, 33, 40, 37, 50, 52	tgbtwnexch 28572	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑥𝐼𝑧))
110	3, 4, 5, 26, 56, 33, 42, 75, 78, 80	tgbtwnexch 28572	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑦𝐼𝑡))
111	3, 4, 5, 26, 56, 33, 75, 110	tgbtwncom 28562	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑡𝐼𝑦))
112	3, 4, 5, 26, 56, 33	axtgcgrrflx 28536	. . . . . . . . . . . . 13 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝐴 − 𝑦))
113	67, 112	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑧) = (𝐴 − 𝑦))
114	3, 4, 5, 26, 28, 75	axtgcgrrflx 28536	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑡) = (𝑡 − 𝑥))
115	91	eqcomd 2742	. . . . . . . . . . . 12 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑡) = (𝐴 − 𝑥))
116	3, 4, 5, 26, 28, 33, 37, 75, 33, 56, 75, 28, 108, 109, 111, 90, 113, 114, 115	axtg5seg 28539	. . . . . . . . . . 11 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑧 − 𝑡) = (𝑦 − 𝑥))
117	95, 116	eqtr2d 2772	. . . . . . . . . 10 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝑥) = (𝑡 − 𝑧))
118	3, 4, 5, 26, 56, 36, 33, 28, 75, 42, 33, 37, 61, 82, 92, 94, 117, 71	tgifscgr 28582	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝑥) = ((𝑀‘𝑌) − 𝑧))
119	3, 4, 5, 26, 36, 28, 42, 37, 118	tgcgrcomlr 28554	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑌) = (𝑧 − (𝑀‘𝑌)))
120	84	eqcomd 2742	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑌) = (𝐴 − (𝑀‘𝑌)))
121	3, 4, 5, 26, 28, 30, 33, 36, 37, 40, 33, 42, 47, 54, 72, 74, 119, 120	tgifscgr 28582	. . . . . . 7 ⊢ ((((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝑌) = ((𝑀‘𝑋) − (𝑀‘𝑌)))
122	121	eqcomd 2742	. . . . . 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 28538	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ∃𝑡 ∈ 𝑃 ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
131	123, 55, 124, 130	syl21anc 837	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → ∃𝑡 ∈ 𝑃 ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)))
132	122, 131	r19.29a 3144	. . . . 5 ⊢ ((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
133	3, 4, 5, 25, 27, 39, 35, 32	axtgsegcon 28538	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ∃𝑧 ∈ 𝑃 ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
134	133	ad2antrr 726	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ∃𝑧 ∈ 𝑃 ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)))
135	132, 134	r19.29a 3144	. . . 4 ⊢ ((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
136	3, 4, 5, 24, 41, 34, 29, 31	axtgsegcon 28538	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ∃𝑦 ∈ 𝑃 (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
137	136	ad2antrr 726	. . . 4 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ∃𝑦 ∈ 𝑃 (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴)))
138	135, 137	r19.29a 3144	. . 3 ⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
139	3, 4, 5, 24, 38, 29, 34, 31	axtgsegcon 28538	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ∃𝑥 ∈ 𝑃 (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴)))
140	138, 139	r19.29a 3144	. 2 ⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))
141	23, 140	pm2.61dane 3019	1 ⊢ (𝜑 → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 ∃wrex 3060 ‘cfv 6492 (class class class)co 7358 Basecbs 17138 distcds 17188 TarskiGcstrkg 28501 Itvcitv 28507 LineGclng 28508 pInvGcmir 28726

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-oadd 8401 df-er 8635 df-en 8886 df-dom 8887 df-sdom 8888 df-fin 8889 df-dju 9815 df-card 9853 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-nn 12148 df-2 12210 df-n0 12404 df-xnn0 12477 df-z 12491 df-uz 12754 df-fz 13426 df-hash 14256 df-trkgc 28522 df-trkgb 28523 df-trkgcb 28524 df-trkg 28527 df-mir 28727

This theorem is referenced by: mirbtwni 28745 mircgrs 28747 mirmot 28749 miduniq 28759 ragcom 28772 colperpexlem1 28804 lmiisolem 28870 hypcgrlem2 28874 hypcgr 28875

W3C validator