Metamath Proof Explorer

Theorem lmif

Description: Line mirror as a function. (Contributed by Thierry Arnoux, 11-Dec-2019)

Ref Expression
Hypotheses ismid.p 
|- P = ( Base ` G )
ismid.d 
|- .- = ( dist ` G )
ismid.i 
|- I = ( Itv ` G )
ismid.g 
|- ( ph -> G e. TarskiG )
ismid.1 
|- ( ph -> G TarskiGDim>= 2 )
lmif.m 
|- M = ( ( lInvG ` G ) ` D )
lmif.l 
|- L = ( LineG ` G )
lmif.d 
|- ( ph -> D e. ran L )
Assertion lmif 
|- ( ph -> M : P --> P )

Proof

Step Hyp Ref Expression
1 ismid.p 
 |-  P = ( Base ` G )
2 ismid.d 
 |-  .- = ( dist ` G )
3 ismid.i 
 |-  I = ( Itv ` G )
4 ismid.g 
 |-  ( ph -> G e. TarskiG )
5 ismid.1 
 |-  ( ph -> G TarskiGDim>= 2 )
6 lmif.m 
 |-  M = ( ( lInvG ` G ) ` D )
7 lmif.l 
 |-  L = ( LineG ` G )
8 lmif.d 
 |-  ( ph -> D e. ran L )
9 df-lmi 
 |-  lInvG = ( g e. _V |-> ( d e. ran ( LineG ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a ( midG ` g ) b ) e. d /\ ( d ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) ) ) ) )
10 fveq2 
 |-  ( g = G -> ( LineG ` g ) = ( LineG ` G ) )
11 10 7 eqtr4di 
 |-  ( g = G -> ( LineG ` g ) = L )
12 11 rneqd 
 |-  ( g = G -> ran ( LineG ` g ) = ran L )
13 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
14 13 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
15 fveq2 
 |-  ( g = G -> ( midG ` g ) = ( midG ` G ) )
16 15 oveqd 
 |-  ( g = G -> ( a ( midG ` g ) b ) = ( a ( midG ` G ) b ) )
17 16 eleq1d 
 |-  ( g = G -> ( ( a ( midG ` g ) b ) e. d <-> ( a ( midG ` G ) b ) e. d ) )
18 eqidd 
 |-  ( g = G -> d = d )
19 fveq2 
 |-  ( g = G -> ( perpG ` g ) = ( perpG ` G ) )
20 11 oveqd 
 |-  ( g = G -> ( a ( LineG ` g ) b ) = ( a L b ) )
21 18 19 20 breq123d 
 |-  ( g = G -> ( d ( perpG ` g ) ( a ( LineG ` g ) b ) <-> d ( perpG ` G ) ( a L b ) ) )
22 21 orbi1d 
 |-  ( g = G -> ( ( d ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) <-> ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) )
23 17 22 anbi12d 
 |-  ( g = G -> ( ( ( a ( midG ` g ) b ) e. d /\ ( d ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) <-> ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) )
24 14 23 riotaeqbidv 
 |-  ( g = G -> ( iota_ b e. ( Base ` g ) ( ( a ( midG ` g ) b ) e. d /\ ( d ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) ) = ( iota_ b e. P ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) )
25 14 24 mpteq12dv 
 |-  ( g = G -> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a ( midG ` g ) b ) e. d /\ ( d ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) ) ) = ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) )
26 12 25 mpteq12dv 
 |-  ( g = G -> ( d e. ran ( LineG ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a ( midG ` g ) b ) e. d /\ ( d ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) ) ) ) ) = ( d e. ran L |-> ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) ) )
27 4 elexd 
 |-  ( ph -> G e. _V )
28 7 fvexi 
 |-  L e. _V
29 rnexg 
 |-  ( L e. _V -> ran L e. _V )
30 mptexg 
 |-  ( ran L e. _V -> ( d e. ran L |-> ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) ) e. _V )
31 28 29 30 mp2b 
 |-  ( d e. ran L |-> ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) ) e. _V
32 31 a1i 
 |-  ( ph -> ( d e. ran L |-> ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) ) e. _V )
33 9 26 27 32 fvmptd3 
 |-  ( ph -> ( lInvG ` G ) = ( d e. ran L |-> ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) ) )
34 eleq2 
 |-  ( d = D -> ( ( a ( midG ` G ) b ) e. d <-> ( a ( midG ` G ) b ) e. D ) )
35 breq1 
 |-  ( d = D -> ( d ( perpG ` G ) ( a L b ) <-> D ( perpG ` G ) ( a L b ) ) )
36 35 orbi1d 
 |-  ( d = D -> ( ( d ( perpG ` G ) ( a L b ) \/ a = b ) <-> ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) )
37 34 36 anbi12d 
 |-  ( d = D -> ( ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) <-> ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) )
38 37 riotabidv 
 |-  ( d = D -> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) = ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) )
39 38 mpteq2dv 
 |-  ( d = D -> ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) = ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) )
40 39 adantl 
 |-  ( ( ph /\ d = D ) -> ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. d /\ ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) = ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) )
41 1 fvexi 
 |-  P e. _V
42 41 mptex 
 |-  ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) e. _V
43 42 a1i 
 |-  ( ph -> ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) e. _V )
44 33 40 8 43 fvmptd 
 |-  ( ph -> ( ( lInvG ` G ) ` D ) = ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) )
45 6 44 syl5eq 
 |-  ( ph -> M = ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) )
46 4 adantr 
 |-  ( ( ph /\ a e. P ) -> G e. TarskiG )
47 5 adantr 
 |-  ( ( ph /\ a e. P ) -> G TarskiGDim>= 2 )
48 8 adantr 
 |-  ( ( ph /\ a e. P ) -> D e. ran L )
49 simpr 
 |-  ( ( ph /\ a e. P ) -> a e. P )
50 1 2 3 46 47 7 48 49 lmieu 
 |-  ( ( ph /\ a e. P ) -> E! b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) )
51 riotacl 
 |-  ( E! b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) -> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) e. P )
52 50 51 syl 
 |-  ( ( ph /\ a e. P ) -> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) e. P )
53 45 52 fmpt3d 
 |-  ( ph -> M : P --> P )