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 eqtrid ⊢ φ → 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