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 φ G 𝒢 Tarski
ismid.1 φ G Dim 𝒢 2
lmif.m M = lInv 𝒢 G D
lmif.l L = Line 𝒢 G
lmif.d φ D ran L
Assertion lmif φ 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 φ G 𝒢 Tarski
5 ismid.1 φ G Dim 𝒢 2
6 lmif.m M = lInv 𝒢 G D
7 lmif.l L = Line 𝒢 G
8 lmif.d φ D ran L
9 df-lmi lInv 𝒢 = g V d ran Line 𝒢 g a Base g ι b Base g | a mid 𝒢 g b d d 𝒢 g a Line 𝒢 g b a = b
10 fveq2 g = G Line 𝒢 g = Line 𝒢 G
11 10 7 eqtr4di g = G Line 𝒢 g = L
12 11 rneqd g = G ran Line 𝒢 g = ran L
13 fveq2 g = G Base g = Base G
14 13 1 eqtr4di g = G Base g = P
15 fveq2 g = G mid 𝒢 g = mid 𝒢 G
16 15 oveqd g = G a mid 𝒢 g b = a mid 𝒢 G b
17 16 eleq1d g = G a mid 𝒢 g b d a mid 𝒢 G b d
18 eqidd g = G d = d
19 fveq2 g = G 𝒢 g = 𝒢 G
20 11 oveqd g = G a Line 𝒢 g b = a L b
21 18 19 20 breq123d g = G d 𝒢 g a Line 𝒢 g b d 𝒢 G a L b
22 21 orbi1d g = G d 𝒢 g a Line 𝒢 g b a = b d 𝒢 G a L b a = b
23 17 22 anbi12d g = G a mid 𝒢 g b d d 𝒢 g a Line 𝒢 g b a = b a mid 𝒢 G b d d 𝒢 G a L b a = b
24 14 23 riotaeqbidv g = G ι b Base g | a mid 𝒢 g b d d 𝒢 g a Line 𝒢 g b a = b = ι b P | a mid 𝒢 G b d d 𝒢 G a L b a = b
25 14 24 mpteq12dv g = G a Base g ι b Base g | a mid 𝒢 g b d d 𝒢 g a Line 𝒢 g b a = b = a P ι b P | a mid 𝒢 G b d d 𝒢 G a L b a = b
26 12 25 mpteq12dv g = G d ran Line 𝒢 g a Base g ι b Base g | a mid 𝒢 g b d d 𝒢 g a Line 𝒢 g b a = b = d ran L a P ι b P | a mid 𝒢 G b d d 𝒢 G a L b a = b
27 4 elexd φ G V
28 7 fvexi L V
29 rnexg L V ran L V
30 mptexg ran L V d ran L a P ι b P | a mid 𝒢 G b d d 𝒢 G a L b a = b V
31 28 29 30 mp2b d ran L a P ι b P | a mid 𝒢 G b d d 𝒢 G a L b a = b V
32 31 a1i φ d ran L a P ι b P | a mid 𝒢 G b d d 𝒢 G a L b a = b V
33 9 26 27 32 fvmptd3 φ lInv 𝒢 G = d ran L a P ι b P | a mid 𝒢 G b d d 𝒢 G a L b a = b
34 eleq2 d = D a mid 𝒢 G b d a mid 𝒢 G b D
35 breq1 d = D d 𝒢 G a L b D 𝒢 G a L b
36 35 orbi1d d = D d 𝒢 G a L b a = b D 𝒢 G a L b a = b
37 34 36 anbi12d d = D a mid 𝒢 G b d d 𝒢 G a L b a = b a mid 𝒢 G b D D 𝒢 G a L b a = b
38 37 riotabidv d = D ι b P | a mid 𝒢 G b d d 𝒢 G a L b a = b = ι b P | a mid 𝒢 G b D D 𝒢 G a L b a = b
39 38 mpteq2dv d = D a P ι b P | a mid 𝒢 G b d d 𝒢 G a L b a = b = a P ι b P | a mid 𝒢 G b D D 𝒢 G a L b a = b
40 39 adantl φ d = D a P ι b P | a mid 𝒢 G b d d 𝒢 G a L b a = b = a P ι b P | a mid 𝒢 G b D D 𝒢 G a L b a = b
41 1 fvexi P V
42 41 mptex a P ι b P | a mid 𝒢 G b D D 𝒢 G a L b a = b V
43 42 a1i φ a P ι b P | a mid 𝒢 G b D D 𝒢 G a L b a = b V
44 33 40 8 43 fvmptd φ lInv 𝒢 G D = a P ι b P | a mid 𝒢 G b D D 𝒢 G a L b a = b
45 6 44 syl5eq φ M = a P ι b P | a mid 𝒢 G b D D 𝒢 G a L b a = b
46 4 adantr φ a P G 𝒢 Tarski
47 5 adantr φ a P G Dim 𝒢 2
48 8 adantr φ a P D ran L
49 simpr φ a P a P
50 1 2 3 46 47 7 48 49 lmieu φ a P ∃! b P a mid 𝒢 G b D D 𝒢 G a L b a = b
51 riotacl ∃! b P a mid 𝒢 G b D D 𝒢 G a L b a = b ι b P | a mid 𝒢 G b D D 𝒢 G a L b a = b P
52 50 51 syl φ a P ι b P | a mid 𝒢 G b D D 𝒢 G a L b a = b P
53 45 52 fmpt3d φ M : P P