Metamath Proof Explorer

Theorem mirln

Description: If two points are on the same line, so is the mirror point of one through the other. (Contributed by Thierry Arnoux, 21-Dec-2019)

Ref Expression
Hypotheses mirval.p 
|- P = ( Base ` G )
mirval.d 
|- .- = ( dist ` G )
mirval.i 
|- I = ( Itv ` G )
mirval.l 
|- L = ( LineG ` G )
mirval.s 
|- S = ( pInvG ` G )
mirval.g 
|- ( ph -> G e. TarskiG )
mirln.m 
|- M = ( S ` A )
mirln.1 
|- ( ph -> D e. ran L )
mirln.a 
|- ( ph -> A e. D )
mirln.b 
|- ( ph -> B e. D )
Assertion mirln 
|- ( ph -> ( M ` B ) e. 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 = ( LineG ` G )
5 mirval.s 
 |-  S = ( pInvG ` G )
6 mirval.g 
 |-  ( ph -> G e. TarskiG )
7 mirln.m 
 |-  M = ( S ` A )
8 mirln.1 
 |-  ( ph -> D e. ran L )
9 mirln.a 
 |-  ( ph -> A e. D )
10 mirln.b 
 |-  ( ph -> B e. D )
11 simpr 
 |-  ( ( ph /\ A = B ) -> A = B )
12 11 fveq2d 
 |-  ( ( ph /\ A = B ) -> ( M ` A ) = ( M ` B ) )
13 6 adantr 
 |-  ( ( ph /\ A = B ) -> G e. TarskiG )
14 1 4 3 6 8 9 tglnpt 
 |-  ( ph -> A e. P )
15 14 adantr 
 |-  ( ( ph /\ A = B ) -> A e. P )
16 1 2 3 4 5 13 15 7 mircinv 
 |-  ( ( ph /\ A = B ) -> ( M ` A ) = A )
17 12 16 eqtr3d 
 |-  ( ( ph /\ A = B ) -> ( M ` B ) = A )
18 9 adantr 
 |-  ( ( ph /\ A = B ) -> A e. D )
19 17 18 eqeltrd 
 |-  ( ( ph /\ A = B ) -> ( M ` B ) e. D )
20 6 adantr 
 |-  ( ( ph /\ A =/= B ) -> G e. TarskiG )
21 14 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. P )
22 1 4 3 6 8 10 tglnpt 
 |-  ( ph -> B e. P )
23 22 adantr 
 |-  ( ( ph /\ A =/= B ) -> B e. P )
24 1 2 3 4 5 20 21 7 23 mircl 
 |-  ( ( ph /\ A =/= B ) -> ( M ` B ) e. P )
25 simpr 
 |-  ( ( ph /\ A =/= B ) -> A =/= B )
26 1 2 3 4 5 6 14 7 22 mirbtwn 
 |-  ( ph -> A e. ( ( M ` B ) I B ) )
27 26 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. ( ( M ` B ) I B ) )
28 1 3 4 20 21 23 24 25 27 btwnlng2 
 |-  ( ( ph /\ A =/= B ) -> ( M ` B ) e. ( A L B ) )
29 8 adantr 
 |-  ( ( ph /\ A =/= B ) -> D e. ran L )
30 9 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. D )
31 10 adantr 
 |-  ( ( ph /\ A =/= B ) -> B e. D )
32 1 3 4 20 21 23 25 25 29 30 31 tglinethru 
 |-  ( ( ph /\ A =/= B ) -> D = ( A L B ) )
33 28 32 eleqtrrd 
 |-  ( ( ph /\ A =/= B ) -> ( M ` B ) e. D )
34 19 33 pm2.61dane 
 |-  ( ph -> ( M ` B ) e. D )