Metamath Proof Explorer

Theorem mirhl

Description: If two points X and Y are on the same half-line from Z , the same applies to the mirror points. (Contributed by Thierry Arnoux, 21-Feb-2020)

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 )
mirhl.m 
|- M = ( S ` A )
mirhl.k 
|- K = ( hlG ` G )
mirhl.a 
|- ( ph -> A e. P )
mirhl.x 
|- ( ph -> X e. P )
mirhl.y 
|- ( ph -> Y e. P )
mirhl.z 
|- ( ph -> Z e. P )
mirhl.1 
|- ( ph -> X ( K ` Z ) Y )
Assertion mirhl 
|- ( ph -> ( M ` X ) ( K ` ( M ` Z ) ) ( M ` Y ) )

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 mirhl.m 
 |-  M = ( S ` A )
8 mirhl.k 
 |-  K = ( hlG ` G )
9 mirhl.a 
 |-  ( ph -> A e. P )
10 mirhl.x 
 |-  ( ph -> X e. P )
11 mirhl.y 
 |-  ( ph -> Y e. P )
12 mirhl.z 
 |-  ( ph -> Z e. P )
13 mirhl.1 
 |-  ( ph -> X ( K ` Z ) Y )
14 6 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Z ) ) -> G e. TarskiG )
15 9 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Z ) ) -> A e. P )
16 10 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Z ) ) -> X e. P )
17 12 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Z ) ) -> Z e. P )
18 simpr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Z ) ) -> ( M ` X ) = ( M ` Z ) )
19 1 2 3 4 5 14 15 7 16 17 18 mireq 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Z ) ) -> X = Z )
20 1 3 8 10 11 12 6 ishlg 
 |-  ( ph -> ( X ( K ` Z ) Y <-> ( X =/= Z /\ Y =/= Z /\ ( X e. ( Z I Y ) \/ Y e. ( Z I X ) ) ) ) )
21 13 20 mpbid 
 |-  ( ph -> ( X =/= Z /\ Y =/= Z /\ ( X e. ( Z I Y ) \/ Y e. ( Z I X ) ) ) )
22 21 simp1d 
 |-  ( ph -> X =/= Z )
23 22 adantr 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Z ) ) -> X =/= Z )
24 23 neneqd 
 |-  ( ( ph /\ ( M ` X ) = ( M ` Z ) ) -> -. X = Z )
25 19 24 pm2.65da 
 |-  ( ph -> -. ( M ` X ) = ( M ` Z ) )
26 25 neqned 
 |-  ( ph -> ( M ` X ) =/= ( M ` Z ) )
27 6 adantr 
 |-  ( ( ph /\ ( M ` Y ) = ( M ` Z ) ) -> G e. TarskiG )
28 9 adantr 
 |-  ( ( ph /\ ( M ` Y ) = ( M ` Z ) ) -> A e. P )
29 11 adantr 
 |-  ( ( ph /\ ( M ` Y ) = ( M ` Z ) ) -> Y e. P )
30 12 adantr 
 |-  ( ( ph /\ ( M ` Y ) = ( M ` Z ) ) -> Z e. P )
31 simpr 
 |-  ( ( ph /\ ( M ` Y ) = ( M ` Z ) ) -> ( M ` Y ) = ( M ` Z ) )
32 1 2 3 4 5 27 28 7 29 30 31 mireq 
 |-  ( ( ph /\ ( M ` Y ) = ( M ` Z ) ) -> Y = Z )
33 21 simp2d 
 |-  ( ph -> Y =/= Z )
34 33 adantr 
 |-  ( ( ph /\ ( M ` Y ) = ( M ` Z ) ) -> Y =/= Z )
35 34 neneqd 
 |-  ( ( ph /\ ( M ` Y ) = ( M ` Z ) ) -> -. Y = Z )
36 32 35 pm2.65da 
 |-  ( ph -> -. ( M ` Y ) = ( M ` Z ) )
37 36 neqned 
 |-  ( ph -> ( M ` Y ) =/= ( M ` Z ) )
38 21 simp3d 
 |-  ( ph -> ( X e. ( Z I Y ) \/ Y e. ( Z I X ) ) )
39 6 adantr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> G e. TarskiG )
40 9 adantr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> A e. P )
41 12 adantr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> Z e. P )
42 10 adantr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> X e. P )
43 11 adantr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> Y e. P )
44 simpr 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> X e. ( Z I Y ) )
45 1 2 3 4 5 39 40 7 41 42 43 44 mirbtwni 
 |-  ( ( ph /\ X e. ( Z I Y ) ) -> ( M ` X ) e. ( ( M ` Z ) I ( M ` Y ) ) )
46 45 ex 
 |-  ( ph -> ( X e. ( Z I Y ) -> ( M ` X ) e. ( ( M ` Z ) I ( M ` Y ) ) ) )
47 6 adantr 
 |-  ( ( ph /\ Y e. ( Z I X ) ) -> G e. TarskiG )
48 9 adantr 
 |-  ( ( ph /\ Y e. ( Z I X ) ) -> A e. P )
49 12 adantr 
 |-  ( ( ph /\ Y e. ( Z I X ) ) -> Z e. P )
50 11 adantr 
 |-  ( ( ph /\ Y e. ( Z I X ) ) -> Y e. P )
51 10 adantr 
 |-  ( ( ph /\ Y e. ( Z I X ) ) -> X e. P )
52 simpr 
 |-  ( ( ph /\ Y e. ( Z I X ) ) -> Y e. ( Z I X ) )
53 1 2 3 4 5 47 48 7 49 50 51 52 mirbtwni 
 |-  ( ( ph /\ Y e. ( Z I X ) ) -> ( M ` Y ) e. ( ( M ` Z ) I ( M ` X ) ) )
54 53 ex 
 |-  ( ph -> ( Y e. ( Z I X ) -> ( M ` Y ) e. ( ( M ` Z ) I ( M ` X ) ) ) )
55 46 54 orim12d 
 |-  ( ph -> ( ( X e. ( Z I Y ) \/ Y e. ( Z I X ) ) -> ( ( M ` X ) e. ( ( M ` Z ) I ( M ` Y ) ) \/ ( M ` Y ) e. ( ( M ` Z ) I ( M ` X ) ) ) ) )
56 38 55 mpd 
 |-  ( ph -> ( ( M ` X ) e. ( ( M ` Z ) I ( M ` Y ) ) \/ ( M ` Y ) e. ( ( M ` Z ) I ( M ` X ) ) ) )
57 1 2 3 4 5 6 9 7 10 mircl 
 |-  ( ph -> ( M ` X ) e. P )
58 1 2 3 4 5 6 9 7 11 mircl 
 |-  ( ph -> ( M ` Y ) e. P )
59 1 2 3 4 5 6 9 7 12 mircl 
 |-  ( ph -> ( M ` Z ) e. P )
60 1 3 8 57 58 59 6 ishlg 
 |-  ( ph -> ( ( M ` X ) ( K ` ( M ` Z ) ) ( M ` Y ) <-> ( ( M ` X ) =/= ( M ` Z ) /\ ( M ` Y ) =/= ( M ` Z ) /\ ( ( M ` X ) e. ( ( M ` Z ) I ( M ` Y ) ) \/ ( M ` Y ) e. ( ( M ` Z ) I ( M ` X ) ) ) ) ) )
61 26 37 56 60 mpbir3and 
 |-  ( ph -> ( M ` X ) ( K ` ( M ` Z ) ) ( M ` Y ) )