MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mir Structured version   Unicode version

Definition df-mir 23184
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
StepHypRef Expression
1 cmir 23183 . 2  class pInvG
2 vg . . 3  setvar  g
3 cvv 3070 . . 3  class  _V
4 vm . . . 4  setvar  m
52cv 1369 . . . . 5  class  g
6 cbs 14278 . . . . 5  class  Base
75, 6cfv 5518 . . . 4  class  ( Base `  g )
8 va . . . . 5  setvar  a
94cv 1369 . . . . . . . . 9  class  m
10 vb . . . . . . . . . 10  setvar  b
1110cv 1369 . . . . . . . . 9  class  b
12 cds 14351 . . . . . . . . . 10  class  dist
135, 12cfv 5518 . . . . . . . . 9  class  ( dist `  g )
149, 11, 13co 6192 . . . . . . . 8  class  ( m ( dist `  g
) b )
158cv 1369 . . . . . . . . 9  class  a
169, 15, 13co 6192 . . . . . . . 8  class  ( m ( dist `  g
) a )
1714, 16wceq 1370 . . . . . . 7  wff  ( m ( dist `  g
) b )  =  ( m ( dist `  g ) a )
18 citv 23014 . . . . . . . . . 10  class Itv
195, 18cfv 5518 . . . . . . . . 9  class  (Itv `  g )
2011, 15, 19co 6192 . . . . . . . 8  class  ( b (Itv `  g )
a )
219, 20wcel 1758 . . . . . . 7  wff  m  e.  ( b (Itv `  g ) a )
2217, 21wa 369 . . . . . 6  wff  ( ( m ( dist `  g
) b )  =  ( m ( dist `  g ) a )  /\  m  e.  ( b (Itv `  g
) a ) )
2322, 10, 7crio 6152 . . . . 5  class  ( iota_ b  e.  ( Base `  g
) ( ( m ( dist `  g
) b )  =  ( m ( dist `  g ) a )  /\  m  e.  ( b (Itv `  g
) a ) ) )
248, 7, 23cmpt 4450 . . . 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 ) ) ) )
254, 7, 24cmpt 4450 . . 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 ) ) ) ) )
262, 3, 25cmpt 4450 . 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 ) ) ) ) ) )
271, 26wceq 1370 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 ) ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  mirval  23187
  Copyright terms: Public domain W3C validator