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

Definition df-lmi 24345
Description: Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 1-Dec-2019.)
Assertion
Ref Expression
df-lmi  |- lInvG  =  ( g  e.  _V  |->  ( m  e.  ran  (LineG `  g )  |->  ( a  e.  ( Base `  g
)  |->  ( iota_ b  e.  ( Base `  g
) ( ( a (midG `  g )
b )  e.  m  /\  ( m (⟂G `  g
) ( a (LineG `  g ) b )  \/  a  =  b ) ) ) ) ) )
Distinct variable group:    a, b, g, m

Detailed syntax breakdown of Definition df-lmi
StepHypRef Expression
1 clmi 24343 . 2  class lInvG
2 vg . . 3  setvar  g
3 cvv 3106 . . 3  class  _V
4 vm . . . 4  setvar  m
52cv 1397 . . . . . 6  class  g
6 clng 24034 . . . . . 6  class LineG
75, 6cfv 5570 . . . . 5  class  (LineG `  g )
87crn 4989 . . . 4  class  ran  (LineG `  g )
9 va . . . . 5  setvar  a
10 cbs 14719 . . . . . 6  class  Base
115, 10cfv 5570 . . . . 5  class  ( Base `  g )
129cv 1397 . . . . . . . . 9  class  a
13 vb . . . . . . . . . 10  setvar  b
1413cv 1397 . . . . . . . . 9  class  b
15 cmid 24342 . . . . . . . . . 10  class midG
165, 15cfv 5570 . . . . . . . . 9  class  (midG `  g )
1712, 14, 16co 6270 . . . . . . . 8  class  ( a (midG `  g )
b )
184cv 1397 . . . . . . . 8  class  m
1917, 18wcel 1823 . . . . . . 7  wff  ( a (midG `  g )
b )  e.  m
2012, 14, 7co 6270 . . . . . . . . 9  class  ( a (LineG `  g )
b )
21 cperpg 24276 . . . . . . . . . 10  class ⟂G
225, 21cfv 5570 . . . . . . . . 9  class  (⟂G `  g
)
2318, 20, 22wbr 4439 . . . . . . . 8  wff  m (⟂G `  g ) ( a (LineG `  g )
b )
249, 13weq 1738 . . . . . . . 8  wff  a  =  b
2523, 24wo 366 . . . . . . 7  wff  ( m (⟂G `  g )
( a (LineG `  g ) b )  \/  a  =  b )
2619, 25wa 367 . . . . . 6  wff  ( ( a (midG `  g
) b )  e.  m  /\  ( m (⟂G `  g )
( a (LineG `  g ) b )  \/  a  =  b ) )
2726, 13, 11crio 6231 . . . . 5  class  ( iota_ b  e.  ( Base `  g
) ( ( a (midG `  g )
b )  e.  m  /\  ( m (⟂G `  g
) ( a (LineG `  g ) b )  \/  a  =  b ) ) )
289, 11, 27cmpt 4497 . . . 4  class  ( a  e.  ( Base `  g
)  |->  ( iota_ b  e.  ( Base `  g
) ( ( a (midG `  g )
b )  e.  m  /\  ( m (⟂G `  g
) ( a (LineG `  g ) b )  \/  a  =  b ) ) ) )
294, 8, 28cmpt 4497 . . 3  class  ( m  e.  ran  (LineG `  g )  |->  ( a  e.  ( Base `  g
)  |->  ( iota_ b  e.  ( Base `  g
) ( ( a (midG `  g )
b )  e.  m  /\  ( m (⟂G `  g
) ( a (LineG `  g ) b )  \/  a  =  b ) ) ) ) )
302, 3, 29cmpt 4497 . 2  class  ( g  e.  _V  |->  ( m  e.  ran  (LineG `  g )  |->  ( a  e.  ( Base `  g
)  |->  ( iota_ b  e.  ( Base `  g
) ( ( a (midG `  g )
b )  e.  m  /\  ( m (⟂G `  g
) ( a (LineG `  g ) b )  \/  a  =  b ) ) ) ) ) )
311, 30wceq 1398 1  wff lInvG  =  ( g  e.  _V  |->  ( m  e.  ran  (LineG `  g )  |->  ( a  e.  ( Base `  g
)  |->  ( iota_ b  e.  ( Base `  g
) ( ( a (midG `  g )
b )  e.  m  /\  ( m (⟂G `  g
) ( a (LineG `  g ) b )  \/  a  =  b ) ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  lmif  24355  islmib  24357
  Copyright terms: Public domain W3C validator