Metamath Proof Explorer

Theorem lmicom

Description: The line mirroring function is an involution. Theorem 10.4 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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
islmib.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
lmicom.1 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = 𝐵 )
Assertion lmicom ( 𝜑 → ( 𝑀 ‘ 𝐵 ) = 𝐴 )

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 islmib.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
11 lmicom.1 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = 𝐵 )
12 1 2 3 4 5 9 10 midcom ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) = ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) )
13 11 eqcomd ⊢ ( 𝜑 → 𝐵 = ( 𝑀 ‘ 𝐴 ) )
14 1 2 3 4 5 6 7 8 9 10 islmib ⊢ ( 𝜑 → ( 𝐵 = ( 𝑀 ‘ 𝐴 ) ↔ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ) )
15 13 14 mpbid ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) )
16 15 simpld ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝐷 )
17 12 16 eqeltrrd ⊢ ( 𝜑 → ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) ∈ 𝐷 )
18 15 simprd ⊢ ( 𝜑 → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
19 18 orcomd ⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) )
20 19 ord ⊢ ( 𝜑 → ( ¬ 𝐴 = 𝐵 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) )
21 4 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐺 ∈ TarskiG )
22 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝑃 )
23 10 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝑃 )
24 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐴 = 𝐵 )
25 24 neqned ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ≠ 𝐵 )
26 1 3 7 21 22 23 25 tglinecom ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐵 𝐿 𝐴 ) )
27 26 breq2d ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ↔ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ) )
28 27 pm5.74da ⊢ ( 𝜑 → ( ( ¬ 𝐴 = 𝐵 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ↔ ( ¬ 𝐴 = 𝐵 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ) ) )
29 20 28 mpbid ⊢ ( 𝜑 → ( ¬ 𝐴 = 𝐵 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ) )
30 29 orrd ⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ) )
31 30 orcomd ⊢ ( 𝜑 → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∨ 𝐴 = 𝐵 ) )
32 eqcom ⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
33 32 orbi2i ⊢ ( ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∨ 𝐴 = 𝐵 ) ↔ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
34 31 33 sylib ⊢ ( 𝜑 → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
35 1 2 3 4 5 6 7 8 10 9 islmib ⊢ ( 𝜑 → ( 𝐴 = ( 𝑀 ‘ 𝐵 ) ↔ ( ( 𝐵 ( midG ‘ 𝐺 ) 𝐴 ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ) ) )
36 17 34 35 mpbir2and ⊢ ( 𝜑 → 𝐴 = ( 𝑀 ‘ 𝐵 ) )
37 36 eqcomd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) = 𝐴 )