Proof of Theorem mirhl
Step | Hyp | Ref
| Expression |
1 | | mirval.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
2 | | mirval.d |
. . . . 5
⊢ − =
(dist‘𝐺) |
3 | | mirval.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
4 | | mirval.l |
. . . . 5
⊢ 𝐿 = (LineG‘𝐺) |
5 | | mirval.s |
. . . . 5
⊢ 𝑆 = (pInvG‘𝐺) |
6 | | mirval.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
7 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑋) = (𝑀‘𝑍)) → 𝐺 ∈ TarskiG) |
8 | | mirhl.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
9 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑋) = (𝑀‘𝑍)) → 𝐴 ∈ 𝑃) |
10 | | mirhl.m |
. . . . 5
⊢ 𝑀 = (𝑆‘𝐴) |
11 | | mirhl.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
12 | 11 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑋) = (𝑀‘𝑍)) → 𝑋 ∈ 𝑃) |
13 | | mirhl.z |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑃) |
14 | 13 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑋) = (𝑀‘𝑍)) → 𝑍 ∈ 𝑃) |
15 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑋) = (𝑀‘𝑍)) → (𝑀‘𝑋) = (𝑀‘𝑍)) |
16 | 1, 2, 3, 4, 5, 7, 9, 10, 12, 14, 15 | mireq 27026 |
. . . 4
⊢ ((𝜑 ∧ (𝑀‘𝑋) = (𝑀‘𝑍)) → 𝑋 = 𝑍) |
17 | | mirhl.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑋(𝐾‘𝑍)𝑌) |
18 | | mirhl.k |
. . . . . . . . 9
⊢ 𝐾 = (hlG‘𝐺) |
19 | | mirhl.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
20 | 1, 3, 18, 11, 19, 13, 6 | ishlg 26963 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(𝐾‘𝑍)𝑌 ↔ (𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ∧ (𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑍𝐼𝑋))))) |
21 | 17, 20 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ∧ (𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑍𝐼𝑋)))) |
22 | 21 | simp1d 1141 |
. . . . . 6
⊢ (𝜑 → 𝑋 ≠ 𝑍) |
23 | 22 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑋) = (𝑀‘𝑍)) → 𝑋 ≠ 𝑍) |
24 | 23 | neneqd 2948 |
. . . 4
⊢ ((𝜑 ∧ (𝑀‘𝑋) = (𝑀‘𝑍)) → ¬ 𝑋 = 𝑍) |
25 | 16, 24 | pm2.65da 814 |
. . 3
⊢ (𝜑 → ¬ (𝑀‘𝑋) = (𝑀‘𝑍)) |
26 | 25 | neqned 2950 |
. 2
⊢ (𝜑 → (𝑀‘𝑋) ≠ (𝑀‘𝑍)) |
27 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑌) = (𝑀‘𝑍)) → 𝐺 ∈ TarskiG) |
28 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑌) = (𝑀‘𝑍)) → 𝐴 ∈ 𝑃) |
29 | 19 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑌) = (𝑀‘𝑍)) → 𝑌 ∈ 𝑃) |
30 | 13 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑌) = (𝑀‘𝑍)) → 𝑍 ∈ 𝑃) |
31 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑌) = (𝑀‘𝑍)) → (𝑀‘𝑌) = (𝑀‘𝑍)) |
32 | 1, 2, 3, 4, 5, 27,
28, 10, 29, 30, 31 | mireq 27026 |
. . . 4
⊢ ((𝜑 ∧ (𝑀‘𝑌) = (𝑀‘𝑍)) → 𝑌 = 𝑍) |
33 | 21 | simp2d 1142 |
. . . . . 6
⊢ (𝜑 → 𝑌 ≠ 𝑍) |
34 | 33 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑀‘𝑌) = (𝑀‘𝑍)) → 𝑌 ≠ 𝑍) |
35 | 34 | neneqd 2948 |
. . . 4
⊢ ((𝜑 ∧ (𝑀‘𝑌) = (𝑀‘𝑍)) → ¬ 𝑌 = 𝑍) |
36 | 32, 35 | pm2.65da 814 |
. . 3
⊢ (𝜑 → ¬ (𝑀‘𝑌) = (𝑀‘𝑍)) |
37 | 36 | neqned 2950 |
. 2
⊢ (𝜑 → (𝑀‘𝑌) ≠ (𝑀‘𝑍)) |
38 | 21 | simp3d 1143 |
. . 3
⊢ (𝜑 → (𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑍𝐼𝑋))) |
39 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑍𝐼𝑌)) → 𝐺 ∈ TarskiG) |
40 | 8 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑍𝐼𝑌)) → 𝐴 ∈ 𝑃) |
41 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑍𝐼𝑌)) → 𝑍 ∈ 𝑃) |
42 | 11 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑍𝐼𝑌)) → 𝑋 ∈ 𝑃) |
43 | 19 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑍𝐼𝑌)) → 𝑌 ∈ 𝑃) |
44 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑍𝐼𝑌)) → 𝑋 ∈ (𝑍𝐼𝑌)) |
45 | 1, 2, 3, 4, 5, 39,
40, 10, 41, 42, 43, 44 | mirbtwni 27032 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑍𝐼𝑌)) → (𝑀‘𝑋) ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑌))) |
46 | 45 | ex 413 |
. . . 4
⊢ (𝜑 → (𝑋 ∈ (𝑍𝐼𝑌) → (𝑀‘𝑋) ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑌)))) |
47 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑍𝐼𝑋)) → 𝐺 ∈ TarskiG) |
48 | 8 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑍𝐼𝑋)) → 𝐴 ∈ 𝑃) |
49 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑍𝐼𝑋)) → 𝑍 ∈ 𝑃) |
50 | 19 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑍𝐼𝑋)) → 𝑌 ∈ 𝑃) |
51 | 11 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑍𝐼𝑋)) → 𝑋 ∈ 𝑃) |
52 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑍𝐼𝑋)) → 𝑌 ∈ (𝑍𝐼𝑋)) |
53 | 1, 2, 3, 4, 5, 47,
48, 10, 49, 50, 51, 52 | mirbtwni 27032 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑍𝐼𝑋)) → (𝑀‘𝑌) ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑋))) |
54 | 53 | ex 413 |
. . . 4
⊢ (𝜑 → (𝑌 ∈ (𝑍𝐼𝑋) → (𝑀‘𝑌) ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑋)))) |
55 | 46, 54 | orim12d 962 |
. . 3
⊢ (𝜑 → ((𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑍𝐼𝑋)) → ((𝑀‘𝑋) ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑌)) ∨ (𝑀‘𝑌) ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑋))))) |
56 | 38, 55 | mpd 15 |
. 2
⊢ (𝜑 → ((𝑀‘𝑋) ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑌)) ∨ (𝑀‘𝑌) ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑋)))) |
57 | 1, 2, 3, 4, 5, 6, 8, 10, 11 | mircl 27022 |
. . 3
⊢ (𝜑 → (𝑀‘𝑋) ∈ 𝑃) |
58 | 1, 2, 3, 4, 5, 6, 8, 10, 19 | mircl 27022 |
. . 3
⊢ (𝜑 → (𝑀‘𝑌) ∈ 𝑃) |
59 | 1, 2, 3, 4, 5, 6, 8, 10, 13 | mircl 27022 |
. . 3
⊢ (𝜑 → (𝑀‘𝑍) ∈ 𝑃) |
60 | 1, 3, 18, 57, 58, 59, 6 | ishlg 26963 |
. 2
⊢ (𝜑 → ((𝑀‘𝑋)(𝐾‘(𝑀‘𝑍))(𝑀‘𝑌) ↔ ((𝑀‘𝑋) ≠ (𝑀‘𝑍) ∧ (𝑀‘𝑌) ≠ (𝑀‘𝑍) ∧ ((𝑀‘𝑋) ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑌)) ∨ (𝑀‘𝑌) ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑋)))))) |
61 | 26, 37, 56, 60 | mpbir3and 1341 |
1
⊢ (𝜑 → (𝑀‘𝑋)(𝐾‘(𝑀‘𝑍))(𝑀‘𝑌)) |