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 ( 𝜑 → ( ( 𝑀𝑋 ) ( 𝑀𝑌 ) ) = ( 𝑋 𝑌 ) )