![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mircgr | 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 |
---|---|
mircgr | ⊢ (𝜑 → (𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mirval.p | . . . . . 6 ⊢ 𝑃 = (Base‘𝐺) | |
2 | mirval.d | . . . . . 6 ⊢ − = (dist‘𝐺) | |
3 | mirval.i | . . . . . 6 ⊢ 𝐼 = (Itv‘𝐺) | |
4 | mirval.l | . . . . . 6 ⊢ 𝐿 = (LineG‘𝐺) | |
5 | mirval.s | . . . . . 6 ⊢ 𝑆 = (pInvG‘𝐺) | |
6 | mirval.g | . . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG) | |
7 | mirval.a | . . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑃) | |
8 | mirfv.m | . . . . . 6 ⊢ 𝑀 = (𝑆‘𝐴) | |
9 | mirfv.b | . . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃) | |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | mirfv 25907 | . . . . 5 ⊢ (𝜑 → (𝑀‘𝐵) = (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵)))) |
11 | 1, 2, 3, 6, 9, 7 | mirreu3 25905 | . . . . . 6 ⊢ (𝜑 → ∃!𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))) |
12 | riotacl2 6852 | . . . . . 6 ⊢ (∃!𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵)) → (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))) ∈ {𝑧 ∈ 𝑃 ∣ ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))}) | |
13 | 11, 12 | syl 17 | . . . . 5 ⊢ (𝜑 → (℩𝑧 ∈ 𝑃 ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))) ∈ {𝑧 ∈ 𝑃 ∣ ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))}) |
14 | 10, 13 | eqeltrd 2878 | . . . 4 ⊢ (𝜑 → (𝑀‘𝐵) ∈ {𝑧 ∈ 𝑃 ∣ ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))}) |
15 | oveq2 6886 | . . . . . . 7 ⊢ (𝑧 = (𝑀‘𝐵) → (𝐴 − 𝑧) = (𝐴 − (𝑀‘𝐵))) | |
16 | 15 | eqeq1d 2801 | . . . . . 6 ⊢ (𝑧 = (𝑀‘𝐵) → ((𝐴 − 𝑧) = (𝐴 − 𝐵) ↔ (𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵))) |
17 | oveq1 6885 | . . . . . . 7 ⊢ (𝑧 = (𝑀‘𝐵) → (𝑧𝐼𝐵) = ((𝑀‘𝐵)𝐼𝐵)) | |
18 | 17 | eleq2d 2864 | . . . . . 6 ⊢ (𝑧 = (𝑀‘𝐵) → (𝐴 ∈ (𝑧𝐼𝐵) ↔ 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵))) |
19 | 16, 18 | anbi12d 625 | . . . . 5 ⊢ (𝑧 = (𝑀‘𝐵) → (((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵)) ↔ ((𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵) ∧ 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵)))) |
20 | 19 | elrab 3556 | . . . 4 ⊢ ((𝑀‘𝐵) ∈ {𝑧 ∈ 𝑃 ∣ ((𝐴 − 𝑧) = (𝐴 − 𝐵) ∧ 𝐴 ∈ (𝑧𝐼𝐵))} ↔ ((𝑀‘𝐵) ∈ 𝑃 ∧ ((𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵) ∧ 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵)))) |
21 | 14, 20 | sylib 210 | . . 3 ⊢ (𝜑 → ((𝑀‘𝐵) ∈ 𝑃 ∧ ((𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵) ∧ 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵)))) |
22 | 21 | simprd 490 | . 2 ⊢ (𝜑 → ((𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵) ∧ 𝐴 ∈ ((𝑀‘𝐵)𝐼𝐵))) |
23 | 22 | simpld 489 | 1 ⊢ (𝜑 → (𝐴 − (𝑀‘𝐵)) = (𝐴 − 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ∃!wreu 3091 {crab 3093 ‘cfv 6101 ℩crio 6838 (class class class)co 6878 Basecbs 16184 distcds 16276 TarskiGcstrkg 25681 Itvcitv 25687 LineGclng 25688 pInvGcmir 25903 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pr 5097 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-ral 3094 df-rex 3095 df-reu 3096 df-rmo 3097 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-iun 4712 df-br 4844 df-opab 4906 df-mpt 4923 df-id 5220 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-riota 6839 df-ov 6881 df-trkgc 25699 df-trkgb 25700 df-trkgcb 25701 df-trkg 25704 df-mir 25904 |
This theorem is referenced by: mirmir 25913 miriso 25921 mirmir2 25925 mircgrextend 25933 mirtrcgr 25934 mirauto 25935 miduniq 25936 krippenlem 25941 ragcol 25950 ragflat 25955 ragcgr 25958 footex 25969 colperpexlem1 25978 colperpexlem3 25980 mideulem2 25982 opphllem 25983 midcgr 26028 lmiisolem 26044 sacgr 26078 |
Copyright terms: Public domain | W3C validator |