Metamath Proof Explorer

Theorem lmif

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

Ref Expression
Hypotheses ismid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ismid.d ⊢ − = ( dist ‘ 𝐺 )
ismid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ismid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
ismid.1 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
lmif.m ⊢ 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
lmif.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
lmif.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
Assertion lmif ( 𝜑 → 𝑀 : 𝑃 ⟶ 𝑃 )

Proof

Step Hyp Ref Expression
1 ismid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ismid.d ⊢ − = ( dist ‘ 𝐺 )
3 ismid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 ismid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 ismid.1 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
6 lmif.m ⊢ 𝑀 = ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 )
7 lmif.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
8 lmif.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
9 df-lmi ⊢ lInvG = ( 𝑔 ∈ V ↦ ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) )
10 fveq2 ⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) )
11 10 7 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = 𝐿 )
12 11 rneqd ⊢ ( 𝑔 = 𝐺 → ran ( LineG ‘ 𝑔 ) = ran 𝐿 )
13 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
14 13 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
15 fveq2 ⊢ ( 𝑔 = 𝐺 → ( midG ‘ 𝑔 ) = ( midG ‘ 𝐺 ) )
16 15 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) = ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) )
17 16 eleq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ↔ ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ) )
18 eqidd ⊢ ( 𝑔 = 𝐺 → 𝑑 = 𝑑 )
19 fveq2 ⊢ ( 𝑔 = 𝐺 → ( ⟂G ‘ 𝑔 ) = ( ⟂G ‘ 𝐺 ) )
20 11 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) = ( 𝑎 𝐿 𝑏 ) )
21 18 19 20 breq123d ⊢ ( 𝑔 = 𝐺 → ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ↔ 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ) )
22 21 orbi1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) )
23 17 22 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ↔ ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) )
24 14 23 riotaeqbidv ⊢ ( 𝑔 = 𝐺 → ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) = ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) )
25 14 24 mpteq12dv ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) )
26 12 25 mpteq12dv ⊢ ( 𝑔 = 𝐺 → ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) = ( 𝑑 ∈ ran 𝐿 ↦ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) )
27 4 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
28 7 fvexi ⊢ 𝐿 ∈ V
29 rnexg ⊢ ( 𝐿 ∈ V → ran 𝐿 ∈ V )
30 mptexg ⊢ ( ran 𝐿 ∈ V → ( 𝑑 ∈ ran 𝐿 ↦ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) ∈ V )
31 28 29 30 mp2b ⊢ ( 𝑑 ∈ ran 𝐿 ↦ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) ∈ V
32 31 a1i ⊢ ( 𝜑 → ( 𝑑 ∈ ran 𝐿 ↦ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) ∈ V )
33 9 26 27 32 fvmptd3 ⊢ ( 𝜑 → ( lInvG ‘ 𝐺 ) = ( 𝑑 ∈ ran 𝐿 ↦ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) )
34 eleq2 ⊢ ( 𝑑 = 𝐷 → ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ↔ ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ) )
35 breq1 ⊢ ( 𝑑 = 𝐷 → ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ↔ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ) )
36 35 orbi1d ⊢ ( 𝑑 = 𝐷 → ( ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ↔ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) )
37 34 36 anbi12d ⊢ ( 𝑑 = 𝐷 → ( ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ↔ ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) )
38 37 riotabidv ⊢ ( 𝑑 = 𝐷 → ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) = ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) )
39 38 mpteq2dv ⊢ ( 𝑑 = 𝐷 → ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑑 = 𝐷 ) → ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝑑 ∧ ( 𝑑 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) )
41 1 fvexi ⊢ 𝑃 ∈ V
42 41 mptex ⊢ ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ∈ V
43 42 a1i ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ∈ V )
44 33 40 8 43 fvmptd ⊢ ( 𝜑 → ( ( lInvG ‘ 𝐺 ) ‘ 𝐷 ) = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) )
45 6 44 syl5eq ⊢ ( 𝜑 → 𝑀 = ( 𝑎 ∈ 𝑃 ↦ ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) )
46 4 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → 𝐺 ∈ TarskiG )
47 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → 𝐺 DimTarskiG≥ 2 )
48 8 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → 𝐷 ∈ ran 𝐿 )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → 𝑎 ∈ 𝑃 )
50 1 2 3 46 47 7 48 49 lmieu ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → ∃! 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) )
51 riotacl ⊢ ( ∃! 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) → ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ∈ 𝑃 )
52 50 51 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → ( ℩ 𝑏 ∈ 𝑃 ( ( 𝑎 ( midG ‘ 𝐺 ) 𝑏 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝑎 𝐿 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ∈ 𝑃 )
53 45 52 fmpt3d ⊢ ( 𝜑 → 𝑀 : 𝑃 ⟶ 𝑃 )