Metamath Proof Explorer

Theorem miriso

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)

Ref Expression
Hypotheses 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 miriso ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) − ( 𝑀 ‘ 𝑌 ) ) = ( 𝑋 − 𝑌 ) )

Proof

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