Proof of Theorem mirbtwnhl
Step | Hyp | Ref
| Expression |
1 | | mirval.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
2 | | mirval.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
3 | | mirhl.k |
. . . . . 6
⊢ 𝐾 = (hlG‘𝐺) |
4 | | mirhl.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
5 | | mirhl.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
6 | | mirval.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
7 | 1, 2, 3, 4, 5, 4, 6 | hleqnid 25927 |
. . . . 5
⊢ (𝜑 → ¬ 𝐴(𝐾‘𝐴)𝑋) |
8 | 7 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → ¬ 𝐴(𝐾‘𝐴)𝑋) |
9 | | simpr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → 𝑍 = 𝐴) |
10 | 9 | breq1d 4885 |
. . . 4
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → (𝑍(𝐾‘𝐴)𝑋 ↔ 𝐴(𝐾‘𝐴)𝑋)) |
11 | 8, 10 | mtbird 317 |
. . 3
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → ¬ 𝑍(𝐾‘𝐴)𝑋) |
12 | | mirhl.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
13 | 1, 2, 3, 4, 12, 4,
6 | hleqnid 25927 |
. . . . 5
⊢ (𝜑 → ¬ 𝐴(𝐾‘𝐴)𝑌) |
14 | 13 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → ¬ 𝐴(𝐾‘𝐴)𝑌) |
15 | 9 | fveq2d 6441 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → (𝑀‘𝑍) = (𝑀‘𝐴)) |
16 | | mirval.d |
. . . . . . . 8
⊢ − =
(dist‘𝐺) |
17 | | mirval.l |
. . . . . . . 8
⊢ 𝐿 = (LineG‘𝐺) |
18 | | mirval.s |
. . . . . . . 8
⊢ 𝑆 = (pInvG‘𝐺) |
19 | | mirhl.m |
. . . . . . . 8
⊢ 𝑀 = (𝑆‘𝐴) |
20 | 1, 16, 2, 17, 18, 6, 4, 19 | mircinv 25987 |
. . . . . . 7
⊢ (𝜑 → (𝑀‘𝐴) = 𝐴) |
21 | 20 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → (𝑀‘𝐴) = 𝐴) |
22 | 15, 21 | eqtrd 2861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → (𝑀‘𝑍) = 𝐴) |
23 | 22 | breq1d 4885 |
. . . 4
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → ((𝑀‘𝑍)(𝐾‘𝐴)𝑌 ↔ 𝐴(𝐾‘𝐴)𝑌)) |
24 | 14, 23 | mtbird 317 |
. . 3
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → ¬ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) |
25 | 11, 24 | 2falsed 368 |
. 2
⊢ ((𝜑 ∧ 𝑍 = 𝐴) → (𝑍(𝐾‘𝐴)𝑋 ↔ (𝑀‘𝑍)(𝐾‘𝐴)𝑌)) |
26 | | simplr 785 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → 𝑍 ≠ 𝐴) |
27 | 26 | neneqd 3004 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → ¬ 𝑍 = 𝐴) |
28 | 6 | ad3antrrr 721 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) ∧ (𝑀‘𝑍) = 𝐴) → 𝐺 ∈ TarskiG) |
29 | 4 | ad3antrrr 721 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) ∧ (𝑀‘𝑍) = 𝐴) → 𝐴 ∈ 𝑃) |
30 | | mirhl.z |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ 𝑃) |
31 | 30 | ad3antrrr 721 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) ∧ (𝑀‘𝑍) = 𝐴) → 𝑍 ∈ 𝑃) |
32 | | simpr 479 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) ∧ (𝑀‘𝑍) = 𝐴) → (𝑀‘𝑍) = 𝐴) |
33 | 20 | ad3antrrr 721 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) ∧ (𝑀‘𝑍) = 𝐴) → (𝑀‘𝐴) = 𝐴) |
34 | 32, 33 | eqtr4d 2864 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) ∧ (𝑀‘𝑍) = 𝐴) → (𝑀‘𝑍) = (𝑀‘𝐴)) |
35 | 1, 16, 2, 17, 18, 28, 29, 19, 31, 29, 34 | mireq 25984 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) ∧ (𝑀‘𝑍) = 𝐴) → 𝑍 = 𝐴) |
36 | 27, 35 | mtand 850 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → ¬ (𝑀‘𝑍) = 𝐴) |
37 | 36 | neqned 3006 |
. . . . 5
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → (𝑀‘𝑍) ≠ 𝐴) |
38 | | mirbtwnhl.2 |
. . . . . 6
⊢ (𝜑 → 𝑌 ≠ 𝐴) |
39 | 38 | ad2antrr 717 |
. . . . 5
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → 𝑌 ≠ 𝐴) |
40 | 6 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → 𝐺 ∈ TarskiG) |
41 | 5 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → 𝑋 ∈ 𝑃) |
42 | 4 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → 𝐴 ∈ 𝑃) |
43 | 1, 16, 2, 17, 18, 6, 4, 19, 30 | mircl 25980 |
. . . . . . 7
⊢ (𝜑 → (𝑀‘𝑍) ∈ 𝑃) |
44 | 43 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → (𝑀‘𝑍) ∈ 𝑃) |
45 | 12 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → 𝑌 ∈ 𝑃) |
46 | | mirbtwnhl.1 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≠ 𝐴) |
47 | 46 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → 𝑋 ≠ 𝐴) |
48 | 30 | ad2antrr 717 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → 𝑍 ∈ 𝑃) |
49 | 1, 2, 3, 30, 5, 4,
6 | ishlg 25921 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑍(𝐾‘𝐴)𝑋 ↔ (𝑍 ≠ 𝐴 ∧ 𝑋 ≠ 𝐴 ∧ (𝑍 ∈ (𝐴𝐼𝑋) ∨ 𝑋 ∈ (𝐴𝐼𝑍))))) |
50 | 49 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑍 ≠ 𝐴) → (𝑍(𝐾‘𝐴)𝑋 ↔ (𝑍 ≠ 𝐴 ∧ 𝑋 ≠ 𝐴 ∧ (𝑍 ∈ (𝐴𝐼𝑋) ∨ 𝑋 ∈ (𝐴𝐼𝑍))))) |
51 | 50 | biimpa 470 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → (𝑍 ≠ 𝐴 ∧ 𝑋 ≠ 𝐴 ∧ (𝑍 ∈ (𝐴𝐼𝑋) ∨ 𝑋 ∈ (𝐴𝐼𝑍)))) |
52 | 51 | simp3d 1178 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → (𝑍 ∈ (𝐴𝐼𝑋) ∨ 𝑋 ∈ (𝐴𝐼𝑍))) |
53 | 52 | orcomd 902 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → (𝑋 ∈ (𝐴𝐼𝑍) ∨ 𝑍 ∈ (𝐴𝐼𝑋))) |
54 | 1, 16, 2, 17, 18, 40, 19, 42, 41, 48, 53 | mirconn 25997 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → 𝐴 ∈ (𝑋𝐼(𝑀‘𝑍))) |
55 | | mirbtwnhl.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝑌)) |
56 | 55 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → 𝐴 ∈ (𝑋𝐼𝑌)) |
57 | 1, 2, 40, 41, 42, 44, 45, 47, 54, 56 | tgbtwnconn2 25895 |
. . . . 5
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → ((𝑀‘𝑍) ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼(𝑀‘𝑍)))) |
58 | 37, 39, 57 | 3jca 1162 |
. . . 4
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → ((𝑀‘𝑍) ≠ 𝐴 ∧ 𝑌 ≠ 𝐴 ∧ ((𝑀‘𝑍) ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼(𝑀‘𝑍))))) |
59 | 1, 2, 3, 43, 12, 4, 6 | ishlg 25921 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘𝑍)(𝐾‘𝐴)𝑌 ↔ ((𝑀‘𝑍) ≠ 𝐴 ∧ 𝑌 ≠ 𝐴 ∧ ((𝑀‘𝑍) ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼(𝑀‘𝑍)))))) |
60 | 59 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑍 ≠ 𝐴) → ((𝑀‘𝑍)(𝐾‘𝐴)𝑌 ↔ ((𝑀‘𝑍) ≠ 𝐴 ∧ 𝑌 ≠ 𝐴 ∧ ((𝑀‘𝑍) ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼(𝑀‘𝑍)))))) |
61 | 60 | adantr 474 |
. . . 4
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → ((𝑀‘𝑍)(𝐾‘𝐴)𝑌 ↔ ((𝑀‘𝑍) ≠ 𝐴 ∧ 𝑌 ≠ 𝐴 ∧ ((𝑀‘𝑍) ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼(𝑀‘𝑍)))))) |
62 | 58, 61 | mpbird 249 |
. . 3
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ 𝑍(𝐾‘𝐴)𝑋) → (𝑀‘𝑍)(𝐾‘𝐴)𝑌) |
63 | | simplr 785 |
. . . . 5
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝑍 ≠ 𝐴) |
64 | 46 | ad2antrr 717 |
. . . . 5
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝑋 ≠ 𝐴) |
65 | 6 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝐺 ∈ TarskiG) |
66 | 12 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝑌 ∈ 𝑃) |
67 | 4 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝐴 ∈ 𝑃) |
68 | 30 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝑍 ∈ 𝑃) |
69 | 5 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝑋 ∈ 𝑃) |
70 | 38 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝑌 ≠ 𝐴) |
71 | 20 | ad2antrr 717 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → (𝑀‘𝐴) = 𝐴) |
72 | 43 | ad2antrr 717 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → (𝑀‘𝑍) ∈ 𝑃) |
73 | 1, 16, 2, 17, 18, 65, 67, 19, 66 | mircl 25980 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → (𝑀‘𝑌) ∈ 𝑃) |
74 | 60 | biimpa 470 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → ((𝑀‘𝑍) ≠ 𝐴 ∧ 𝑌 ≠ 𝐴 ∧ ((𝑀‘𝑍) ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼(𝑀‘𝑍))))) |
75 | 74 | simp3d 1178 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → ((𝑀‘𝑍) ∈ (𝐴𝐼𝑌) ∨ 𝑌 ∈ (𝐴𝐼(𝑀‘𝑍)))) |
76 | 1, 16, 2, 17, 18, 65, 19, 67, 72, 66, 75 | mirconn 25997 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝐴 ∈ ((𝑀‘𝑍)𝐼(𝑀‘𝑌))) |
77 | 1, 16, 2, 65, 72, 67, 73, 76 | tgbtwncom 25807 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝐴 ∈ ((𝑀‘𝑌)𝐼(𝑀‘𝑍))) |
78 | 71, 77 | eqeltrd 2906 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → (𝑀‘𝐴) ∈ ((𝑀‘𝑌)𝐼(𝑀‘𝑍))) |
79 | 1, 16, 2, 17, 18, 65, 67, 19, 66, 67, 68 | mirbtwnb 25991 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → (𝐴 ∈ (𝑌𝐼𝑍) ↔ (𝑀‘𝐴) ∈ ((𝑀‘𝑌)𝐼(𝑀‘𝑍)))) |
80 | 78, 79 | mpbird 249 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝐴 ∈ (𝑌𝐼𝑍)) |
81 | 1, 16, 2, 6, 5, 4, 12, 55 | tgbtwncom 25807 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝑌𝐼𝑋)) |
82 | 81 | ad2antrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝐴 ∈ (𝑌𝐼𝑋)) |
83 | 1, 2, 65, 66, 67, 68, 69, 70, 80, 82 | tgbtwnconn2 25895 |
. . . . 5
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → (𝑍 ∈ (𝐴𝐼𝑋) ∨ 𝑋 ∈ (𝐴𝐼𝑍))) |
84 | 63, 64, 83 | 3jca 1162 |
. . . 4
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → (𝑍 ≠ 𝐴 ∧ 𝑋 ≠ 𝐴 ∧ (𝑍 ∈ (𝐴𝐼𝑋) ∨ 𝑋 ∈ (𝐴𝐼𝑍)))) |
85 | 50 | adantr 474 |
. . . 4
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → (𝑍(𝐾‘𝐴)𝑋 ↔ (𝑍 ≠ 𝐴 ∧ 𝑋 ≠ 𝐴 ∧ (𝑍 ∈ (𝐴𝐼𝑋) ∨ 𝑋 ∈ (𝐴𝐼𝑍))))) |
86 | 84, 85 | mpbird 249 |
. . 3
⊢ (((𝜑 ∧ 𝑍 ≠ 𝐴) ∧ (𝑀‘𝑍)(𝐾‘𝐴)𝑌) → 𝑍(𝐾‘𝐴)𝑋) |
87 | 62, 86 | impbida 835 |
. 2
⊢ ((𝜑 ∧ 𝑍 ≠ 𝐴) → (𝑍(𝐾‘𝐴)𝑋 ↔ (𝑀‘𝑍)(𝐾‘𝐴)𝑌)) |
88 | 25, 87 | pm2.61dane 3086 |
1
⊢ (𝜑 → (𝑍(𝐾‘𝐴)𝑋 ↔ (𝑀‘𝑍)(𝐾‘𝐴)𝑌)) |