Metamath Proof Explorer

Theorem islmib

Description: Property of the line mirror. (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 )
lmicl.1 
|- ( ph -> A e. P )
islmib.b 
|- ( ph -> B e. P )
Assertion islmib 
|- ( ph -> ( B = ( M ` A ) <-> ( ( A ( midG ` G ) B ) e. D /\ ( D ( perpG ` G ) ( A L B ) \/ A = B ) ) ) )

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 lmicl.1 
 |-  ( ph -> A e. P )
10 islmib.b 
 |-  ( ph -> B e. P )
11 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 ) ) ) ) ) )
12 fveq2 
 |-  ( g = G -> ( LineG ` g ) = ( LineG ` G ) )
13 12 7 eqtr4di 
 |-  ( g = G -> ( LineG ` g ) = L )
14 13 rneqd 
 |-  ( g = G -> ran ( LineG ` g ) = ran L )
15 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
16 15 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
17 fveq2 
 |-  ( g = G -> ( midG ` g ) = ( midG ` G ) )
18 17 oveqd 
 |-  ( g = G -> ( a ( midG ` g ) b ) = ( a ( midG ` G ) b ) )
19 18 eleq1d 
 |-  ( g = G -> ( ( a ( midG ` g ) b ) e. d <-> ( a ( midG ` G ) b ) e. d ) )
20 eqidd 
 |-  ( g = G -> d = d )
21 fveq2 
 |-  ( g = G -> ( perpG ` g ) = ( perpG ` G ) )
22 13 oveqd 
 |-  ( g = G -> ( a ( LineG ` g ) b ) = ( a L b ) )
23 20 21 22 breq123d 
 |-  ( g = G -> ( d ( perpG ` g ) ( a ( LineG ` g ) b ) <-> d ( perpG ` G ) ( a L b ) ) )
24 23 orbi1d 
 |-  ( g = G -> ( ( d ( perpG ` g ) ( a ( LineG ` g ) b ) \/ a = b ) <-> ( d ( perpG ` G ) ( a L b ) \/ a = b ) ) )
25 19 24 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 ) ) ) )
26 16 25 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 ) ) ) )
27 16 26 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 ) ) ) ) )
28 14 27 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 ) ) ) ) ) )
29 4 elexd 
 |-  ( ph -> G e. _V )
30 7 fvexi 
 |-  L e. _V
31 rnexg 
 |-  ( L e. _V -> ran L e. _V )
32 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 )
33 30 31 32 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
34 33 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 )
35 11 28 29 34 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 ) ) ) ) ) )
36 eleq2 
 |-  ( d = D -> ( ( a ( midG ` G ) b ) e. d <-> ( a ( midG ` G ) b ) e. D ) )
37 breq1 
 |-  ( d = D -> ( d ( perpG ` G ) ( a L b ) <-> D ( perpG ` G ) ( a L b ) ) )
38 37 orbi1d 
 |-  ( d = D -> ( ( d ( perpG ` G ) ( a L b ) \/ a = b ) <-> ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) )
39 36 38 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 ) ) ) )
40 39 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 ) ) ) )
41 40 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 ) ) ) ) )
42 41 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 ) ) ) ) )
43 1 fvexi 
 |-  P e. _V
44 43 mptex 
 |-  ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) e. _V
45 44 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 )
46 35 42 8 45 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 ) ) ) ) )
47 6 46 eqtrid 
 |-  ( ph -> M = ( a e. P |-> ( iota_ b e. P ( ( a ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( a L b ) \/ a = b ) ) ) ) )
48 oveq1 
 |-  ( a = A -> ( a ( midG ` G ) b ) = ( A ( midG ` G ) b ) )
49 48 eleq1d 
 |-  ( a = A -> ( ( a ( midG ` G ) b ) e. D <-> ( A ( midG ` G ) b ) e. D ) )
50 oveq1 
 |-  ( a = A -> ( a L b ) = ( A L b ) )
51 50 breq2d 
 |-  ( a = A -> ( D ( perpG ` G ) ( a L b ) <-> D ( perpG ` G ) ( A L b ) ) )
52 eqeq1 
 |-  ( a = A -> ( a = b <-> A = b ) )
53 51 52 orbi12d 
 |-  ( a = A -> ( ( D ( perpG ` G ) ( a L b ) \/ a = b ) <-> ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )
54 49 53 anbi12d 
 |-  ( a = A -> ( ( ( 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 ) ) ) )
55 54 riotabidv 
 |-  ( a = A -> ( 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 ) ) ) )
56 55 adantl 
 |-  ( ( ph /\ a = A ) -> ( 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 ) ) ) )
57 1 2 3 4 5 7 8 9 lmieu 
 |-  ( ph -> E! b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )
58 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 )
59 57 58 syl 
 |-  ( ph -> ( iota_ b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) e. P )
60 47 56 9 59 fvmptd 
 |-  ( ph -> ( M ` A ) = ( iota_ b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) )
61 60 eqeq2d 
 |-  ( ph -> ( B = ( M ` A ) <-> B = ( iota_ b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) ) )
62 oveq2 
 |-  ( b = B -> ( A ( midG ` G ) b ) = ( A ( midG ` G ) B ) )
63 62 eleq1d 
 |-  ( b = B -> ( ( A ( midG ` G ) b ) e. D <-> ( A ( midG ` G ) B ) e. D ) )
64 oveq2 
 |-  ( b = B -> ( A L b ) = ( A L B ) )
65 64 breq2d 
 |-  ( b = B -> ( D ( perpG ` G ) ( A L b ) <-> D ( perpG ` G ) ( A L B ) ) )
66 eqeq2 
 |-  ( b = B -> ( A = b <-> A = B ) )
67 65 66 orbi12d 
 |-  ( b = B -> ( ( D ( perpG ` G ) ( A L b ) \/ A = b ) <-> ( D ( perpG ` G ) ( A L B ) \/ A = B ) ) )
68 63 67 anbi12d 
 |-  ( b = B -> ( ( ( 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 ) ) ) )
69 68 riota2 
 |-  ( ( B e. P /\ E! b e. P ( ( 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 ) ) <-> ( iota_ b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) = B ) )
70 10 57 69 syl2anc 
 |-  ( ph -> ( ( ( 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 ) ) ) = B ) )
71 eqcom 
 |-  ( B = ( 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 ) ) ) = B )
72 70 71 bitr4di 
 |-  ( ph -> ( ( ( A ( midG ` G ) B ) e. D /\ ( D ( perpG ` G ) ( A L B ) \/ A = B ) ) <-> B = ( iota_ b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) ) )
73 61 72 bitr4d 
 |-  ( ph -> ( B = ( M ` A ) <-> ( ( A ( midG ` G ) B ) e. D /\ ( D ( perpG ` G ) ( A L B ) \/ A = B ) ) ) )