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 = Line 𝒢 G
mirval.s S = pInv 𝒢 G
mirval.g φ G 𝒢 Tarski
mirhl.m M = S A
mirhl.k K = hl 𝒢 G
mirhl.a φ A P
mirhl.x φ X P
mirhl.y φ Y P
mirhl.z φ Z P
mirbtwnhl.1 φ X A
mirbtwnhl.2 φ Y A
mirbtwnhl.3 φ A X I Y
Assertion mirbtwnhl φ 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 = Line 𝒢 G
5 mirval.s S = pInv 𝒢 G
6 mirval.g φ G 𝒢 Tarski
7 mirhl.m M = S A
8 mirhl.k K = hl 𝒢 G
9 mirhl.a φ A P
10 mirhl.x φ X P
11 mirhl.y φ Y P
12 mirhl.z φ Z P
13 mirbtwnhl.1 φ X A
14 mirbtwnhl.2 φ Y A
15 mirbtwnhl.3 φ A X I Y
16 simpr φ Z = A Z = A
17 1 3 8 9 10 9 6 hleqnid φ ¬ A K A X
18 17 adantr φ Z = A ¬ A K A X
19 16 18 eqnbrtrd φ Z = A ¬ Z K A X
20 16 fveq2d φ Z = A M Z = M A
21 1 2 3 4 5 6 9 7 mircinv φ M A = A
22 21 adantr φ Z = A M A = A
23 20 22 eqtrd φ Z = A M Z = A
24 1 3 8 9 11 9 6 hleqnid φ ¬ A K A Y
25 24 adantr φ Z = A ¬ A K A Y
26 23 25 eqnbrtrd φ Z = A ¬ M Z K A Y
27 19 26 2falsed φ Z = A Z K A X M Z K A Y
28 simplr φ Z A Z K A X Z A
29 28 neneqd φ Z A Z K A X ¬ Z = A
30 6 ad3antrrr φ Z A Z K A X M Z = A G 𝒢 Tarski
31 9 ad3antrrr φ Z A Z K A X M Z = A A P
32 12 ad3antrrr φ Z A Z K A X M Z = A Z P
33 simpr φ Z A Z K A X M Z = A M Z = A
34 21 ad3antrrr φ Z A Z K A X M Z = A M A = A
35 33 34 eqtr4d φ 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 φ Z A Z K A X M Z = A Z = A
37 29 36 mtand φ Z A Z K A X ¬ M Z = A
38 37 neqned φ Z A Z K A X M Z A
39 14 ad2antrr φ Z A Z K A X Y A
40 6 ad2antrr φ Z A Z K A X G 𝒢 Tarski
41 10 ad2antrr φ Z A Z K A X X P
42 9 ad2antrr φ Z A Z K A X A P
43 1 2 3 4 5 6 9 7 12 mircl φ M Z P
44 43 ad2antrr φ Z A Z K A X M Z P
45 11 ad2antrr φ Z A Z K A X Y P
46 13 ad2antrr φ Z A Z K A X X A
47 12 ad2antrr φ Z A Z K A X Z P
48 1 3 8 12 10 9 6 ishlg φ Z K A X Z A X A Z A I X X A I Z
49 48 adantr φ Z A Z K A X Z A X A Z A I X X A I Z
50 49 biimpa φ Z A Z K A X Z A X A Z A I X X A I Z
51 50 simp3d φ Z A Z K A X Z A I X X A I Z
52 51 orcomd φ Z A Z K A X X A I Z Z A I X
53 1 2 3 4 5 40 7 42 41 47 52 mirconn φ Z A Z K A X A X I M Z
54 15 ad2antrr φ Z A Z K A X A X I Y
55 1 3 40 41 42 44 45 46 53 54 tgbtwnconn2 φ Z A Z K A X M Z A I Y Y A I M Z
56 1 3 8 43 11 9 6 ishlg φ M Z K A Y M Z A Y A M Z A I Y Y A I M Z
57 56 adantr φ Z A M Z K A Y M Z A Y A M Z A I Y Y A I M Z
58 57 adantr φ Z A Z K A X M Z K A Y M Z A Y A M Z A I Y Y A I M Z
59 38 39 55 58 mpbir3and φ Z A Z K A X M Z K A Y
60 simplr φ Z A M Z K A Y Z A
61 13 ad2antrr φ Z A M Z K A Y X A
62 6 ad2antrr φ Z A M Z K A Y G 𝒢 Tarski
63 11 ad2antrr φ Z A M Z K A Y Y P
64 9 ad2antrr φ Z A M Z K A Y A P
65 12 ad2antrr φ Z A M Z K A Y Z P
66 10 ad2antrr φ Z A M Z K A Y X P
67 14 ad2antrr φ Z A M Z K A Y Y A
68 21 ad2antrr φ Z A M Z K A Y M A = A
69 43 ad2antrr φ Z A M Z K A Y M Z P
70 1 2 3 4 5 62 64 7 63 mircl φ Z A M Z K A Y M Y P
71 57 biimpa φ Z A M Z K A Y M Z A Y A M Z A I Y Y A I M Z
72 71 simp3d φ Z A M Z K A Y M Z A I Y Y A I M Z
73 1 2 3 4 5 62 7 64 69 63 72 mirconn φ Z A M Z K A Y A M Z I M Y
74 1 2 3 62 69 64 70 73 tgbtwncom φ Z A M Z K A Y A M Y I M Z
75 68 74 eqeltrd φ Z A M Z K A Y M A M Y I M Z
76 1 2 3 4 5 62 64 7 63 64 65 mirbtwnb φ Z A M Z K A Y A Y I Z M A M Y I M Z
77 75 76 mpbird φ Z A M Z K A Y A Y I Z
78 1 2 3 6 10 9 11 15 tgbtwncom φ A Y I X
79 78 ad2antrr φ Z A M Z K A Y A Y I X
80 1 3 62 63 64 65 66 67 77 79 tgbtwnconn2 φ Z A M Z K A Y Z A I X X A I Z
81 49 adantr φ Z A M Z K A Y Z K A X Z A X A Z A I X X A I Z
82 60 61 80 81 mpbir3and φ Z A M Z K A Y Z K A X
83 59 82 impbida φ Z A Z K A X M Z K A Y
84 27 83 pm2.61dane φ Z K A X M Z K A Y