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 ) )