Metamath Proof Explorer

Theorem lmicl

Description: Closure of the line mirror. (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 𝐿 )
lmicl.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
Assertion lmicl ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 )

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 lmicl.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10 1 2 3 4 5 6 7 8 lmif ⊢ ( 𝜑 → 𝑀 : 𝑃 ⟶ 𝑃 )
11 10 9 ffvelrnd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 )