Definition df-mir 23740

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 23739	. 2 class pInvG
2		vg	. . 3 setvar g
3		cvv 3106	. . 3 class _V
4		vm	. . . 4 setvar m
5	2	cv 1373	. . . . 5 class g
6		cbs 14479	. . . . 5 class Base
7	5, 6	cfv 5579	. . . 4 class ( Base ` g )
8		va	. . . . 5 setvar a
9	4	cv 1373	. . . . . . . . 9 class m
10		vb	. . . . . . . . . 10 setvar b
11	10	cv 1373	. . . . . . . . 9 class b
12		cds 14553	. . . . . . . . . 10 class dist
13	5, 12	cfv 5579	. . . . . . . . 9 class ( dist ` g )
14	9, 11, 13	co 6275	. . . . . . . 8 class ( m ( dist ` g ) b )
15	8	cv 1373	. . . . . . . . 9 class a
16	9, 15, 13	co 6275	. . . . . . . 8 class ( m ( dist ` g ) a )
17	14, 16	wceq 1374	. . . . . . 7 wff ( m ( dist ` g ) b ) = ( m ( dist ` g ) a )
18		citv 23553	. . . . . . . . . 10 class Itv
19	5, 18	cfv 5579	. . . . . . . . 9 class (Itv ` g )
20	11, 15, 19	co 6275	. . . . . . . 8 class ( b (Itv ` g ) a )
21	9, 20	wcel 1762	. . . . . . 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 6235	. . . . 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 4498	. . . 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 4498	. . 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 4498	. 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 1374	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  23742