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 𝑃 = ( Base ‘ 𝐺 )
mirval.d = ( dist ‘ 𝐺 )
mirval.i 𝐼 = ( Itv ‘ 𝐺 )
mirval.l 𝐿 = ( LineG ‘ 𝐺 )
mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ( 𝜑𝐺 ∈ TarskiG )
mirln2.m 𝑀 = ( 𝑆𝐴 )
mirln2.d ( 𝜑𝐷 ∈ ran 𝐿 )
mirln2.a ( 𝜑𝐴𝑃 )
mirln2.1 ( 𝜑𝐵𝐷 )
mirln2.2 ( 𝜑 → ( 𝑀𝐵 ) ∈ 𝐷 )
Assertion mirln2 ( 𝜑𝐴𝐷 )

Proof

Step Hyp Ref Expression
1 mirval.p 𝑃 = ( Base ‘ 𝐺 )
2 mirval.d = ( dist ‘ 𝐺 )
3 mirval.i 𝐼 = ( Itv ‘ 𝐺 )
4 mirval.l 𝐿 = ( LineG ‘ 𝐺 )
5 mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
6 mirval.g ( 𝜑𝐺 ∈ TarskiG )
7 mirln2.m 𝑀 = ( 𝑆𝐴 )
8 mirln2.d ( 𝜑𝐷 ∈ ran 𝐿 )
9 mirln2.a ( 𝜑𝐴𝑃 )
10 mirln2.1 ( 𝜑𝐵𝐷 )
11 mirln2.2 ( 𝜑 → ( 𝑀𝐵 ) ∈ 𝐷 )
12 1 4 3 6 8 10 tglnpt ( 𝜑𝐵𝑃 )
13 1 2 3 4 5 6 9 7 12 mirinv ( 𝜑 → ( ( 𝑀𝐵 ) = 𝐵𝐴 = 𝐵 ) )
14 13 biimpa ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → 𝐴 = 𝐵 )
15 10 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → 𝐵𝐷 )
16 14 15 eqeltrd ( ( 𝜑 ∧ ( 𝑀𝐵 ) = 𝐵 ) → 𝐴𝐷 )
17 6 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
18 1 4 3 6 8 11 tglnpt ( 𝜑 → ( 𝑀𝐵 ) ∈ 𝑃 )
19 18 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → ( 𝑀𝐵 ) ∈ 𝑃 )
20 12 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → 𝐵𝑃 )
21 9 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → 𝐴𝑃 )
22 simpr ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → ( 𝑀𝐵 ) ≠ 𝐵 )
23 1 2 3 4 5 17 21 7 20 mirbtwn ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → 𝐴 ∈ ( ( 𝑀𝐵 ) 𝐼 𝐵 ) )
24 1 3 4 17 19 20 21 22 23 btwnlng1 ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → 𝐴 ∈ ( ( 𝑀𝐵 ) 𝐿 𝐵 ) )
25 8 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → 𝐷 ∈ ran 𝐿 )
26 11 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → ( 𝑀𝐵 ) ∈ 𝐷 )
27 10 adantr ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → 𝐵𝐷 )
28 1 3 4 17 19 20 22 22 25 26 27 tglinethru ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → 𝐷 = ( ( 𝑀𝐵 ) 𝐿 𝐵 ) )
29 24 28 eleqtrrd ( ( 𝜑 ∧ ( 𝑀𝐵 ) ≠ 𝐵 ) → 𝐴𝐷 )
30 16 29 pm2.61dane ( 𝜑𝐴𝐷 )