Proof of Theorem mirconn
| Step | Hyp | Ref
| Expression |
| 1 | | mirval.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
| 2 | | mirval.d |
. . 3
⊢ − =
(dist‘𝐺) |
| 3 | | mirval.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
| 4 | | mirval.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 5 | 4 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴𝐼𝑌)) → 𝐺 ∈ TarskiG) |
| 6 | | mirconn.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
| 7 | 6 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴𝐼𝑌)) → 𝑋 ∈ 𝑃) |
| 8 | | mirconn.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 9 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴𝐼𝑌)) → 𝐴 ∈ 𝑃) |
| 10 | | mirval.l |
. . . . 5
⊢ 𝐿 = (LineG‘𝐺) |
| 11 | | mirval.s |
. . . . 5
⊢ 𝑆 = (pInvG‘𝐺) |
| 12 | | mirconn.m |
. . . . 5
⊢ 𝑀 = (𝑆‘𝐴) |
| 13 | | mirconn.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
| 14 | 1, 2, 3, 10, 11, 4, 8, 12, 13 | mircl 28669 |
. . . 4
⊢ (𝜑 → (𝑀‘𝑌) ∈ 𝑃) |
| 15 | 14 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴𝐼𝑌)) → (𝑀‘𝑌) ∈ 𝑃) |
| 16 | 13 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴𝐼𝑌)) → 𝑌 ∈ 𝑃) |
| 17 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴𝐼𝑌)) → 𝑋 ∈ (𝐴𝐼𝑌)) |
| 18 | 1, 2, 3, 10, 11, 4, 8, 12, 13 | mirbtwn 28666 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ((𝑀‘𝑌)𝐼𝑌)) |
| 19 | 18 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴𝐼𝑌)) → 𝐴 ∈ ((𝑀‘𝑌)𝐼𝑌)) |
| 20 | 1, 2, 3, 5, 7, 9, 15, 16, 17, 19 | tgbtwnintr 28501 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴𝐼𝑌)) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) |
| 21 | 1, 2, 3, 4, 6, 8 | tgbtwntriv2 28495 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝐴)) |
| 22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝐴) → 𝐴 ∈ (𝑋𝐼𝐴)) |
| 23 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = 𝐴) → 𝑌 = 𝐴) |
| 24 | 23 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝐴) → (𝑀‘𝑌) = (𝑀‘𝐴)) |
| 25 | 1, 2, 3, 10, 11, 4, 8, 12 | mircinv 28676 |
. . . . . . . 8
⊢ (𝜑 → (𝑀‘𝐴) = 𝐴) |
| 26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = 𝐴) → (𝑀‘𝐴) = 𝐴) |
| 27 | 24, 26 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = 𝐴) → (𝑀‘𝑌) = 𝐴) |
| 28 | 27 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = 𝐴) → (𝑋𝐼(𝑀‘𝑌)) = (𝑋𝐼𝐴)) |
| 29 | 22, 28 | eleqtrrd 2844 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝐴) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) |
| 30 | 29 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 = 𝐴) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) |
| 31 | 4 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 ≠ 𝐴) → 𝐺 ∈ TarskiG) |
| 32 | 6 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 ≠ 𝐴) → 𝑋 ∈ 𝑃) |
| 33 | 13 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 ≠ 𝐴) → 𝑌 ∈ 𝑃) |
| 34 | 8 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 ≠ 𝐴) → 𝐴 ∈ 𝑃) |
| 35 | 14 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 ≠ 𝐴) → (𝑀‘𝑌) ∈ 𝑃) |
| 36 | | simpr 484 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 ≠ 𝐴) → 𝑌 ≠ 𝐴) |
| 37 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 ≠ 𝐴) → 𝑌 ∈ (𝐴𝐼𝑋)) |
| 38 | 1, 2, 3, 31, 34, 33, 32, 37 | tgbtwncom 28496 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 ≠ 𝐴) → 𝑌 ∈ (𝑋𝐼𝐴)) |
| 39 | 1, 2, 3, 4, 14, 8,
13, 18 | tgbtwncom 28496 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (𝑌𝐼(𝑀‘𝑌))) |
| 40 | 39 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 ≠ 𝐴) → 𝐴 ∈ (𝑌𝐼(𝑀‘𝑌))) |
| 41 | 1, 2, 3, 31, 32, 33, 34, 35, 36, 38, 40 | tgbtwnouttr2 28503 |
. . 3
⊢ (((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) ∧ 𝑌 ≠ 𝐴) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) |
| 42 | 30, 41 | pm2.61dane 3029 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ (𝐴𝐼𝑋)) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) |
| 43 | | mirconn.1 |
. 2
⊢ (𝜑 → (𝑋 ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼𝑋))) |
| 44 | 20, 42, 43 | mpjaodan 961 |
1
⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑌))) |