Definition df-mir

Description: Define the point inversion ("mirror") function. Definition 7.5 of Schwabhauser p. 49. See mirval and ismir . (Contributed by Thierry Arnoux, 30-May-2019)

	Ref	Expression
Assertion	df-mir	$$⊢{pInv}_{𝒢}=\left(g\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_g⟼\left(a\in {\mathrm{Base}}_g⟼\left(\iota b\in {\mathrm{Base}}_g|\left(m\mathrm{dist}\left(g\right)b=m\mathrm{dist}\left(g\right)a\wedge m\in \left(b\mathrm{Itv}\left(g\right)a\right)\right)\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmir	$$class{pInv}_{𝒢}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		vm	$$setvarm$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarg$$
6	5 4	cfv	$$class{\mathrm{Base}}_g$$
7		va	$$setvara$$
8		vb	$$setvarb$$
9	3	cv	$$setvarm$$
10		cds	$$class\mathrm{dist}$$
11	5 10	cfv	$$class\mathrm{dist}\left(g\right)$$
12	8	cv	$$setvarb$$
13	9 12 11	co	$$class\left(m\mathrm{dist}\left(g\right)b\right)$$
14	7	cv	$$setvara$$
15	9 14 11	co	$$class\left(m\mathrm{dist}\left(g\right)a\right)$$
16	13 15	wceq	$$wffm\mathrm{dist}\left(g\right)b=m\mathrm{dist}\left(g\right)a$$
17		citv	$$class\mathrm{Itv}$$
18	5 17	cfv	$$class\mathrm{Itv}\left(g\right)$$
19	12 14 18	co	$$class\left(b\mathrm{Itv}\left(g\right)a\right)$$
20	9 19	wcel	$$wffm\in \left(b\mathrm{Itv}\left(g\right)a\right)$$
21	16 20	wa	$$wff\left(m\mathrm{dist}\left(g\right)b=m\mathrm{dist}\left(g\right)a\wedge m\in \left(b\mathrm{Itv}\left(g\right)a\right)\right)$$
22	21 8 6	crio	$$class\left(\iota b\in {\mathrm{Base}}_g|\left(m\mathrm{dist}\left(g\right)b=m\mathrm{dist}\left(g\right)a\wedge m\in \left(b\mathrm{Itv}\left(g\right)a\right)\right)\right)$$
23	7 6 22	cmpt	$$class\left(a\in {\mathrm{Base}}_g⟼\left(\iota b\in {\mathrm{Base}}_g|\left(m\mathrm{dist}\left(g\right)b=m\mathrm{dist}\left(g\right)a\wedge m\in \left(b\mathrm{Itv}\left(g\right)a\right)\right)\right)\right)$$
24	3 6 23	cmpt	$$class\left(m\in {\mathrm{Base}}_g⟼\left(a\in {\mathrm{Base}}_g⟼\left(\iota b\in {\mathrm{Base}}_g|\left(m\mathrm{dist}\left(g\right)b=m\mathrm{dist}\left(g\right)a\wedge m\in \left(b\mathrm{Itv}\left(g\right)a\right)\right)\right)\right)\right)$$
25	1 2 24	cmpt	$$class\left(g\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_g⟼\left(a\in {\mathrm{Base}}_g⟼\left(\iota b\in {\mathrm{Base}}_g|\left(m\mathrm{dist}\left(g\right)b=m\mathrm{dist}\left(g\right)a\wedge m\in \left(b\mathrm{Itv}\left(g\right)a\right)\right)\right)\right)\right)\right)$$
26	0 25	wceq	$$wff{pInv}_{𝒢}=\left(g\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_g⟼\left(a\in {\mathrm{Base}}_g⟼\left(\iota b\in {\mathrm{Base}}_g|\left(m\mathrm{dist}\left(g\right)b=m\mathrm{dist}\left(g\right)a\wedge m\in \left(b\mathrm{Itv}\left(g\right)a\right)\right)\right)\right)\right)\right)$$