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 P = Base G
ismid.d - ˙ = dist G
ismid.i I = Itv G
ismid.g φ G 𝒢 Tarski
ismid.1 φ G Dim 𝒢 2
lmif.m M = lInv 𝒢 G D
lmif.l L = Line 𝒢 G
lmif.d φ D ran L
lmicl.1 φ A P
lmimid.s S = pInv 𝒢 G B
lmimid.r φ ⟨“ ABC ”⟩ 𝒢 G
lmimid.a φ A D
lmimid.b φ B D
lmimid.c φ C P
lmimid.d φ A B
Assertion lmimid φ M C = S C

Proof

Step Hyp Ref Expression
1 ismid.p P = Base G
2 ismid.d - ˙ = dist G
3 ismid.i I = Itv G
4 ismid.g φ G 𝒢 Tarski
5 ismid.1 φ G Dim 𝒢 2
6 lmif.m M = lInv 𝒢 G D
7 lmif.l L = Line 𝒢 G
8 lmif.d φ D ran L
9 lmicl.1 φ A P
10 lmimid.s S = pInv 𝒢 G B
11 lmimid.r φ ⟨“ ABC ”⟩ 𝒢 G
12 lmimid.a φ A D
13 lmimid.b φ B D
14 lmimid.c φ C P
15 lmimid.d φ A B
16 10 a1i φ S = pInv 𝒢 G B
17 16 fveq1d φ S C = pInv 𝒢 G B C
18 eqid pInv 𝒢 G = pInv 𝒢 G
19 1 7 3 4 8 13 tglnpt φ B P
20 1 2 3 7 18 4 19 10 14 mircl φ S C P
21 1 2 3 4 5 14 20 18 19 ismidb φ S C = pInv 𝒢 G B C C mid 𝒢 G S C = B
22 17 21 mpbid φ C mid 𝒢 G S C = B
23 22 13 eqeltrd φ C mid 𝒢 G S C D
24 df-ne C S C ¬ C = S C
25 4 adantr φ C S C G 𝒢 Tarski
26 8 adantr φ C S C D ran L
27 14 adantr φ C S C C P
28 20 adantr φ C S C S C P
29 simpr φ C S C C S C
30 1 3 7 25 27 28 29 tgelrnln φ C S C C L S C ran L
31 13 adantr φ C S C B D
32 19 adantr φ C S C B P
33 1 2 3 4 5 14 20 midbtwn φ C mid 𝒢 G S C C I S C
34 22 33 eqeltrrd φ B C I S C
35 34 adantr φ C S C B C I S C
36 1 3 7 25 27 28 32 29 35 btwnlng1 φ C S C B C L S C
37 31 36 elind φ C S C B D C L S C
38 12 adantr φ C S C A D
39 1 3 7 25 27 28 29 tglinerflx1 φ C S C C C L S C
40 15 adantr φ C S C A B
41 1 2 3 7 18 4 19 10 14 mirinv φ S C = C B = C
42 eqcom B = C C = B
43 41 42 bitrdi φ S C = C C = B
44 43 biimpar φ C = B S C = C
45 44 eqcomd φ C = B C = S C
46 45 ex φ C = B C = S C
47 46 necon3d φ C S C C B
48 47 imp φ C S C C B
49 11 adantr φ C S C ⟨“ ABC ”⟩ 𝒢 G
50 1 2 3 7 25 26 30 37 38 39 40 48 49 ragperp φ C S C D 𝒢 G C L S C
51 50 ex φ C S C D 𝒢 G C L S C
52 24 51 syl5bir φ ¬ C = S C D 𝒢 G C L S C
53 52 orrd φ C = S C D 𝒢 G C L S C
54 53 orcomd φ D 𝒢 G C L S C C = S C
55 1 2 3 4 5 6 7 8 14 20 islmib φ S C = M C C mid 𝒢 G S C D D 𝒢 G C L S C C = S C
56 23 54 55 mpbir2and φ S C = M C
57 56 eqcomd φ M C = S C