Metamath Proof Explorer


Theorem mirln2

Description: If a point and its mirror point are both on the same line, so is the center of the point inversion. (Contributed by Thierry Arnoux, 3-Mar-2020)

Ref Expression
Hypotheses mirval.p P = Base G
mirval.d - ˙ = dist G
mirval.i I = Itv G
mirval.l L = Line 𝒢 G
mirval.s S = pInv 𝒢 G
mirval.g φ G 𝒢 Tarski
mirln2.m M = S A
mirln2.d φ D ran L
mirln2.a φ A P
mirln2.1 φ B D
mirln2.2 φ M B D
Assertion mirln2 φ A D

Proof

Step Hyp Ref Expression
1 mirval.p P = Base G
2 mirval.d - ˙ = dist G
3 mirval.i I = Itv G
4 mirval.l L = Line 𝒢 G
5 mirval.s S = pInv 𝒢 G
6 mirval.g φ G 𝒢 Tarski
7 mirln2.m M = S A
8 mirln2.d φ D ran L
9 mirln2.a φ A P
10 mirln2.1 φ B D
11 mirln2.2 φ M B D
12 1 4 3 6 8 10 tglnpt φ B P
13 1 2 3 4 5 6 9 7 12 mirinv φ M B = B A = B
14 13 biimpa φ M B = B A = B
15 10 adantr φ M B = B B D
16 14 15 eqeltrd φ M B = B A D
17 6 adantr φ M B B G 𝒢 Tarski
18 1 4 3 6 8 11 tglnpt φ M B P
19 18 adantr φ M B B M B P
20 12 adantr φ M B B B P
21 9 adantr φ M B B A P
22 simpr φ M B B M B B
23 1 2 3 4 5 17 21 7 20 mirbtwn φ M B B A M B I B
24 1 3 4 17 19 20 21 22 23 btwnlng1 φ M B B A M B L B
25 8 adantr φ M B B D ran L
26 11 adantr φ M B B M B D
27 10 adantr φ M B B B D
28 1 3 4 17 19 20 22 22 25 26 27 tglinethru φ M B B D = M B L B
29 24 28 eleqtrrd φ M B B A D
30 16 29 pm2.61dane φ A D