Metamath Proof Explorer

Theorem mirbtwnhl

Description: If the center of the point inversion A is between two points X and Y , then the half lines are mirrored. (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 = ( 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 )
mirbtwnhl.1 
|- ( ph -> X =/= A )
mirbtwnhl.2 
|- ( ph -> Y =/= A )
mirbtwnhl.3 
|- ( ph -> A e. ( X I Y ) )
Assertion mirbtwnhl 
|- ( ph -> ( Z ( K ` A ) X <-> ( M ` Z ) ( K ` A ) 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 mirbtwnhl.1 
 |-  ( ph -> X =/= A )
14 mirbtwnhl.2 
 |-  ( ph -> Y =/= A )
15 mirbtwnhl.3 
 |-  ( ph -> A e. ( X I Y ) )
16 simpr 
 |-  ( ( ph /\ Z = A ) -> Z = A )
17 1 3 8 9 10 9 6 hleqnid 
 |-  ( ph -> -. A ( K ` A ) X )
18 17 adantr 
 |-  ( ( ph /\ Z = A ) -> -. A ( K ` A ) X )
19 16 18 eqnbrtrd 
 |-  ( ( ph /\ Z = A ) -> -. Z ( K ` A ) X )
20 16 fveq2d 
 |-  ( ( ph /\ Z = A ) -> ( M ` Z ) = ( M ` A ) )
21 1 2 3 4 5 6 9 7 mircinv 
 |-  ( ph -> ( M ` A ) = A )
22 21 adantr 
 |-  ( ( ph /\ Z = A ) -> ( M ` A ) = A )
23 20 22 eqtrd 
 |-  ( ( ph /\ Z = A ) -> ( M ` Z ) = A )
24 1 3 8 9 11 9 6 hleqnid 
 |-  ( ph -> -. A ( K ` A ) Y )
25 24 adantr 
 |-  ( ( ph /\ Z = A ) -> -. A ( K ` A ) Y )
26 23 25 eqnbrtrd 
 |-  ( ( ph /\ Z = A ) -> -. ( M ` Z ) ( K ` A ) Y )
27 19 26 2falsed 
 |-  ( ( ph /\ Z = A ) -> ( Z ( K ` A ) X <-> ( M ` Z ) ( K ` A ) Y ) )
28 simplr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> Z =/= A )
29 28 neneqd 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> -. Z = A )
30 6 ad3antrrr 
 |-  ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> G e. TarskiG )
31 9 ad3antrrr 
 |-  ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> A e. P )
32 12 ad3antrrr 
 |-  ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> Z e. P )
33 simpr 
 |-  ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> ( M ` Z ) = A )
34 21 ad3antrrr 
 |-  ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> ( M ` A ) = A )
35 33 34 eqtr4d 
 |-  ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> ( M ` Z ) = ( M ` A ) )
36 1 2 3 4 5 30 31 7 32 31 35 mireq 
 |-  ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> Z = A )
37 29 36 mtand 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> -. ( M ` Z ) = A )
38 37 neqned 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( M ` Z ) =/= A )
39 14 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> Y =/= A )
40 6 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> G e. TarskiG )
41 10 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> X e. P )
42 9 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> A e. P )
43 1 2 3 4 5 6 9 7 12 mircl 
 |-  ( ph -> ( M ` Z ) e. P )
44 43 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( M ` Z ) e. P )
45 11 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> Y e. P )
46 13 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> X =/= A )
47 12 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> Z e. P )
48 1 3 8 12 10 9 6 ishlg 
 |-  ( ph -> ( Z ( K ` A ) X <-> ( Z =/= A /\ X =/= A /\ ( Z e. ( A I X ) \/ X e. ( A I Z ) ) ) ) )
49 48 adantr 
 |-  ( ( ph /\ Z =/= A ) -> ( Z ( K ` A ) X <-> ( Z =/= A /\ X =/= A /\ ( Z e. ( A I X ) \/ X e. ( A I Z ) ) ) ) )
50 49 biimpa 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( Z =/= A /\ X =/= A /\ ( Z e. ( A I X ) \/ X e. ( A I Z ) ) ) )
51 50 simp3d 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( Z e. ( A I X ) \/ X e. ( A I Z ) ) )
52 51 orcomd 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( X e. ( A I Z ) \/ Z e. ( A I X ) ) )
53 1 2 3 4 5 40 7 42 41 47 52 mirconn 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> A e. ( X I ( M ` Z ) ) )
54 15 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> A e. ( X I Y ) )
55 1 3 40 41 42 44 45 46 53 54 tgbtwnconn2 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) )
56 1 3 8 43 11 9 6 ishlg 
 |-  ( ph -> ( ( M ` Z ) ( K ` A ) Y <-> ( ( M ` Z ) =/= A /\ Y =/= A /\ ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) ) ) )
57 56 adantr 
 |-  ( ( ph /\ Z =/= A ) -> ( ( M ` Z ) ( K ` A ) Y <-> ( ( M ` Z ) =/= A /\ Y =/= A /\ ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) ) ) )
58 57 adantr 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( ( M ` Z ) ( K ` A ) Y <-> ( ( M ` Z ) =/= A /\ Y =/= A /\ ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) ) ) )
59 38 39 55 58 mpbir3and 
 |-  ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( M ` Z ) ( K ` A ) Y )
60 simplr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> Z =/= A )
61 13 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> X =/= A )
62 6 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> G e. TarskiG )
63 11 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> Y e. P )
64 9 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> A e. P )
65 12 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> Z e. P )
66 10 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> X e. P )
67 14 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> Y =/= A )
68 21 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( M ` A ) = A )
69 43 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( M ` Z ) e. P )
70 1 2 3 4 5 62 64 7 63 mircl 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( M ` Y ) e. P )
71 57 biimpa 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( ( M ` Z ) =/= A /\ Y =/= A /\ ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) ) )
72 71 simp3d 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) )
73 1 2 3 4 5 62 7 64 69 63 72 mirconn 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> A e. ( ( M ` Z ) I ( M ` Y ) ) )
74 1 2 3 62 69 64 70 73 tgbtwncom 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> A e. ( ( M ` Y ) I ( M ` Z ) ) )
75 68 74 eqeltrd 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( M ` A ) e. ( ( M ` Y ) I ( M ` Z ) ) )
76 1 2 3 4 5 62 64 7 63 64 65 mirbtwnb 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( A e. ( Y I Z ) <-> ( M ` A ) e. ( ( M ` Y ) I ( M ` Z ) ) ) )
77 75 76 mpbird 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> A e. ( Y I Z ) )
78 1 2 3 6 10 9 11 15 tgbtwncom 
 |-  ( ph -> A e. ( Y I X ) )
79 78 ad2antrr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> A e. ( Y I X ) )
80 1 3 62 63 64 65 66 67 77 79 tgbtwnconn2 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( Z e. ( A I X ) \/ X e. ( A I Z ) ) )
81 49 adantr 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( Z ( K ` A ) X <-> ( Z =/= A /\ X =/= A /\ ( Z e. ( A I X ) \/ X e. ( A I Z ) ) ) ) )
82 60 61 80 81 mpbir3and 
 |-  ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> Z ( K ` A ) X )
83 59 82 impbida 
 |-  ( ( ph /\ Z =/= A ) -> ( Z ( K ` A ) X <-> ( M ` Z ) ( K ` A ) Y ) )
84 27 83 pm2.61dane 
 |-  ( ph -> ( Z ( K ` A ) X <-> ( M ` Z ) ( K ` A ) Y ) )