Metamath Proof Explorer

Theorem lmimid

Description: If we have a right angle, then the mirror point is the point inversion. (Contributed by Thierry Arnoux, 15-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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
lmimid.s ⊢ 𝑆 = ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 )
lmimid.r ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
lmimid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
lmimid.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
lmimid.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
lmimid.d ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion lmimid ( 𝜑 → ( 𝑀 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 ) )

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 lmimid.s ⊢ 𝑆 = ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 )
11 lmimid.r ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
12 lmimid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
13 lmimid.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
14 lmimid.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
15 lmimid.d ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
16 10 a1i ⊢ ( 𝜑 → 𝑆 = ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) )
17 16 fveq1d ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐶 ) )
18 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
19 1 7 3 4 8 13 tglnpt ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
20 1 2 3 7 18 4 19 10 14 mircl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐶 ) ∈ 𝑃 )
21 1 2 3 4 5 14 20 18 19 ismidb ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐵 ) ‘ 𝐶 ) ↔ ( 𝐶 ( midG ‘ 𝐺 ) ( 𝑆 ‘ 𝐶 ) ) = 𝐵 ) )
22 17 21 mpbid ⊢ ( 𝜑 → ( 𝐶 ( midG ‘ 𝐺 ) ( 𝑆 ‘ 𝐶 ) ) = 𝐵 )
23 22 13 eqeltrd ⊢ ( 𝜑 → ( 𝐶 ( midG ‘ 𝐺 ) ( 𝑆 ‘ 𝐶 ) ) ∈ 𝐷 )
24 df-ne ⊢ ( 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ↔ ¬ 𝐶 = ( 𝑆 ‘ 𝐶 ) )
25 4 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐺 ∈ TarskiG )
26 8 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐷 ∈ ran 𝐿 )
27 14 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐶 ∈ 𝑃 )
28 20 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → ( 𝑆 ‘ 𝐶 ) ∈ 𝑃 )
29 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) )
30 1 3 7 25 27 28 29 tgelrnln ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → ( 𝐶 𝐿 ( 𝑆 ‘ 𝐶 ) ) ∈ ran 𝐿 )
31 13 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐵 ∈ 𝐷 )
32 19 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐵 ∈ 𝑃 )
33 1 2 3 4 5 14 20 midbtwn ⊢ ( 𝜑 → ( 𝐶 ( midG ‘ 𝐺 ) ( 𝑆 ‘ 𝐶 ) ) ∈ ( 𝐶 𝐼 ( 𝑆 ‘ 𝐶 ) ) )
34 22 33 eqeltrrd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐶 𝐼 ( 𝑆 ‘ 𝐶 ) ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐵 ∈ ( 𝐶 𝐼 ( 𝑆 ‘ 𝐶 ) ) )
36 1 3 7 25 27 28 32 29 35 btwnlng1 ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐵 ∈ ( 𝐶 𝐿 ( 𝑆 ‘ 𝐶 ) ) )
37 31 36 elind ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐵 ∈ ( 𝐷 ∩ ( 𝐶 𝐿 ( 𝑆 ‘ 𝐶 ) ) ) )
38 12 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐴 ∈ 𝐷 )
39 1 3 7 25 27 28 29 tglinerflx1 ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐶 ∈ ( 𝐶 𝐿 ( 𝑆 ‘ 𝐶 ) ) )
40 15 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐴 ≠ 𝐵 )
41 1 2 3 7 18 4 19 10 14 mirinv ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐶 ) = 𝐶 ↔ 𝐵 = 𝐶 ) )
42 eqcom ⊢ ( 𝐵 = 𝐶 ↔ 𝐶 = 𝐵 )
43 41 42 bitrdi ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐶 ) = 𝐶 ↔ 𝐶 = 𝐵 ) )
44 43 biimpar ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐵 ) → ( 𝑆 ‘ 𝐶 ) = 𝐶 )
45 44 eqcomd ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐵 ) → 𝐶 = ( 𝑆 ‘ 𝐶 ) )
46 45 ex ⊢ ( 𝜑 → ( 𝐶 = 𝐵 → 𝐶 = ( 𝑆 ‘ 𝐶 ) ) )
47 46 necon3d ⊢ ( 𝜑 → ( 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) → 𝐶 ≠ 𝐵 ) )
48 47 imp ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐶 ≠ 𝐵 )
49 11 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
50 1 2 3 7 25 26 30 37 38 39 40 48 49 ragperp ⊢ ( ( 𝜑 ∧ 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 ( 𝑆 ‘ 𝐶 ) ) )
51 50 ex ⊢ ( 𝜑 → ( 𝐶 ≠ ( 𝑆 ‘ 𝐶 ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 ( 𝑆 ‘ 𝐶 ) ) ) )
52 24 51 syl5bir ⊢ ( 𝜑 → ( ¬ 𝐶 = ( 𝑆 ‘ 𝐶 ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 ( 𝑆 ‘ 𝐶 ) ) ) )
53 52 orrd ⊢ ( 𝜑 → ( 𝐶 = ( 𝑆 ‘ 𝐶 ) ∨ 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 ( 𝑆 ‘ 𝐶 ) ) ) )
54 53 orcomd ⊢ ( 𝜑 → ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 ( 𝑆 ‘ 𝐶 ) ) ∨ 𝐶 = ( 𝑆 ‘ 𝐶 ) ) )
55 1 2 3 4 5 6 7 8 14 20 islmib ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐶 ) = ( 𝑀 ‘ 𝐶 ) ↔ ( ( 𝐶 ( midG ‘ 𝐺 ) ( 𝑆 ‘ 𝐶 ) ) ∈ 𝐷 ∧ ( 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 ( 𝑆 ‘ 𝐶 ) ) ∨ 𝐶 = ( 𝑆 ‘ 𝐶 ) ) ) ) )
56 23 54 55 mpbir2and ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐶 ) = ( 𝑀 ‘ 𝐶 ) )
57 56 eqcomd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 ) )