Metamath Proof Explorer

Theorem lmif

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

Ref Expression
Hypotheses ismid.p ⊢P=BaseG
ismid.d ⊢-˙=dist⁡G
ismid.i ⊢I=Itv⁡G
ismid.g ⊢φ→G∈𝒢Tarski
ismid.1 ⊢φ→GDim𝒢≥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=BaseG
2 ismid.d ⊢-˙=dist⁡G
3 ismid.i ⊢I=Itv⁡G
4 ismid.g ⊢φ→G∈𝒢Tarski
5 ismid.1 ⊢φ→GDim𝒢≥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∈Baseg⟼ιb∈Baseg|amid𝒢⁡gb∈d∧d⟂𝒢⁡gaLine𝒢⁡gb∨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→Baseg=BaseG
14 13 1 eqtr4di ⊢g=G→Baseg=P
15 fveq2 ⊢g=G→mid𝒢⁡g=mid𝒢⁡G
16 15 oveqd ⊢g=G→amid𝒢⁡gb=amid𝒢⁡Gb
17 16 eleq1d ⊢g=G→amid𝒢⁡gb∈d↔amid𝒢⁡Gb∈d
18 eqidd ⊢g=G→d=d
19 fveq2 ⊢g=G→⟂𝒢⁡g=⟂𝒢⁡G
20 11 oveqd ⊢g=G→aLine𝒢⁡gb=aLb
21 18 19 20 breq123d ⊢g=G→d⟂𝒢⁡gaLine𝒢⁡gb↔d⟂𝒢⁡GaLb
22 21 orbi1d ⊢g=G→d⟂𝒢⁡gaLine𝒢⁡gb∨a=b↔d⟂𝒢⁡GaLb∨a=b
23 17 22 anbi12d ⊢g=G→amid𝒢⁡gb∈d∧d⟂𝒢⁡gaLine𝒢⁡gb∨a=b↔amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b
24 14 23 riotaeqbidv ⊢g=G→ιb∈Baseg|amid𝒢⁡gb∈d∧d⟂𝒢⁡gaLine𝒢⁡gb∨a=b=ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b
25 14 24 mpteq12dv ⊢g=G→a∈Baseg⟼ιb∈Baseg|amid𝒢⁡gb∈d∧d⟂𝒢⁡gaLine𝒢⁡gb∨a=b=a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b
26 12 25 mpteq12dv ⊢g=G→d∈ran⁡Line𝒢⁡g⟼a∈Baseg⟼ιb∈Baseg|amid𝒢⁡gb∈d∧d⟂𝒢⁡gaLine𝒢⁡gb∨a=b=d∈ran⁡L⟼a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨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|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b∈V
31 28 29 30 mp2b ⊢d∈ran⁡L⟼a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b∈V
32 31 a1i ⊢φ→d∈ran⁡L⟼a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b∈V
33 9 26 27 32 fvmptd3 ⊢φ→lInv𝒢⁡G=d∈ran⁡L⟼a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b
34 eleq2 ⊢d=D→amid𝒢⁡Gb∈d↔amid𝒢⁡Gb∈D
35 breq1 ⊢d=D→d⟂𝒢⁡GaLb↔D⟂𝒢⁡GaLb
36 35 orbi1d ⊢d=D→d⟂𝒢⁡GaLb∨a=b↔D⟂𝒢⁡GaLb∨a=b
37 34 36 anbi12d ⊢d=D→amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b↔amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
38 37 riotabidv ⊢d=D→ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b=ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
39 38 mpteq2dv ⊢d=D→a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b=a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
40 39 adantl ⊢φ∧d=D→a∈P⟼ιb∈P|amid𝒢⁡Gb∈d∧d⟂𝒢⁡GaLb∨a=b=a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
41 1 fvexi ⊢P∈V
42 41 mptex ⊢a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b∈V
43 42 a1i ⊢φ→a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b∈V
44 33 40 8 43 fvmptd ⊢φ→lInv𝒢⁡G⁡D=a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
45 6 44 eqtrid ⊢φ→M=a∈P⟼ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
46 4 adantr ⊢φ∧a∈P→G∈𝒢Tarski
47 5 adantr ⊢φ∧a∈P→GDim𝒢≥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∈Pamid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b
51 riotacl ⊢∃!b∈Pamid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b→ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b∈P
52 50 51 syl ⊢φ∧a∈P→ιb∈P|amid𝒢⁡Gb∈D∧D⟂𝒢⁡GaLb∨a=b∈P
53 45 52 fmpt3d ⊢φ→M:P⟶P