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

Theorem miriso 28467
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 484 . . . 4 ((𝜑𝑋 = 𝐴) → 𝑋 = 𝐴)
21oveq1d 7429 . . 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 480 . . . 4 ((𝜑𝑋 = 𝐴) → 𝐺 ∈ TarskiG)
10 mirval.a . . . . 5 (𝜑𝐴𝑃)
1110adantr 480 . . . 4 ((𝜑𝑋 = 𝐴) → 𝐴𝑃)
12 mirfv.m . . . 4 𝑀 = (𝑆𝐴)
13 miriso.2 . . . . 5 (𝜑𝑌𝑃)
1413adantr 480 . . . 4 ((𝜑𝑋 = 𝐴) → 𝑌𝑃)
153, 4, 5, 6, 7, 9, 11, 12, 14mircgr 28454 . . 3 ((𝜑𝑋 = 𝐴) → (𝐴 (𝑀𝑌)) = (𝐴 𝑌))
16 miriso.1 . . . . . 6 (𝜑𝑋𝑃)
1716adantr 480 . . . . 5 ((𝜑𝑋 = 𝐴) → 𝑋𝑃)
181eqcomd 2734 . . . . . 6 ((𝜑𝑋 = 𝐴) → 𝐴 = 𝑋)
1918oveq2d 7430 . . . . 5 ((𝜑𝑋 = 𝐴) → (𝐴 𝐴) = (𝐴 𝑋))
203, 4, 5, 9, 11, 17tgbtwntriv1 28288 . . . . 5 ((𝜑𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐼𝑋))
213, 4, 5, 6, 7, 9, 11, 12, 17, 11, 19, 20ismir 28456 . . . 4 ((𝜑𝑋 = 𝐴) → 𝐴 = (𝑀𝑋))
2221oveq1d 7429 . . 3 ((𝜑𝑋 = 𝐴) → (𝐴 (𝑀𝑌)) = ((𝑀𝑋) (𝑀𝑌)))
232, 15, 223eqtr2rd 2775 . 2 ((𝜑𝑋 = 𝐴) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
248adantr 480 . . . . . . . . . 10 ((𝜑𝑋𝐴) → 𝐺 ∈ TarskiG)
2524ad2antrr 725 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝐺 ∈ TarskiG)
2625ad6antr 735 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐺 ∈ TarskiG)
27 simplr 768 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝑥𝑃)
2827ad6antr 735 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑥𝑃)
2916adantr 480 . . . . . . . . 9 ((𝜑𝑋𝐴) → 𝑋𝑃)
3029ad8antr 739 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋𝑃)
3110adantr 480 . . . . . . . . . 10 ((𝜑𝑋𝐴) → 𝐴𝑃)
3231ad2antrr 725 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝐴𝑃)
3332ad6antr 735 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴𝑃)
3413adantr 480 . . . . . . . . . 10 ((𝜑𝑋𝐴) → 𝑌𝑃)
3534ad2antrr 725 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → 𝑌𝑃)
3635ad6antr 735 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌𝑃)
37 simp-4r 783 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑧𝑃)
383, 4, 5, 6, 7, 24, 31, 12, 29mircl 28458 . . . . . . . . . 10 ((𝜑𝑋𝐴) → (𝑀𝑋) ∈ 𝑃)
3938ad2antrr 725 . . . . . . . . 9 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → (𝑀𝑋) ∈ 𝑃)
4039ad6antr 735 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ 𝑃)
413, 4, 5, 6, 7, 24, 31, 12, 34mircl 28458 . . . . . . . . 9 ((𝜑𝑋𝐴) → (𝑀𝑌) ∈ 𝑃)
4241ad8antr 739 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ 𝑃)
433, 4, 5, 6, 7, 26, 33, 12, 30mirbtwn 28455 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ ((𝑀𝑋)𝐼𝑋))
44 simp-7r 789 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴)))
4544simpld 494 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ ((𝑀𝑋)𝐼𝑥))
463, 4, 5, 26, 40, 33, 30, 28, 43, 45tgbtwnexch3 28291 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ (𝐴𝐼𝑥))
473, 4, 5, 26, 33, 30, 28, 46tgbtwncom 28285 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ (𝑥𝐼𝐴))
483, 4, 5, 26, 40, 30, 28, 45tgbtwncom 28285 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋 ∈ (𝑥𝐼(𝑀𝑋)))
493, 4, 5, 26, 40, 33, 30, 43tgbtwncom 28285 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑋𝐼(𝑀𝑋)))
503, 4, 5, 26, 28, 30, 33, 40, 48, 49tgbtwnexch2 28293 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑥𝐼(𝑀𝑋)))
51 simpllr 775 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴)))
5251simpld 494 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ (𝑥𝐼𝑧))
533, 4, 5, 26, 28, 33, 40, 37, 50, 52tgbtwnexch3 28291 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ (𝐴𝐼𝑧))
543, 4, 5, 26, 33, 40, 37, 53tgbtwncom 28285 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑋) ∈ (𝑧𝐼𝐴))
55 simp-4r 783 . . . . . . . . . . . 12 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → 𝑦𝑃)
5655ad2antrr 725 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑦𝑃)
573, 4, 5, 6, 7, 26, 33, 12, 36mirbtwn 28455 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ ((𝑀𝑌)𝐼𝑌))
58 simp-5r 785 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
5958simpld 494 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ ((𝑀𝑌)𝐼𝑦))
603, 4, 5, 26, 42, 33, 36, 56, 57, 59tgbtwnexch3 28291 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ (𝐴𝐼𝑦))
613, 4, 5, 26, 33, 36, 56, 60tgbtwncom 28285 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ (𝑦𝐼𝐴))
623, 4, 5, 6, 7, 26, 33, 12, 30mircgr 28454 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 (𝑀𝑋)) = (𝐴 𝑋))
6358simprd 495 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝑦) = (𝑋 𝐴))
643, 4, 5, 26, 36, 56, 30, 33, 63tgcgrcomlr 28277 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝑌) = (𝐴 𝑋))
6562, 64eqtr4d 2771 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 (𝑀𝑋)) = (𝑦 𝑌))
6651simprd 495 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑋) 𝑧) = (𝑌 𝐴))
673, 4, 5, 26, 33, 40, 37, 56, 36, 33, 53, 61, 65, 66tgcgrextend 28282 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑧) = (𝑦 𝐴))
6844simprd 495 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝑥) = (𝑌 𝐴))
6968eqcomd 2734 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝐴) = (𝑋 𝑥))
703, 4, 5, 26, 56, 36, 33, 33, 30, 28, 61, 46, 64, 69tgcgrextend 28282 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝐴) = (𝐴 𝑥))
7167, 70eqtr2d 2769 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑥) = (𝐴 𝑧))
723, 4, 5, 26, 33, 28, 33, 37, 71tgcgrcomlr 28277 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝐴) = (𝑧 𝐴))
7362eqcomd 2734 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑋) = (𝐴 (𝑀𝑋)))
743, 4, 5, 26, 33, 30, 33, 40, 73tgcgrcomlr 28277 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝐴) = ((𝑀𝑋) 𝐴))
75 simplr 768 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑡𝑃)
763, 4, 5, 26, 42, 36, 56, 59tgbtwncom 28285 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑌 ∈ (𝑦𝐼(𝑀𝑌)))
773, 4, 5, 26, 42, 33, 36, 57tgbtwncom 28285 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑌𝐼(𝑀𝑌)))
783, 4, 5, 26, 56, 36, 33, 42, 76, 77tgbtwnexch2 28293 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑦𝐼(𝑀𝑌)))
79 simpr 484 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴)))
8079simpld 494 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ (𝑦𝐼𝑡))
813, 4, 5, 26, 56, 33, 42, 75, 78, 80tgbtwnexch3 28291 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ (𝐴𝐼𝑡))
823, 4, 5, 26, 33, 42, 75, 81tgbtwncom 28285 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑀𝑌) ∈ (𝑡𝐼𝐴))
833, 4, 5, 26, 30, 28, 36, 33, 68tgcgrcomlr 28277 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑋) = (𝐴 𝑌))
843, 4, 5, 6, 7, 26, 33, 12, 36mircgr 28454 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 (𝑀𝑌)) = (𝐴 𝑌))
8583, 84eqtr4d 2771 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑋) = (𝐴 (𝑀𝑌)))
8679simprd 495 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑌) 𝑡) = (𝑋 𝐴))
8786eqcomd 2734 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝐴) = ((𝑀𝑌) 𝑡))
883, 4, 5, 26, 28, 30, 33, 33, 42, 75, 47, 81, 85, 87tgcgrextend 28282 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝐴) = (𝐴 𝑡))
893, 4, 5, 26, 33, 75axtgcgrrflx 28259 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑡) = (𝑡 𝐴))
9088, 89eqtrd 2768 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝐴) = (𝑡 𝐴))
913, 4, 5, 26, 28, 33, 75, 33, 90tgcgrcomlr 28277 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑥) = (𝐴 𝑡))
9270, 91, 893eqtrd 2772 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝐴) = (𝑡 𝐴))
933, 4, 5, 26, 33, 42, 33, 36, 84tgcgrcomlr 28277 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑌) 𝐴) = (𝑌 𝐴))
9493eqcomd 2734 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝐴) = ((𝑀𝑌) 𝐴))
953, 4, 5, 26, 75, 37axtgcgrrflx 28259 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑡 𝑧) = (𝑧 𝑡))
96 simp-9r 793 . . . . . . . . . . . . . . 15 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑋𝐴)
9796neneqd 2941 . . . . . . . . . . . . . 14 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ¬ 𝑋 = 𝐴)
9826adantr 480 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝐺 ∈ TarskiG)
9933adantr 480 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴𝑃)
10030adantr 480 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋𝑃)
10146adantr 480 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝑥))
102 simpr 484 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
103102oveq2d 7430 . . . . . . . . . . . . . . . . 17 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → (𝐴𝐼𝑥) = (𝐴𝐼𝐴))
104101, 103eleqtrd 2831 . . . . . . . . . . . . . . . 16 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝐴))
1053, 4, 5, 98, 99, 100, 104axtgbtwnid 28263 . . . . . . . . . . . . . . 15 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 = 𝑋)
106105eqcomd 2734 . . . . . . . . . . . . . 14 (((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 = 𝐴)
10797, 106mtand 815 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ¬ 𝑥 = 𝐴)
108107neqned 2943 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝑥𝐴)
1093, 4, 5, 26, 28, 33, 40, 37, 50, 52tgbtwnexch 28295 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑥𝐼𝑧))
1103, 4, 5, 26, 56, 33, 42, 75, 78, 80tgbtwnexch 28295 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑦𝐼𝑡))
1113, 4, 5, 26, 56, 33, 75, 110tgbtwncom 28285 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → 𝐴 ∈ (𝑡𝐼𝑦))
1123, 4, 5, 26, 56, 33axtgcgrrflx 28259 . . . . . . . . . . . . 13 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝐴) = (𝐴 𝑦))
11367, 112eqtrd 2768 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑧) = (𝐴 𝑦))
1143, 4, 5, 26, 28, 75axtgcgrrflx 28259 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑡) = (𝑡 𝑥))
11591eqcomd 2734 . . . . . . . . . . . 12 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑡) = (𝐴 𝑥))
1163, 4, 5, 26, 28, 33, 37, 75, 33, 56, 75, 28, 108, 109, 111, 90, 113, 114, 115axtg5seg 28262 . . . . . . . . . . 11 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑧 𝑡) = (𝑦 𝑥))
11795, 116eqtr2d 2769 . . . . . . . . . 10 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑦 𝑥) = (𝑡 𝑧))
1183, 4, 5, 26, 56, 36, 33, 28, 75, 42, 33, 37, 61, 82, 92, 94, 117, 71tgifscgr 28305 . . . . . . . . 9 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑌 𝑥) = ((𝑀𝑌) 𝑧))
1193, 4, 5, 26, 36, 28, 42, 37, 118tgcgrcomlr 28277 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑥 𝑌) = (𝑧 (𝑀𝑌)))
12084eqcomd 2734 . . . . . . . 8 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝐴 𝑌) = (𝐴 (𝑀𝑌)))
1213, 4, 5, 26, 28, 30, 33, 36, 37, 40, 33, 42, 47, 54, 72, 74, 119, 120tgifscgr 28305 . . . . . . 7 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → (𝑋 𝑌) = ((𝑀𝑋) (𝑀𝑌)))
122121eqcomd 2734 . . . . . 6 ((((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) ∧ 𝑡𝑃) ∧ ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
123 simp-6l 786 . . . . . . 7 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → (𝜑𝑋𝐴))
124 simpllr 775 . . . . . . 7 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
12524ad2antrr 725 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝐺 ∈ TarskiG)
126 simplr 768 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝑦𝑃)
12741ad2antrr 725 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → (𝑀𝑌) ∈ 𝑃)
12829ad2antrr 725 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝑋𝑃)
12931ad2antrr 725 . . . . . . . 8 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → 𝐴𝑃)
1303, 4, 5, 125, 126, 127, 128, 129axtgsegcon 28261 . . . . . . 7 ((((𝜑𝑋𝐴) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → ∃𝑡𝑃 ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴)))
131123, 55, 124, 130syl21anc 837 . . . . . 6 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → ∃𝑡𝑃 ((𝑀𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀𝑌) 𝑡) = (𝑋 𝐴)))
132122, 131r19.29a 3158 . . . . 5 ((((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) ∧ 𝑧𝑃) ∧ ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
1333, 4, 5, 25, 27, 39, 35, 32axtgsegcon 28261 . . . . . 6 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → ∃𝑧𝑃 ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴)))
134133ad2antrr 725 . . . . 5 ((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → ∃𝑧𝑃 ((𝑀𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀𝑋) 𝑧) = (𝑌 𝐴)))
135132, 134r19.29a 3158 . . . 4 ((((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) ∧ 𝑦𝑃) ∧ (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
1363, 4, 5, 24, 41, 34, 29, 31axtgsegcon 28261 . . . . 5 ((𝜑𝑋𝐴) → ∃𝑦𝑃 (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
137136ad2antrr 725 . . . 4 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → ∃𝑦𝑃 (𝑌 ∈ ((𝑀𝑌)𝐼𝑦) ∧ (𝑌 𝑦) = (𝑋 𝐴)))
138135, 137r19.29a 3158 . . 3 ((((𝜑𝑋𝐴) ∧ 𝑥𝑃) ∧ (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴))) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
1393, 4, 5, 24, 38, 29, 34, 31axtgsegcon 28261 . . 3 ((𝜑𝑋𝐴) → ∃𝑥𝑃 (𝑋 ∈ ((𝑀𝑋)𝐼𝑥) ∧ (𝑋 𝑥) = (𝑌 𝐴)))
140138, 139r19.29a 3158 . 2 ((𝜑𝑋𝐴) → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
14123, 140pm2.61dane 3025 1 (𝜑 → ((𝑀𝑋) (𝑀𝑌)) = (𝑋 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1534  wcel 2099  wne 2936  wrex 3066  cfv 6542  (class class class)co 7414  Basecbs 17173  distcds 17235  TarskiGcstrkg 28224  Itvcitv 28230  LineGclng 28231  pInvGcmir 28449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11188  ax-resscn 11189  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-mulcom 11196  ax-addass 11197  ax-mulass 11198  ax-distr 11199  ax-i2m1 11200  ax-1ne0 11201  ax-1rid 11202  ax-rnegex 11203  ax-rrecex 11204  ax-cnre 11205  ax-pre-lttri 11206  ax-pre-lttrn 11207  ax-pre-ltadd 11208  ax-pre-mulgt0 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-oadd 8484  df-er 8718  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-dju 9918  df-card 9956  df-pnf 11274  df-mnf 11275  df-xr 11276  df-ltxr 11277  df-le 11278  df-sub 11470  df-neg 11471  df-nn 12237  df-2 12299  df-n0 12497  df-xnn0 12569  df-z 12583  df-uz 12847  df-fz 13511  df-hash 14316  df-trkgc 28245  df-trkgb 28246  df-trkgcb 28247  df-trkg 28250  df-mir 28450
This theorem is referenced by:  mirbtwni  28468  mircgrs  28470  mirmot  28472  miduniq  28482  ragcom  28495  colperpexlem1  28527  lmiisolem  28593  hypcgrlem2  28597  hypcgr  28598
  Copyright terms: Public domain W3C validator