Description: Line mirroring is an involution. Theorem 10.5 of Schwabhauser p. 89. (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 | lmilmi | ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) |
| 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 9 | lmicl | ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑃 ) |
| 11 | eqidd | ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ 𝐴 ) ) | |
| 12 | 1 2 3 4 5 6 7 8 9 10 11 | lmicom | ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) |