Definition df-mir 27893

Description: Define the point inversion ("mirror") function. Definition 7.5 of [Schwabhauser] p. 49. See mirval 27895 and ismir 27899. (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

Step	Hyp	Ref	Expression
1		cmir 27892	. 2 class pInvG
2		vg	. . 3 setvar 𝑔
3		cvv 3474	. . 3 class V
4		vm	. . . 4 setvar 𝑚
5	2	cv 1540	. . . . 5 class 𝑔
6		cbs 17140	. . . . 5 class Base
7	5, 6	cfv 6540	. . . 4 class (Base‘𝑔)
8		va	. . . . 5 setvar 𝑎
9	4	cv 1540	. . . . . . . . 9 class 𝑚
10		vb	. . . . . . . . . 10 setvar 𝑏
11	10	cv 1540	. . . . . . . . 9 class 𝑏
12		cds 17202	. . . . . . . . . 10 class dist
13	5, 12	cfv 6540	. . . . . . . . 9 class (dist‘𝑔)
14	9, 11, 13	co 7405	. . . . . . . 8 class (𝑚(dist‘𝑔)𝑏)
15	8	cv 1540	. . . . . . . . 9 class 𝑎
16	9, 15, 13	co 7405	. . . . . . . 8 class (𝑚(dist‘𝑔)𝑎)
17	14, 16	wceq 1541	. . . . . . 7 wff (𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎)
18		citv 27673	. . . . . . . . . 10 class Itv
19	5, 18	cfv 6540	. . . . . . . . 9 class (Itv‘𝑔)
20	11, 15, 19	co 7405	. . . . . . . 8 class (𝑏(Itv‘𝑔)𝑎)
21	9, 20	wcel 2106	. . . . . . 7 wff 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)
22	17, 21	wa 396	. . . . . 6 wff ((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))
23	22, 10, 7	crio 7360	. . . . 5 class (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)))
24	8, 7, 23	cmpt 5230	. . . 4 class (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))
25	4, 7, 24	cmpt 5230	. . 3 class (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎)))))
26	2, 3, 25	cmpt 5230	. 2 class (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))))
27	1, 26	wceq 1541	1 wff pInvG = (𝑔 ∈ V ↦ (𝑚 ∈ (Base‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑚(dist‘𝑔)𝑏) = (𝑚(dist‘𝑔)𝑎) ∧ 𝑚 ∈ (𝑏(Itv‘𝑔)𝑎))))))

This definition is referenced by:  mirval  27895