Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mirbtwn | Structured version Visualization version GIF version |
Description: Property of the image by the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 3-Jun-2019.) |
Ref | Expression |
---|---|
mirval.p | ⊢ 𝑃 = (Base‘𝐺) |
mirval.d | ⊢ − = (dist‘𝐺) |
mirval.i | ⊢ 𝐼 = (Itv‘𝐺) |
mirval.l | ⊢ 𝐿 = (LineG‘𝐺) |
mirval.s | ⊢ 𝑆 = (pInvG‘𝐺) |
mirval.g | ⊢ (𝜑 → 𝐺 ∈ TarskiG) |
mirval.a | ⊢ (𝜑 → 𝐴 ∈ 𝑃) |
mirfv.m | ⊢ 𝑀 = (𝑆‘𝐴) |
mirfv.b | ⊢ (𝜑 → 𝐵 ∈ 𝑃) |
Ref | Expression |
---|---|
mirbtwn | ⊢ (𝜑 → 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mirval.p | . . . . 5 ⊢ 𝑃 = (Base‘𝐺) | |
2 | mirval.d | . . . . 5 ⊢ − = (dist‘𝐺) | |
3 | mirval.i | . . . . 5 ⊢ 𝐼 = (Itv‘𝐺) | |
4 | mirval.l | . . . . 5 ⊢ 𝐿 = (LineG‘𝐺) | |
5 | mirval.s | . . . . 5 ⊢ 𝑆 = (pInvG‘𝐺) | |
6 | mirval.g | . . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG) | |
7 | mirval.a | . . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃) | |
8 | mirfv.m | . . . . 5 ⊢ 𝑀 = (𝑆‘𝐴) | |
9 | mirfv.b | . . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃) | |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | mirfv 26370 | . . . 4 ⊢ (𝜑 → (𝑀‘𝐵) = (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵)))) |
11 | 1, 2, 3, 6, 9, 7 | mirreu3 26368 | . . . . 5 ⊢ (𝜑 → ∃!𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))) |
12 | riotacl2 7119 | . . . . 5 ⊢ (∃!𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵)) → (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))) ∈ {𝑧 ∈ 𝑃 ∣ ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))}) | |
13 | 11, 12 | syl 17 | . . . 4 ⊢ (𝜑 → (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))) ∈ {𝑧 ∈ 𝑃 ∣ ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))}) |
14 | 10, 13 | eqeltrd 2913 | . . 3 ⊢ (𝜑 → (𝑀‘𝐵) ∈ {𝑧 ∈ 𝑃 ∣ ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))}) |
15 | oveq2 7153 | . . . . . 6 ⊢ (𝑧 = (𝑀‘𝐵) → (𝐴 − 𝑧) = (𝐴 − (𝑀‘𝐵))) | |
16 | 15 | eqeq1d 2823 | . . . . 5 ⊢ (𝑧 = (𝑀‘𝐵) → ((𝐴 − 𝑧) = (𝐴 − 𝐵) ↔ (𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵))) |
17 | oveq1 7152 | . . . . . 6 ⊢ (𝑧 = (𝑀‘𝐵) → (𝑧𝐼𝐵) = ((𝑀‘𝐵)𝐼𝐵)) | |
18 | 17 | eleq2d 2898 | . . . . 5 ⊢ (𝑧 = (𝑀‘𝐵) → (𝐴 ∈ (𝑧𝐼𝐵) ↔ 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵))) |
19 | 16, 18 | anbi12d 630 | . . . 4 ⊢ (𝑧 = (𝑀‘𝐵) → (((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵)) ↔ ((𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵) ∧ 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵)))) |
20 | 19 | elrab 3679 | . . 3 ⊢ ((𝑀‘𝐵) ∈ {𝑧 ∈ 𝑃 ∣ ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))} ↔ ((𝑀‘𝐵) ∈ 𝑃 ∧ ((𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵) ∧ 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵)))) |
21 | 14, 20 | sylib 219 | . 2 ⊢ (𝜑 → ((𝑀‘𝐵) ∈ 𝑃 ∧ ((𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵) ∧ 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵)))) |
22 | 21 | simprrd 770 | 1 ⊢ (𝜑 → 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ wcel 2105 ∃!wreu 3140 {crab 3142 ‘cfv 6349 ℩crio 7102 (class class class)co 7145 Basecbs 16473 distcds 16564 TarskiGcstrkg 26144 Itvcitv 26150 LineGclng 26151 pInvGcmir 26366 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3497 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-iun 4914 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-riota 7103 df-ov 7148 df-trkgc 26162 df-trkgb 26163 df-trkgcb 26164 df-trkg 26167 df-mir 26367 |
This theorem is referenced by: mirmir 26376 mirinv 26380 miriso 26384 mirmir2 26388 mirln 26390 mirln2 26391 mirconn 26392 mirhl2 26395 mircgrextend 26396 mirtrcgr 26397 mirauto 26398 miduniq 26399 krippenlem 26404 ragflat 26418 ragcgr 26421 footexALT 26432 footexlem1 26433 footexlem2 26434 colperpexlem1 26444 colperpexlem3 26446 mideulem2 26448 opphllem 26449 opphllem1 26461 opphllem2 26462 opphllem4 26464 colhp 26484 midbtwn 26493 lmieu 26498 lmiisolem 26510 |
Copyright terms: Public domain | W3C validator |