Metamath Proof Explorer

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 
|- 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 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmir 
 |-  pInvG
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vm 
 |-  m
4 cbs 
 |-  Base
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( Base ` g )
7 va 
 |-  a
8 vb 
 |-  b
9 3 cv 
 |-  m
10 cds 
 |-  dist
11 5 10 cfv 
 |-  ( dist ` g )
12 8 cv 
 |-  b
13 9 12 11 co 
 |-  ( m ( dist ` g ) b )
14 7 cv 
 |-  a
15 9 14 11 co 
 |-  ( m ( dist ` g ) a )
16 13 15 wceq 
 |-  ( m ( dist ` g ) b ) = ( m ( dist ` g ) a )
17 citv 
 |-  Itv
18 5 17 cfv 
 |-  ( Itv ` g )
19 12 14 18 co 
 |-  ( b ( Itv ` g ) a )
20 9 19 wcel 
 |-  m e. ( b ( Itv ` g ) a )
21 16 20 wa 
 |-  ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b ( Itv ` g ) a ) )
22 21 8 6 crio 
 |-  ( iota_ b e. ( Base ` g ) ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b ( Itv ` g ) a ) ) )
23 7 6 22 cmpt 
 |-  ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( m ( dist ` g ) b ) = ( m ( dist ` g ) a ) /\ m e. ( b ( Itv ` g ) a ) ) ) )
24 3 6 23 cmpt 
 |-  ( 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 ) ) ) ) )
25 1 2 24 cmpt 
 |-  ( 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 ) ) ) ) ) )
26 0 25 wceq 
 |-  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 ) ) ) ) ) )