Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mircl | Structured version Visualization version GIF version |
Description: Closure of the point inversion function. (Contributed by Thierry Arnoux, 20-Oct-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 | ⊢ 𝑀 = (𝑆‘𝐴) |
mircl.x | ⊢ (𝜑 → 𝑋 ∈ 𝑃) |
Ref | Expression |
---|---|
mircl | ⊢ (𝜑 → (𝑀‘𝑋) ∈ 𝑃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mirval.p | . . 3 ⊢ 𝑃 = (Base‘𝐺) | |
2 | mirval.d | . . 3 ⊢ − = (dist‘𝐺) | |
3 | mirval.i | . . 3 ⊢ 𝐼 = (Itv‘𝐺) | |
4 | mirval.l | . . 3 ⊢ 𝐿 = (LineG‘𝐺) | |
5 | mirval.s | . . 3 ⊢ 𝑆 = (pInvG‘𝐺) | |
6 | mirval.g | . . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiG) | |
7 | mirval.a | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃) | |
8 | mirfv.m | . . 3 ⊢ 𝑀 = (𝑆‘𝐴) | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mirf 27049 | . 2 ⊢ (𝜑 → 𝑀:𝑃⟶𝑃) |
10 | mircl.x | . 2 ⊢ (𝜑 → 𝑋 ∈ 𝑃) | |
11 | 9, 10 | ffvelcdmd 6982 | 1 ⊢ (𝜑 → (𝑀‘𝑋) ∈ 𝑃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2101 ‘cfv 6447 Basecbs 16940 distcds 16999 TarskiGcstrkg 26816 Itvcitv 26822 LineGclng 26823 pInvGcmir 27041 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 ax-rep 5212 ax-sep 5226 ax-nul 5233 ax-pr 5355 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2063 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ne 2939 df-ral 3060 df-rex 3069 df-rmo 3222 df-reu 3223 df-rab 3224 df-v 3436 df-sbc 3719 df-csb 3835 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4260 df-if 4463 df-pw 4538 df-sn 4565 df-pr 4567 df-op 4571 df-uni 4842 df-iun 4929 df-br 5078 df-opab 5140 df-mpt 5161 df-id 5491 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-rn 5602 df-res 5603 df-ima 5604 df-iota 6399 df-fun 6449 df-fn 6450 df-f 6451 df-f1 6452 df-fo 6453 df-f1o 6454 df-fv 6455 df-riota 7252 df-ov 7298 df-trkgc 26837 df-trkgb 26838 df-trkgcb 26839 df-trkg 26842 df-mir 27042 |
This theorem is referenced by: mirmir 27051 mirreu 27053 mireq 27054 miriso 27059 mirmir2 27063 mirln 27065 mirconn 27067 mirhl 27068 mirbtwnhl 27069 mirhl2 27070 mircgrextend 27071 mirtrcgr 27072 miduniq 27074 miduniq1 27075 miduniq2 27076 ragcom 27087 ragcol 27088 ragmir 27089 mirrag 27090 ragflat2 27092 ragflat 27093 ragcgr 27096 footexALT 27107 footexlem1 27108 footexlem2 27109 footex 27110 colperpexlem1 27119 colperpexlem3 27121 mideulem2 27123 opphllem 27124 opphllem2 27137 opphllem3 27138 opphllem4 27139 opphllem6 27141 opphl 27143 colhp 27159 mirmid 27172 lmieu 27173 lmimid 27183 lmiisolem 27185 hypcgrlem1 27188 hypcgrlem2 27189 hypcgr 27190 sacgr 27220 |
Copyright terms: Public domain | W3C validator |