MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mir Structured version   Visualization version   GIF version

Definition df-mir 26367
Description: Define the point inversion ("mirror") function. Definition 7.5 of [Schwabhauser] p. 49. See mirval 26369 and ismir 26373. (Contributed by Thierry Arnoux, 30-May-2019.)
Assertion
Ref Expression
df-mir pInvG = (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))))
Distinct variable group:   𝑎,𝑏,𝑔,𝑚

Detailed syntax breakdown of Definition df-mir
StepHypRef Expression
1 cmir 26366 . 2 class pInvG
2 vg . . 3 setvar 𝑔
3 cvv 3495 . . 3 class V
4 vm . . . 4 setvar 𝑚
52cv 1527 . . . . 5 class 𝑔
6 cbs 16473 . . . . 5 class Base
75, 6cfv 6349 . . . 4 class (Base‘𝑔)
8 va . . . . 5 setvar 𝑎
94cv 1527 . . . . . . . . 9 class 𝑚
10 vb . . . . . . . . . 10 setvar 𝑏
1110cv 1527 . . . . . . . . 9 class 𝑏
12 cds 16564 . . . . . . . . . 10 class dist
135, 12cfv 6349 . . . . . . . . 9 class (dist‘𝑔)
149, 11, 13co 7145 . . . . . . . 8 class (𝑚(dist‘𝑔)𝑏)
158cv 1527 . . . . . . . . 9 class 𝑎
169, 15, 13co 7145 . . . . . . . 8 class (𝑚(dist‘𝑔)𝑎)
1714, 16wceq 1528 . . . . . . 7 wff (𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎)
18 citv 26150 . . . . . . . . . 10 class Itv
195, 18cfv 6349 . . . . . . . . 9 class (Itv‘𝑔)
2011, 15, 19co 7145 . . . . . . . 8 class (𝑏(Itv‘𝑔)𝑎)
219, 20wcel 2105 . . . . . . 7 wff 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)
2217, 21wa 396 . . . . . 6 wff ((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))
2322, 10, 7crio 7102 . . . . 5 class (𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)))
248, 7, 23cmpt 5138 . . . 4 class (𝑎 ∈ (Base‘𝑔) ↦ (𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))
254, 7, 24cmpt 5138 . . 3 class (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)))))
262, 3, 25cmpt 5138 . 2 class (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))))
271, 26wceq 1528 1 wff pInvG = (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))))
Colors of variables: wff setvar class
This definition is referenced by:  mirval  26369
  Copyright terms: Public domain W3C validator