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