| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 = 𝐴) |
| 2 | 1 | oveq1d 7446 |
. . 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) |
| 9 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐺 ∈ TarskiG) |
| 10 | | mirval.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 11 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ 𝑃) |
| 12 | | mirfv.m |
. . . 4
⊢ 𝑀 = (𝑆‘𝐴) |
| 13 | | miriso.2 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
| 14 | 13 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑌 ∈ 𝑃) |
| 15 | 3, 4, 5, 6, 7, 9, 11, 12, 14 | mircgr 28665 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − (𝑀‘𝑌)) = (𝐴 − 𝑌)) |
| 16 | | miriso.1 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
| 17 | 16 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝑋 ∈ 𝑃) |
| 18 | 1 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = 𝑋) |
| 19 | 18 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − 𝐴) = (𝐴 − 𝑋)) |
| 20 | 3, 4, 5, 9, 11, 17 | tgbtwntriv1 28499 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 ∈ (𝐴𝐼𝑋)) |
| 21 | 3, 4, 5, 6, 7, 9, 11, 12, 17, 11, 19, 20 | ismir 28667 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → 𝐴 = (𝑀‘𝑋)) |
| 22 | 21 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → (𝐴 − (𝑀‘𝑌)) = ((𝑀‘𝑋) − (𝑀‘𝑌))) |
| 23 | 2, 15, 22 | 3eqtr2rd 2784 |
. 2
⊢ ((𝜑 ∧ 𝑋 = 𝐴) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌)) |
| 24 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝐺 ∈ TarskiG) |
| 25 | 24 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝐺 ∈ TarskiG) |
| 26 | 25 | ad6antr 736 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐺 ∈ TarskiG) |
| 27 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝑥 ∈ 𝑃) |
| 28 | 27 | ad6antr 736 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑥 ∈ 𝑃) |
| 29 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝑋 ∈ 𝑃) |
| 30 | 29 | ad8antr 740 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ 𝑃) |
| 31 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝐴 ∈ 𝑃) |
| 32 | 31 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝐴 ∈ 𝑃) |
| 33 | 32 | ad6antr 736 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ 𝑃) |
| 34 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → 𝑌 ∈ 𝑃) |
| 35 | 34 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → 𝑌 ∈ 𝑃) |
| 36 | 35 | ad6antr 736 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ 𝑃) |
| 37 | | simp-4r 784 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑧 ∈ 𝑃) |
| 38 | 3, 4, 5, 6, 7, 24,
31, 12, 29 | mircl 28669 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → (𝑀‘𝑋) ∈ 𝑃) |
| 39 | 38 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → (𝑀‘𝑋) ∈ 𝑃) |
| 40 | 39 | ad6antr 736 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ 𝑃) |
| 41 | 3, 4, 5, 6, 7, 24,
31, 12, 34 | mircl 28669 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → (𝑀‘𝑌) ∈ 𝑃) |
| 42 | 41 | ad8antr 740 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ 𝑃) |
| 43 | 3, 4, 5, 6, 7, 26,
33, 12, 30 | mirbtwn 28666 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ ((𝑀‘𝑋)𝐼𝑋)) |
| 44 | | simp-7r 790 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) |
| 45 | 44 | simpld 494 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥)) |
| 46 | 3, 4, 5, 26, 40, 33, 30, 28, 43, 45 | tgbtwnexch3 28502 |
. . . . . . . . 9
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝐴𝐼𝑥)) |
| 47 | 3, 4, 5, 26, 33, 30, 28, 46 | tgbtwncom 28496 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝑥𝐼𝐴)) |
| 48 | 3, 4, 5, 26, 40, 30, 28, 45 | tgbtwncom 28496 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ∈ (𝑥𝐼(𝑀‘𝑋))) |
| 49 | 3, 4, 5, 26, 40, 33, 30, 43 | tgbtwncom 28496 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑋))) |
| 50 | 3, 4, 5, 26, 28, 30, 33, 40, 48, 49 | tgbtwnexch2 28504 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑥𝐼(𝑀‘𝑋))) |
| 51 | | simpllr 776 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) |
| 52 | 51 | simpld 494 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝑥𝐼𝑧)) |
| 53 | 3, 4, 5, 26, 28, 33, 40, 37, 50, 52 | tgbtwnexch3 28502 |
. . . . . . . . 9
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝐴𝐼𝑧)) |
| 54 | 3, 4, 5, 26, 33, 40, 37, 53 | tgbtwncom 28496 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑋) ∈ (𝑧𝐼𝐴)) |
| 55 | | simp-4r 784 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → 𝑦 ∈ 𝑃) |
| 56 | 55 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑦 ∈ 𝑃) |
| 57 | 3, 4, 5, 6, 7, 26,
33, 12, 36 | mirbtwn 28666 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ ((𝑀‘𝑌)𝐼𝑌)) |
| 58 | | simp-5r 786 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) |
| 59 | 58 | simpld 494 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦)) |
| 60 | 3, 4, 5, 26, 42, 33, 36, 56, 57, 59 | tgbtwnexch3 28502 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝐴𝐼𝑦)) |
| 61 | 3, 4, 5, 26, 33, 36, 56, 60 | tgbtwncom 28496 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝑦𝐼𝐴)) |
| 62 | 3, 4, 5, 6, 7, 26,
33, 12, 30 | mircgr 28665 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑋)) = (𝐴 − 𝑋)) |
| 63 | 58 | simprd 495 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝑦) = (𝑋 − 𝐴)) |
| 64 | 3, 4, 5, 26, 36, 56, 30, 33, 63 | tgcgrcomlr 28488 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝑌) = (𝐴 − 𝑋)) |
| 65 | 62, 64 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑋)) = (𝑦 − 𝑌)) |
| 66 | 51 | simprd 495 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴)) |
| 67 | 3, 4, 5, 26, 33, 40, 37, 56, 36, 33, 53, 61, 65, 66 | tgcgrextend 28493 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑧) = (𝑦 − 𝐴)) |
| 68 | 44 | simprd 495 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝑥) = (𝑌 − 𝐴)) |
| 69 | 68 | eqcomd 2743 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝐴) = (𝑋 − 𝑥)) |
| 70 | 3, 4, 5, 26, 56, 36, 33, 33, 30, 28, 61, 46, 64, 69 | tgcgrextend 28493 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝐴 − 𝑥)) |
| 71 | 67, 70 | eqtr2d 2778 |
. . . . . . . . 9
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑥) = (𝐴 − 𝑧)) |
| 72 | 3, 4, 5, 26, 33, 28, 33, 37, 71 | tgcgrcomlr 28488 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝑧 − 𝐴)) |
| 73 | 62 | eqcomd 2743 |
. . . . . . . . 9
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑋) = (𝐴 − (𝑀‘𝑋))) |
| 74 | 3, 4, 5, 26, 33, 30, 33, 40, 73 | tgcgrcomlr 28488 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝐴) = ((𝑀‘𝑋) − 𝐴)) |
| 75 | | simplr 769 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑡 ∈ 𝑃) |
| 76 | 3, 4, 5, 26, 42, 36, 56, 59 | tgbtwncom 28496 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑌 ∈ (𝑦𝐼(𝑀‘𝑌))) |
| 77 | 3, 4, 5, 26, 42, 33, 36, 57 | tgbtwncom 28496 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑌𝐼(𝑀‘𝑌))) |
| 78 | 3, 4, 5, 26, 56, 36, 33, 42, 76, 77 | tgbtwnexch2 28504 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑦𝐼(𝑀‘𝑌))) |
| 79 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) |
| 80 | 79 | simpld 494 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝑦𝐼𝑡)) |
| 81 | 3, 4, 5, 26, 56, 33, 42, 75, 78, 80 | tgbtwnexch3 28502 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝐴𝐼𝑡)) |
| 82 | 3, 4, 5, 26, 33, 42, 75, 81 | tgbtwncom 28496 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ (𝑡𝐼𝐴)) |
| 83 | 3, 4, 5, 26, 30, 28, 36, 33, 68 | tgcgrcomlr 28488 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑋) = (𝐴 − 𝑌)) |
| 84 | 3, 4, 5, 6, 7, 26,
33, 12, 36 | mircgr 28665 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − (𝑀‘𝑌)) = (𝐴 − 𝑌)) |
| 85 | 83, 84 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑋) = (𝐴 − (𝑀‘𝑌))) |
| 86 | 79 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴)) |
| 87 | 86 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝐴) = ((𝑀‘𝑌) − 𝑡)) |
| 88 | 3, 4, 5, 26, 28, 30, 33, 33, 42, 75, 47, 81, 85, 87 | tgcgrextend 28493 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝐴 − 𝑡)) |
| 89 | 3, 4, 5, 26, 33, 75 | axtgcgrrflx 28470 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑡) = (𝑡 − 𝐴)) |
| 90 | 88, 89 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝐴) = (𝑡 − 𝐴)) |
| 91 | 3, 4, 5, 26, 28, 33, 75, 33, 90 | tgcgrcomlr 28488 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑥) = (𝐴 − 𝑡)) |
| 92 | 70, 91, 89 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝑡 − 𝐴)) |
| 93 | 3, 4, 5, 26, 33, 42, 33, 36, 84 | tgcgrcomlr 28488 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑌) − 𝐴) = (𝑌 − 𝐴)) |
| 94 | 93 | eqcomd 2743 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝐴) = ((𝑀‘𝑌) − 𝐴)) |
| 95 | 3, 4, 5, 26, 75, 37 | axtgcgrrflx 28470 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑡 − 𝑧) = (𝑧 − 𝑡)) |
| 96 | | simp-9r 794 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑋 ≠ 𝐴) |
| 97 | 96 | neneqd 2945 |
. . . . . . . . . . . . . 14
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ¬ 𝑋 = 𝐴) |
| 98 | 26 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐺 ∈ TarskiG) |
| 99 | 33 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 ∈ 𝑃) |
| 100 | 30 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ 𝑃) |
| 101 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝑥)) |
| 102 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴) |
| 103 | 102 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → (𝐴𝐼𝑥) = (𝐴𝐼𝐴)) |
| 104 | 101, 103 | eleqtrd 2843 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 ∈ (𝐴𝐼𝐴)) |
| 105 | 3, 4, 5, 98, 99, 100, 104 | axtgbtwnid 28474 |
. . . . . . . . . . . . . . 15
⊢
(((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝐴 = 𝑋) |
| 106 | 105 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢
(((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) ∧ 𝑥 = 𝐴) → 𝑋 = 𝐴) |
| 107 | 97, 106 | mtand 816 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ¬ 𝑥 = 𝐴) |
| 108 | 107 | neqned 2947 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝑥 ≠ 𝐴) |
| 109 | 3, 4, 5, 26, 28, 33, 40, 37, 50, 52 | tgbtwnexch 28506 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑥𝐼𝑧)) |
| 110 | 3, 4, 5, 26, 56, 33, 42, 75, 78, 80 | tgbtwnexch 28506 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑦𝐼𝑡)) |
| 111 | 3, 4, 5, 26, 56, 33, 75, 110 | tgbtwncom 28496 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → 𝐴 ∈ (𝑡𝐼𝑦)) |
| 112 | 3, 4, 5, 26, 56, 33 | axtgcgrrflx 28470 |
. . . . . . . . . . . . 13
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝐴) = (𝐴 − 𝑦)) |
| 113 | 67, 112 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑧) = (𝐴 − 𝑦)) |
| 114 | 3, 4, 5, 26, 28, 75 | axtgcgrrflx 28470 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑡) = (𝑡 − 𝑥)) |
| 115 | 91 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑡) = (𝐴 − 𝑥)) |
| 116 | 3, 4, 5, 26, 28, 33, 37, 75, 33, 56, 75, 28, 108, 109, 111, 90, 113, 114, 115 | axtg5seg 28473 |
. . . . . . . . . . 11
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑧 − 𝑡) = (𝑦 − 𝑥)) |
| 117 | 95, 116 | eqtr2d 2778 |
. . . . . . . . . 10
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑦 − 𝑥) = (𝑡 − 𝑧)) |
| 118 | 3, 4, 5, 26, 56, 36, 33, 28, 75, 42, 33, 37, 61, 82, 92, 94, 117, 71 | tgifscgr 28516 |
. . . . . . . . 9
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑌 − 𝑥) = ((𝑀‘𝑌) − 𝑧)) |
| 119 | 3, 4, 5, 26, 36, 28, 42, 37, 118 | tgcgrcomlr 28488 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑥 − 𝑌) = (𝑧 − (𝑀‘𝑌))) |
| 120 | 84 | eqcomd 2743 |
. . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝐴 − 𝑌) = (𝐴 − (𝑀‘𝑌))) |
| 121 | 3, 4, 5, 26, 28, 30, 33, 36, 37, 40, 33, 42, 47, 54, 72, 74, 119, 120 | tgifscgr 28516 |
. . . . . . 7
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → (𝑋 − 𝑌) = ((𝑀‘𝑋) − (𝑀‘𝑌))) |
| 122 | 121 | eqcomd 2743 |
. . . . . 6
⊢
((((((((((𝜑 ∧
𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) ∧ 𝑡 ∈ 𝑃) ∧ ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌)) |
| 123 | | simp-6l 787 |
. . . . . . 7
⊢
((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → (𝜑 ∧ 𝑋 ≠ 𝐴)) |
| 124 | | simpllr 776 |
. . . . . . 7
⊢
((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) |
| 125 | 24 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝐺 ∈ TarskiG) |
| 126 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝑦 ∈ 𝑃) |
| 127 | 41 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → (𝑀‘𝑌) ∈ 𝑃) |
| 128 | 29 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝑋 ∈ 𝑃) |
| 129 | 31 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → 𝐴 ∈ 𝑃) |
| 130 | 3, 4, 5, 125, 126, 127, 128, 129 | axtgsegcon 28472 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ∃𝑡 ∈ 𝑃 ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) |
| 131 | 123, 55, 124, 130 | syl21anc 838 |
. . . . . 6
⊢
((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → ∃𝑡 ∈ 𝑃 ((𝑀‘𝑌) ∈ (𝑦𝐼𝑡) ∧ ((𝑀‘𝑌) − 𝑡) = (𝑋 − 𝐴))) |
| 132 | 122, 131 | r19.29a 3162 |
. . . . 5
⊢
((((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) ∧ 𝑧 ∈ 𝑃) ∧ ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌)) |
| 133 | 3, 4, 5, 25, 27, 39, 35, 32 | axtgsegcon 28472 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ∃𝑧 ∈ 𝑃 ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) |
| 134 | 133 | ad2antrr 726 |
. . . . 5
⊢
((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ∃𝑧 ∈ 𝑃 ((𝑀‘𝑋) ∈ (𝑥𝐼𝑧) ∧ ((𝑀‘𝑋) − 𝑧) = (𝑌 − 𝐴))) |
| 135 | 132, 134 | r19.29a 3162 |
. . . 4
⊢
((((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌)) |
| 136 | 3, 4, 5, 24, 41, 34, 29, 31 | axtgsegcon 28472 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ∃𝑦 ∈ 𝑃 (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) |
| 137 | 136 | ad2antrr 726 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ∃𝑦 ∈ 𝑃 (𝑌 ∈ ((𝑀‘𝑌)𝐼𝑦) ∧ (𝑌 − 𝑦) = (𝑋 − 𝐴))) |
| 138 | 135, 137 | r19.29a 3162 |
. . 3
⊢ ((((𝜑 ∧ 𝑋 ≠ 𝐴) ∧ 𝑥 ∈ 𝑃) ∧ (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌)) |
| 139 | 3, 4, 5, 24, 38, 29, 34, 31 | axtgsegcon 28472 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ∃𝑥 ∈ 𝑃 (𝑋 ∈ ((𝑀‘𝑋)𝐼𝑥) ∧ (𝑋 − 𝑥) = (𝑌 − 𝐴))) |
| 140 | 138, 139 | r19.29a 3162 |
. 2
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐴) → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌)) |
| 141 | 23, 140 | pm2.61dane 3029 |
1
⊢ (𝜑 → ((𝑀‘𝑋) − (𝑀‘𝑌)) = (𝑋 − 𝑌)) |