MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  miriso Structured version   Visualization version   GIF version

Theorem miriso 26383
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.
StepHypRef Expression
1 simpr 485 . . . 4 ((𝜑𝑋 = 𝐴) → 𝑋 = 𝐴)
21oveq1d 7160 . . 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)
98adantr 481 . . . 4 ((𝜑𝑋 = 𝐴) → 𝐺 ∈ TarskiG)
10 mirval.a . . . . 5 (𝜑𝐴𝑃)
1110adantr 481 . . . 4 ((𝜑𝑋 = 𝐴) → 𝐴𝑃)
12 mirfv.m . . . 4 𝑀 = (𝑆𝐴)
13 miriso.2 . . . . 5 (𝜑𝑌𝑃)
1413adantr 481 . . . 4 ((𝜑𝑋 = 𝐴) → 𝑌𝑃)
153, 4, 5, 6, 7, 9, 11, 12, 14mircgr 26370 . . 3 ((𝜑𝑋 = 𝐴) → (𝐴 (𝑀𝑌)) = (𝐴 𝑌))
16 miriso.1 . . . . . 6 (𝜑𝑋𝑃)
1716adantr 481 . . . . 5 ((𝜑𝑋 = 𝐴) → 𝑋𝑃)
181eqcomd 2824 . . . . . 6 ((𝜑𝑋 = 𝐴) → 𝐴 = 𝑋)
1918oveq2d 7161 . . . . 5 ((𝜑𝑋 = 𝐴) → (𝐴 𝐴) = (𝐴 𝑋))
203, 4, 5, 9, 11, 17tgbtwntriv1 26204 . . . . 5 ((𝜑𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐼𝑋))
213, 4, 5, 6, 7, 9, 11, 12, 17, 11, 19, 20ismir 26372 . . . 4 ((𝜑𝑋 = 𝐴) → 𝐴 = (𝑀𝑋))
2221oveq1d 7160 . . 3 ((𝜑𝑋 = 𝐴) → (𝐴 (𝑀𝑌)) = ((𝑀𝑋) (𝑀𝑌)))
232, 15, 223eqtr2rd 2860 . 2 ((𝜑𝑋 = 𝐴) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
248adantr 481 . . . . . . . . . 10 ((𝜑𝑋𝐴) → 𝐺 ∈ TarskiG)
2524ad2antrr 722 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝐺 ∈ TarskiG)
2625ad6antr 732 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐺 ∈ TarskiG)
27 simplr 765 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝑥𝑃)
2827ad6antr 732 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑥𝑃)
2916adantr 481 . . . . . . . . 9 ((𝜑𝑋𝐴) → 𝑋𝑃)
3029ad8antr 736 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋𝑃)
3110adantr 481 . . . . . . . . . 10 ((𝜑𝑋𝐴) → 𝐴𝑃)
3231ad2antrr 722 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝐴𝑃)
3332ad6antr 732 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴𝑃)
3413adantr 481 . . . . . . . . . 10 ((𝜑𝑋𝐴) → 𝑌𝑃)
3534ad2antrr 722 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝑌𝑃)
3635ad6antr 732 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌𝑃)
37 simp-4r 780 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑧𝑃)
383, 4, 5, 6, 7, 24, 31, 12, 29mircl 26374 . . . . . . . . . 10 ((𝜑𝑋𝐴) → (𝑀𝑋) ∈ 𝑃)
3938ad2antrr 722 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → (𝑀𝑋) ∈ 𝑃)
4039ad6antr 732 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ 𝑃)
413, 4, 5, 6, 7, 24, 31, 12, 34mircl 26374 . . . . . . . . 9 ((𝜑𝑋𝐴) → (𝑀𝑌) ∈ 𝑃)
4241ad8antr 736 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ 𝑃)
433, 4, 5, 6, 7, 26, 33, 12, 30mirbtwn 26371 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ ((𝑀𝑋)𝐼𝑋))
44 simp-7r 786 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴)))
4544simpld 495 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ ((𝑀𝑋)𝐼𝑥))
463, 4, 5, 26, 40, 33, 30, 28, 43, 45tgbtwnexch3 26207 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ (𝐴𝐼𝑥))
473, 4, 5, 26, 33, 30, 28, 46tgbtwncom 26201 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ (𝑥𝐼𝐴))
483, 4, 5, 26, 40, 30, 28, 45tgbtwncom 26201 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ (𝑥𝐼(𝑀𝑋)))
493, 4, 5, 26, 40, 33, 30, 43tgbtwncom 26201 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑋𝐼(𝑀𝑋)))
503, 4, 5, 26, 28, 30, 33, 40, 48, 49tgbtwnexch2 26209 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑥𝐼(𝑀𝑋)))
51 simpllr 772 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴)))
5251simpld 495 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ (𝑥𝐼𝑧))
533, 4, 5, 26, 28, 33, 40, 37, 50, 52tgbtwnexch3 26207 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ (𝐴𝐼𝑧))
543, 4, 5, 26, 33, 40, 37, 53tgbtwncom 26201 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ (𝑧𝐼𝐴))
55 simp-4r 780 . . . . . . . . . . . 12 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → 𝑦𝑃)
5655ad2antrr 722 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑦𝑃)
573, 4, 5, 6, 7, 26, 33, 12, 36mirbtwn 26371 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ ((𝑀𝑌)𝐼𝑌))
58 simp-5r 782 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
5958simpld 495 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ ((𝑀𝑌)𝐼𝑦))
603, 4, 5, 26, 42, 33, 36, 56, 57, 59tgbtwnexch3 26207 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ (𝐴𝐼𝑦))
613, 4, 5, 26, 33, 36, 56, 60tgbtwncom 26201 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ (𝑦𝐼𝐴))
623, 4, 5, 6, 7, 26, 33, 12, 30mircgr 26370 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 (𝑀𝑋)) = (𝐴 𝑋))
6358simprd 496 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝑦) = (𝑋 𝐴))
643, 4, 5, 26, 36, 56, 30, 33, 63tgcgrcomlr 26193 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝑌) = (𝐴 𝑋))
6562, 64eqtr4d 2856 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 (𝑀𝑋)) = (𝑦 𝑌))
6651simprd 496 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑋) 𝑧) = (𝑌 𝐴))
673, 4, 5, 26, 33, 40, 37, 56, 36, 33, 53, 61, 65, 66tgcgrextend 26198 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑧) = (𝑦 𝐴))
6844simprd 496 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝑥) = (𝑌 𝐴))
6968eqcomd 2824 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝐴) = (𝑋 𝑥))
703, 4, 5, 26, 56, 36, 33, 33, 30, 28, 61, 46, 64, 69tgcgrextend 26198 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝐴) = (𝐴 𝑥))
7167, 70eqtr2d 2854 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑥) = (𝐴 𝑧))
723, 4, 5, 26, 33, 28, 33, 37, 71tgcgrcomlr 26193 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝐴) = (𝑧 𝐴))
7362eqcomd 2824 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑋) = (𝐴 (𝑀𝑋)))
743, 4, 5, 26, 33, 30, 33, 40, 73tgcgrcomlr 26193 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝐴) = ((𝑀𝑋) 𝐴))
75 simplr 765 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑡𝑃)
763, 4, 5, 26, 42, 36, 56, 59tgbtwncom 26201 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ (𝑦𝐼(𝑀𝑌)))
773, 4, 5, 26, 42, 33, 36, 57tgbtwncom 26201 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑌𝐼(𝑀𝑌)))
783, 4, 5, 26, 56, 36, 33, 42, 76, 77tgbtwnexch2 26209 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑦𝐼(𝑀𝑌)))
79 simpr 485 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴)))
8079simpld 495 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ (𝑦𝐼𝑡))
813, 4, 5, 26, 56, 33, 42, 75, 78, 80tgbtwnexch3 26207 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ (𝐴𝐼𝑡))
823, 4, 5, 26, 33, 42, 75, 81tgbtwncom 26201 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ (𝑡𝐼𝐴))
833, 4, 5, 26, 30, 28, 36, 33, 68tgcgrcomlr 26193 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑋) = (𝐴 𝑌))
843, 4, 5, 6, 7, 26, 33, 12, 36mircgr 26370 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 (𝑀𝑌)) = (𝐴 𝑌))
8583, 84eqtr4d 2856 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑋) = (𝐴 (𝑀𝑌)))
8679simprd 496 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑌) 𝑡) = (𝑋 𝐴))
8786eqcomd 2824 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝐴) = ((𝑀𝑌) 𝑡))
883, 4, 5, 26, 28, 30, 33, 33, 42, 75, 47, 81, 85, 87tgcgrextend 26198 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝐴) = (𝐴 𝑡))
893, 4, 5, 26, 33, 75axtgcgrrflx 26175 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑡) = (𝑡 𝐴))
9088, 89eqtrd 2853 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝐴) = (𝑡 𝐴))
913, 4, 5, 26, 28, 33, 75, 33, 90tgcgrcomlr 26193 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑥) = (𝐴 𝑡))
9270, 91, 893eqtrd 2857 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝐴) = (𝑡 𝐴))
933, 4, 5, 26, 33, 42, 33, 36, 84tgcgrcomlr 26193 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑌) 𝐴) = (𝑌 𝐴))
9493eqcomd 2824 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝐴) = ((𝑀𝑌) 𝐴))
953, 4, 5, 26, 75, 37axtgcgrrflx 26175 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑡 𝑧) = (𝑧 𝑡))
96 simp-9r 790 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋𝐴)
9796neneqd 3018 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ¬ 𝑋 = 𝐴)
9826adantr 481 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝐺 ∈ TarskiG)
9933adantr 481 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴𝑃)
10030adantr 481 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋𝑃)
10146adantr 481 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝑥))
102 simpr 485 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
103102oveq2d 7161 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → (𝐴𝐼𝑥) = (𝐴𝐼𝐴))
104101, 103eleqtrd 2912 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝐴))
1053, 4, 5, 98, 99, 100, 104axtgbtwnid 26179 . . . . . . . . . . . . . . 15 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 = 𝑋)
106105eqcomd 2824 . . . . . . . . . . . . . 14 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 = 𝐴)
10797, 106mtand 812 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ¬ 𝑥 = 𝐴)
108107neqned 3020 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑥𝐴)
1093, 4, 5, 26, 28, 33, 40, 37, 50, 52tgbtwnexch 26211 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑥𝐼𝑧))
1103, 4, 5, 26, 56, 33, 42, 75, 78, 80tgbtwnexch 26211 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑦𝐼𝑡))
1113, 4, 5, 26, 56, 33, 75, 110tgbtwncom 26201 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑡𝐼𝑦))
1123, 4, 5, 26, 56, 33axtgcgrrflx 26175 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝐴) = (𝐴 𝑦))
11367, 112eqtrd 2853 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑧) = (𝐴 𝑦))
1143, 4, 5, 26, 28, 75axtgcgrrflx 26175 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑡) = (𝑡 𝑥))
11591eqcomd 2824 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑡) = (𝐴 𝑥))
1163, 4, 5, 26, 28, 33, 37, 75, 33, 56, 75, 28, 108, 109, 111, 90, 113, 114, 115axtg5seg 26178 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑧 𝑡) = (𝑦 𝑥))
11795, 116eqtr2d 2854 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝑥) = (𝑡 𝑧))
1183, 4, 5, 26, 56, 36, 33, 28, 75, 42, 33, 37, 61, 82, 92, 94, 117, 71tgifscgr 26221 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝑥) = ((𝑀𝑌) 𝑧))
1193, 4, 5, 26, 36, 28, 42, 37, 118tgcgrcomlr 26193 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑌) = (𝑧 (𝑀𝑌)))
12084eqcomd 2824 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑌) = (𝐴 (𝑀𝑌)))
1213, 4, 5, 26, 28, 30, 33, 36, 37, 40, 33, 42, 47, 54, 72, 74, 119, 120tgifscgr 26221 . . . . . . 7 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝑌) = ((𝑀𝑋) (𝑀𝑌)))
122121eqcomd 2824 . . . . . 6 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
123 simp-6l 783 . . . . . . 7 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → (𝜑𝑋𝐴))
124 simpllr 772 . . . . . . 7 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
12524ad2antrr 722 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝐺 ∈ TarskiG)
126 simplr 765 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝑦𝑃)
12741ad2antrr 722 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → (𝑀𝑌) ∈ 𝑃)
12829ad2antrr 722 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝑋𝑃)
12931ad2antrr 722 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝐴𝑃)
1303, 4, 5, 125, 126, 127, 128, 129axtgsegcon 26177 . . . . . . 7 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → ∃𝑡𝑃 ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴)))
131123, 55, 124, 130syl21anc 833 . . . . . 6 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → ∃𝑡𝑃 ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴)))
132122, 131r19.29a 3286 . . . . 5 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
1333, 4, 5, 25, 27, 39, 35, 32axtgsegcon 26177 . . . . . 6 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → ∃𝑧𝑃 ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴)))
134133ad2antrr 722 . . . . 5 ((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → ∃𝑧𝑃 ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴)))
135132, 134r19.29a 3286 . . . 4 ((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
1363, 4, 5, 24, 41, 34, 29, 31axtgsegcon 26177 . . . . 5 ((𝜑𝑋𝐴) → ∃𝑦𝑃 (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
137136ad2antrr 722 . . . 4 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → ∃𝑦𝑃 (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
138135, 137r19.29a 3286 . . 3 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
1393, 4, 5, 24, 38, 29, 34, 31axtgsegcon 26177 . . 3 ((𝜑𝑋𝐴) → ∃𝑥𝑃 (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴)))
140138, 139r19.29a 3286 . 2 ((𝜑𝑋𝐴) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
14123, 140pm2.61dane 3101 1 (𝜑 → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  wne 3013  wrex 3136  cfv 6348  (class class class)co 7145  Basecbs 16471  distcds 16562  TarskiGcstrkg 26143  Itvcitv 26149  LineGclng 26150  pInvGcmir 26365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-dju 9318  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-2 11688  df-n0 11886  df-xnn0 11956  df-z 11970  df-uz 12232  df-fz 12881  df-hash 13679  df-trkgc 26161  df-trkgb 26162  df-trkgcb 26163  df-trkg 26166  df-mir 26366
This theorem is referenced by:  mirbtwni  26384  mircgrs  26386  mirmot  26388  miduniq  26398  ragcom  26411  colperpexlem1  26443  lmiisolem  26509  hypcgrlem2  26513  hypcgr  26514
  Copyright terms: Public domain W3C validator