Definition df-mir 24012

Description: Define the point inversion function. Definition 7.5 of [Schwabhauser] p. 49. (Contributed by Thierry Arnoux, 30-May-2019.)

Assertion

Ref	Expression
df-mir	|- pInvG = ( g e. _V |-> ( m e. ( Base ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b (Itv ` g ) a ) ) ) ) ) )

Distinct variable group:   a, b, g, m

Detailed syntax breakdown of Definition df-mir

Step	Hyp	Ref	Expression
1		cmir 24011	. 2 class pInvG
2		vg	. . 3 setvar g
3		cvv 3095	. . 3 class _V
4		vm	. . . 4 setvar m
5	2	cv 1382	. . . . 5 class g
6		cbs 14614	. . . . 5 class Base
7	5, 6	cfv 5578	. . . 4 class ( Base ` g )
8		va	. . . . 5 setvar a
9	4	cv 1382	. . . . . . . . 9 class m
10		vb	. . . . . . . . . 10 setvar b
11	10	cv 1382	. . . . . . . . 9 class b
12		cds 14688	. . . . . . . . . 10 class dist
13	5, 12	cfv 5578	. . . . . . . . 9 class ( dist ` g )
14	9, 11, 13	co 6281	. . . . . . . 8 class ( m ( dist ` g ) b )
15	8	cv 1382	. . . . . . . . 9 class a
16	9, 15, 13	co 6281	. . . . . . . 8 class ( m ( dist ` g ) a )
17	14, 16	wceq 1383	. . . . . . 7 wff ( m ( dist ` g ) b ) = ( m ( dist ` g ) a )
18		citv 23810	. . . . . . . . . 10 class Itv
19	5, 18	cfv 5578	. . . . . . . . 9 class (Itv ` g )
20	11, 15, 19	co 6281	. . . . . . . 8 class ( b (Itv ` g ) a )
21	9, 20	wcel 1804	. . . . . . 7 wff m e. ( b (Itv ` g ) a )
22	17, 21	wa 369	. . . . . 6 wff ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b (Itv ` g ) a ) )
23	22, 10, 7	crio 6241	. . . . 5 class ( iota_ b e. ( Base ` g ) ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b (Itv ` g ) a ) ) )
24	8, 7, 23	cmpt 4495	. . . 4 class ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b (Itv ` g ) a ) ) ) )
25	4, 7, 24	cmpt 4495	. . 3 class ( m e. ( Base ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b (Itv ` g ) a ) ) ) ) )
26	2, 3, 25	cmpt 4495	. 2 class ( g e. _V |-> ( m e. ( Base ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b (Itv ` g ) a ) ) ) ) ) )
27	1, 26	wceq 1383	1 wff pInvG = ( g e. _V |-> ( m e. ( Base ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b (Itv ` g ) a ) ) ) ) ) )

This definition is referenced by:  mirval  24014