Metamath Proof Explorer

Definition df-lmi

Description: Define the line mirroring function. Definition 10.3 of Schwabhauser p. 89. See islmib . (Contributed by Thierry Arnoux, 1-Dec-2019)

Ref Expression
Assertion 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 ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmi 
 |-  lInvG
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vm 
 |-  m
4 clng 
 |-  LineG
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( LineG ` g )
7 6 crn 
 |-  ran ( LineG ` g )
8 va 
 |-  a
9 cbs 
 |-  Base
10 5 9 cfv 
 |-  ( Base ` g )
11 vb 
 |-  b
12 8 cv 
 |-  a
13 cmid 
 |-  midG
14 5 13 cfv 
 |-  ( midG ` g )
15 11 cv 
 |-  b
16 12 15 14 co 
 |-  ( a ( midG ` g ) b )
17 3 cv 
 |-  m
18 16 17 wcel 
 |-  ( a ( midG ` g ) b ) e. m
19 cperpg 
 |-  perpG
20 5 19 cfv 
 |-  ( perpG ` g )
21 12 15 6 co 
 |-  ( a ( LineG ` g ) b )
22 17 21 20 wbr 
 |-  m ( perpG ` g ) ( a ( LineG ` g ) b )
23 12 15 wceq 
 |-  a = b
24 22 23 wo 
 |-  ( m ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b )
25 18 24 wa 
 |-  ( ( a ( midG ` g ) b ) e. m /\ ( m ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) )
26 25 11 10 crio 
 |-  ( iota_ b e. ( Base ` g ) ( ( a ( midG ` g ) b ) e. m /\ ( m ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) )
27 8 10 26 cmpt 
 |-  ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a ( midG ` g ) b ) e. m /\ ( m ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) ) )
28 3 7 27 cmpt 
 |-  ( m e. ran ( LineG ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a ( midG ` g ) b ) e. m /\ ( m ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) ) ) )
29 1 2 28 cmpt 
 |-  ( g e. _V |-> ( m e. ran ( LineG ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a ( midG ` g ) b ) e. m /\ ( m ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) ) ) ) )
30 0 29 wceq 
 |-  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 ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) ) ) ) )