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

Theorem miriso 26025
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 479 . . . 4 ((𝜑𝑋 = 𝐴) → 𝑋 = 𝐴)
21oveq1d 6939 . . 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 474 . . . 4 ((𝜑𝑋 = 𝐴) → 𝐺 ∈ TarskiG)
10 mirval.a . . . . 5 (𝜑𝐴𝑃)
1110adantr 474 . . . 4 ((𝜑𝑋 = 𝐴) → 𝐴𝑃)
12 mirfv.m . . . 4 𝑀 = (𝑆𝐴)
13 miriso.2 . . . . 5 (𝜑𝑌𝑃)
1413adantr 474 . . . 4 ((𝜑𝑋 = 𝐴) → 𝑌𝑃)
153, 4, 5, 6, 7, 9, 11, 12, 14mircgr 26012 . . 3 ((𝜑𝑋 = 𝐴) → (𝐴 (𝑀𝑌)) = (𝐴 𝑌))
16 miriso.1 . . . . . 6 (𝜑𝑋𝑃)
1716adantr 474 . . . . 5 ((𝜑𝑋 = 𝐴) → 𝑋𝑃)
181eqcomd 2784 . . . . . 6 ((𝜑𝑋 = 𝐴) → 𝐴 = 𝑋)
1918oveq2d 6940 . . . . 5 ((𝜑𝑋 = 𝐴) → (𝐴 𝐴) = (𝐴 𝑋))
203, 4, 5, 9, 11, 17tgbtwntriv1 25846 . . . . 5 ((𝜑𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐼𝑋))
213, 4, 5, 6, 7, 9, 11, 12, 17, 11, 19, 20ismir 26014 . . . 4 ((𝜑𝑋 = 𝐴) → 𝐴 = (𝑀𝑋))
2221oveq1d 6939 . . 3 ((𝜑𝑋 = 𝐴) → (𝐴 (𝑀𝑌)) = ((𝑀𝑋) (𝑀𝑌)))
232, 15, 223eqtr2rd 2821 . 2 ((𝜑𝑋 = 𝐴) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
248adantr 474 . . . . . . . . . 10 ((𝜑𝑋𝐴) → 𝐺 ∈ TarskiG)
2524ad2antrr 716 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝐺 ∈ TarskiG)
2625ad6antr 726 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐺 ∈ TarskiG)
27 simplr 759 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝑥𝑃)
2827ad6antr 726 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑥𝑃)
2916adantr 474 . . . . . . . . 9 ((𝜑𝑋𝐴) → 𝑋𝑃)
3029ad8antr 730 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋𝑃)
3110adantr 474 . . . . . . . . . 10 ((𝜑𝑋𝐴) → 𝐴𝑃)
3231ad2antrr 716 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝐴𝑃)
3332ad6antr 726 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴𝑃)
3413adantr 474 . . . . . . . . . 10 ((𝜑𝑋𝐴) → 𝑌𝑃)
3534ad2antrr 716 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝑌𝑃)
3635ad6antr 726 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌𝑃)
37 simp-4r 774 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑧𝑃)
383, 4, 5, 6, 7, 24, 31, 12, 29mircl 26016 . . . . . . . . . 10 ((𝜑𝑋𝐴) → (𝑀𝑋) ∈ 𝑃)
3938ad2antrr 716 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → (𝑀𝑋) ∈ 𝑃)
4039ad6antr 726 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ 𝑃)
413, 4, 5, 6, 7, 24, 31, 12, 34mircl 26016 . . . . . . . . 9 ((𝜑𝑋𝐴) → (𝑀𝑌) ∈ 𝑃)
4241ad8antr 730 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ 𝑃)
433, 4, 5, 6, 7, 26, 33, 12, 30mirbtwn 26013 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ ((𝑀𝑋)𝐼𝑋))
44 simp-7r 780 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴)))
4544simpld 490 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ ((𝑀𝑋)𝐼𝑥))
463, 4, 5, 26, 40, 33, 30, 28, 43, 45tgbtwnexch3 25849 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ (𝐴𝐼𝑥))
473, 4, 5, 26, 33, 30, 28, 46tgbtwncom 25843 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ (𝑥𝐼𝐴))
483, 4, 5, 26, 40, 30, 28, 45tgbtwncom 25843 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ (𝑥𝐼(𝑀𝑋)))
493, 4, 5, 26, 40, 33, 30, 43tgbtwncom 25843 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑋𝐼(𝑀𝑋)))
503, 4, 5, 26, 28, 30, 33, 40, 48, 49tgbtwnexch2 25851 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑥𝐼(𝑀𝑋)))
51 simpllr 766 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴)))
5251simpld 490 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ (𝑥𝐼𝑧))
533, 4, 5, 26, 28, 33, 40, 37, 50, 52tgbtwnexch3 25849 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ (𝐴𝐼𝑧))
543, 4, 5, 26, 33, 40, 37, 53tgbtwncom 25843 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ (𝑧𝐼𝐴))
55 simp-4r 774 . . . . . . . . . . . 12 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → 𝑦𝑃)
5655ad2antrr 716 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑦𝑃)
573, 4, 5, 6, 7, 26, 33, 12, 36mirbtwn 26013 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ ((𝑀𝑌)𝐼𝑌))
58 simp-5r 776 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
5958simpld 490 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ ((𝑀𝑌)𝐼𝑦))
603, 4, 5, 26, 42, 33, 36, 56, 57, 59tgbtwnexch3 25849 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ (𝐴𝐼𝑦))
613, 4, 5, 26, 33, 36, 56, 60tgbtwncom 25843 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ (𝑦𝐼𝐴))
623, 4, 5, 6, 7, 26, 33, 12, 30mircgr 26012 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 (𝑀𝑋)) = (𝐴 𝑋))
6358simprd 491 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝑦) = (𝑋 𝐴))
643, 4, 5, 26, 36, 56, 30, 33, 63tgcgrcomlr 25835 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝑌) = (𝐴 𝑋))
6562, 64eqtr4d 2817 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 (𝑀𝑋)) = (𝑦 𝑌))
6651simprd 491 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑋) 𝑧) = (𝑌 𝐴))
673, 4, 5, 26, 33, 40, 37, 56, 36, 33, 53, 61, 65, 66tgcgrextend 25840 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑧) = (𝑦 𝐴))
6844simprd 491 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝑥) = (𝑌 𝐴))
6968eqcomd 2784 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝐴) = (𝑋 𝑥))
703, 4, 5, 26, 56, 36, 33, 33, 30, 28, 61, 46, 64, 69tgcgrextend 25840 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝐴) = (𝐴 𝑥))
7167, 70eqtr2d 2815 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑥) = (𝐴 𝑧))
723, 4, 5, 26, 33, 28, 33, 37, 71tgcgrcomlr 25835 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝐴) = (𝑧 𝐴))
7362eqcomd 2784 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑋) = (𝐴 (𝑀𝑋)))
743, 4, 5, 26, 33, 30, 33, 40, 73tgcgrcomlr 25835 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝐴) = ((𝑀𝑋) 𝐴))
75 simplr 759 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑡𝑃)
763, 4, 5, 26, 42, 36, 56, 59tgbtwncom 25843 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ (𝑦𝐼(𝑀𝑌)))
773, 4, 5, 26, 42, 33, 36, 57tgbtwncom 25843 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑌𝐼(𝑀𝑌)))
783, 4, 5, 26, 56, 36, 33, 42, 76, 77tgbtwnexch2 25851 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑦𝐼(𝑀𝑌)))
79 simpr 479 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴)))
8079simpld 490 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ (𝑦𝐼𝑡))
813, 4, 5, 26, 56, 33, 42, 75, 78, 80tgbtwnexch3 25849 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ (𝐴𝐼𝑡))
823, 4, 5, 26, 33, 42, 75, 81tgbtwncom 25843 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ (𝑡𝐼𝐴))
833, 4, 5, 26, 30, 28, 36, 33, 68tgcgrcomlr 25835 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑋) = (𝐴 𝑌))
843, 4, 5, 6, 7, 26, 33, 12, 36mircgr 26012 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 (𝑀𝑌)) = (𝐴 𝑌))
8583, 84eqtr4d 2817 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑋) = (𝐴 (𝑀𝑌)))
8679simprd 491 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑌) 𝑡) = (𝑋 𝐴))
8786eqcomd 2784 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝐴) = ((𝑀𝑌) 𝑡))
883, 4, 5, 26, 28, 30, 33, 33, 42, 75, 47, 81, 85, 87tgcgrextend 25840 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝐴) = (𝐴 𝑡))
893, 4, 5, 26, 33, 75axtgcgrrflx 25817 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑡) = (𝑡 𝐴))
9088, 89eqtrd 2814 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝐴) = (𝑡 𝐴))
913, 4, 5, 26, 28, 33, 75, 33, 90tgcgrcomlr 25835 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑥) = (𝐴 𝑡))
9270, 91, 893eqtrd 2818 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝐴) = (𝑡 𝐴))
933, 4, 5, 26, 33, 42, 33, 36, 84tgcgrcomlr 25835 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑌) 𝐴) = (𝑌 𝐴))
9493eqcomd 2784 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝐴) = ((𝑀𝑌) 𝐴))
953, 4, 5, 26, 75, 37axtgcgrrflx 25817 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑡 𝑧) = (𝑧 𝑡))
96 simp-9r 784 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋𝐴)
9796neneqd 2974 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ¬ 𝑋 = 𝐴)
9826adantr 474 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝐺 ∈ TarskiG)
9933adantr 474 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴𝑃)
10030adantr 474 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋𝑃)
10146adantr 474 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝑥))
102 simpr 479 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
103102oveq2d 6940 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → (𝐴𝐼𝑥) = (𝐴𝐼𝐴))
104101, 103eleqtrd 2861 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝐴))
1053, 4, 5, 98, 99, 100, 104axtgbtwnid 25821 . . . . . . . . . . . . . . 15 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 = 𝑋)
106105eqcomd 2784 . . . . . . . . . . . . . 14 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 = 𝐴)
10797, 106mtand 806 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ¬ 𝑥 = 𝐴)
108107neqned 2976 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑥𝐴)
1093, 4, 5, 26, 28, 33, 40, 37, 50, 52tgbtwnexch 25853 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑥𝐼𝑧))
1103, 4, 5, 26, 56, 33, 42, 75, 78, 80tgbtwnexch 25853 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑦𝐼𝑡))
1113, 4, 5, 26, 56, 33, 75, 110tgbtwncom 25843 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑡𝐼𝑦))
1123, 4, 5, 26, 56, 33axtgcgrrflx 25817 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝐴) = (𝐴 𝑦))
11367, 112eqtrd 2814 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑧) = (𝐴 𝑦))
1143, 4, 5, 26, 28, 75axtgcgrrflx 25817 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑡) = (𝑡 𝑥))
11591eqcomd 2784 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑡) = (𝐴 𝑥))
1163, 4, 5, 26, 28, 33, 37, 75, 33, 56, 75, 28, 108, 109, 111, 90, 113, 114, 115axtg5seg 25820 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑧 𝑡) = (𝑦 𝑥))
11795, 116eqtr2d 2815 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝑥) = (𝑡 𝑧))
1183, 4, 5, 26, 56, 36, 33, 28, 75, 42, 33, 37, 61, 82, 92, 94, 117, 71tgifscgr 25863 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝑥) = ((𝑀𝑌) 𝑧))
1193, 4, 5, 26, 36, 28, 42, 37, 118tgcgrcomlr 25835 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑌) = (𝑧 (𝑀𝑌)))
12084eqcomd 2784 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑌) = (𝐴 (𝑀𝑌)))
1213, 4, 5, 26, 28, 30, 33, 36, 37, 40, 33, 42, 47, 54, 72, 74, 119, 120tgifscgr 25863 . . . . . . 7 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝑌) = ((𝑀𝑋) (𝑀𝑌)))
122121eqcomd 2784 . . . . . 6 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
123 simp-6l 777 . . . . . . 7 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → (𝜑𝑋𝐴))
124 simpllr 766 . . . . . . 7 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
12524ad2antrr 716 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝐺 ∈ TarskiG)
126 simplr 759 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝑦𝑃)
12741ad2antrr 716 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → (𝑀𝑌) ∈ 𝑃)
12829ad2antrr 716 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝑋𝑃)
12931ad2antrr 716 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝐴𝑃)
1303, 4, 5, 125, 126, 127, 128, 129axtgsegcon 25819 . . . . . . 7 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → ∃𝑡𝑃 ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴)))
131123, 55, 124, 130syl21anc 828 . . . . . 6 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → ∃𝑡𝑃 ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴)))
132122, 131r19.29a 3264 . . . . 5 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
1333, 4, 5, 25, 27, 39, 35, 32axtgsegcon 25819 . . . . . 6 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → ∃𝑧𝑃 ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴)))
134133ad2antrr 716 . . . . 5 ((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → ∃𝑧𝑃 ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴)))
135132, 134r19.29a 3264 . . . 4 ((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
1363, 4, 5, 24, 41, 34, 29, 31axtgsegcon 25819 . . . . 5 ((𝜑𝑋𝐴) → ∃𝑦𝑃 (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
137136ad2antrr 716 . . . 4 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → ∃𝑦𝑃 (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
138135, 137r19.29a 3264 . . 3 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
1393, 4, 5, 24, 38, 29, 34, 31axtgsegcon 25819 . . 3 ((𝜑𝑋𝐴) → ∃𝑥𝑃 (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴)))
140138, 139r19.29a 3264 . 2 ((𝜑𝑋𝐴) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
14123, 140pm2.61dane 3057 1 (𝜑 → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wcel 2107  wne 2969  wrex 3091  cfv 6137  (class class class)co 6924  Basecbs 16259  distcds 16351  TarskiGcstrkg 25785  Itvcitv 25791  LineGclng 25792  pInvGcmir 26007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-oadd 7849  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-nn 11379  df-2 11442  df-n0 11647  df-xnn0 11719  df-z 11733  df-uz 11997  df-fz 12648  df-hash 13440  df-trkgc 25803  df-trkgb 25804  df-trkgcb 25805  df-trkg 25808  df-mir 26008
This theorem is referenced by:  mirbtwni  26026  mircgrs  26028  mirmot  26030  miduniq  26040  ragcom  26053  colperpexlem1  26082  lmiisolem  26148  hypcgrlem2  26152  hypcgr  26153
  Copyright terms: Public domain W3C validator