Proof of Theorem lnhl
Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = 𝐵) → 𝐶 = 𝐵) |
2 | | ishlg.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
3 | | eqid 2739 |
. . . . . 6
⊢
(dist‘𝐺) =
(dist‘𝐺) |
4 | | ishlg.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
5 | | hlln.1 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
6 | | ishlg.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
7 | | ishlg.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
8 | 2, 3, 4, 5, 6, 7 | tgbtwntriv2 26609 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐶)) |
9 | 8 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = 𝐵) → 𝐶 ∈ (𝐴𝐼𝐶)) |
10 | 1, 9 | eqeltrrd 2841 |
. . 3
⊢ ((𝜑 ∧ 𝐶 = 𝐵) → 𝐵 ∈ (𝐴𝐼𝐶)) |
11 | 10 | olcd 874 |
. 2
⊢ ((𝜑 ∧ 𝐶 = 𝐵) → (𝐶(𝐾‘𝐵)𝐴 ∨ 𝐵 ∈ (𝐴𝐼𝐶))) |
12 | | lnhl.1 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ (𝐴𝐿𝐵)) |
13 | | lnhl.l |
. . . . . . 7
⊢ 𝐿 = (LineG‘𝐺) |
14 | | ishlg.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
15 | 2, 13, 4, 5, 6, 14,
12 | tglngne 26672 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
16 | 2, 13, 4, 5, 6, 14,
15, 7 | tgellng 26675 |
. . . . . 6
⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))) |
17 | 12, 16 | mpbid 235 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶))) |
18 | | df-3or 1090 |
. . . . 5
⊢ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)) ↔ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶))) |
19 | 17, 18 | sylib 221 |
. . . 4
⊢ (𝜑 → ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶))) |
20 | 19 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶))) |
21 | | ishlg.k |
. . . . . . . 8
⊢ 𝐾 = (hlG‘𝐺) |
22 | 2, 4, 21, 7, 6, 14, 5 | ishlg 26724 |
. . . . . . 7
⊢ (𝜑 → (𝐶(𝐾‘𝐵)𝐴 ↔ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))) |
23 | 22 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → (𝐶(𝐾‘𝐵)𝐴 ↔ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))) |
24 | | df-3an 1091 |
. . . . . 6
⊢ ((𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))) ↔ ((𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))) |
25 | 23, 24 | bitrdi 290 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → (𝐶(𝐾‘𝐵)𝐴 ↔ ((𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))) |
26 | 15 | anim1ci 619 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
27 | 26 | biantrurd 536 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → ((𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)) ↔ ((𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))) |
28 | 5 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → 𝐺 ∈ TarskiG) |
29 | 14 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → 𝐵 ∈ 𝑃) |
30 | 7 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → 𝐶 ∈ 𝑃) |
31 | 6 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → 𝐴 ∈ 𝑃) |
32 | 2, 3, 4, 28, 29, 30, 31 | tgbtwncomb 26611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → (𝐶 ∈ (𝐵𝐼𝐴) ↔ 𝐶 ∈ (𝐴𝐼𝐵))) |
33 | 2, 3, 4, 28, 29, 31, 30 | tgbtwncomb 26611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → (𝐴 ∈ (𝐵𝐼𝐶) ↔ 𝐴 ∈ (𝐶𝐼𝐵))) |
34 | 32, 33 | orbi12d 919 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → ((𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)) ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)))) |
35 | 25, 27, 34 | 3bitr2d 310 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → (𝐶(𝐾‘𝐵)𝐴 ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)))) |
36 | 35 | orbi1d 917 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → ((𝐶(𝐾‘𝐵)𝐴 ∨ 𝐵 ∈ (𝐴𝐼𝐶)) ↔ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))) |
37 | 20, 36 | mpbird 260 |
. 2
⊢ ((𝜑 ∧ 𝐶 ≠ 𝐵) → (𝐶(𝐾‘𝐵)𝐴 ∨ 𝐵 ∈ (𝐴𝐼𝐶))) |
38 | 11, 37 | pm2.61dane 3032 |
1
⊢ (𝜑 → (𝐶(𝐾‘𝐵)𝐴 ∨ 𝐵 ∈ (𝐴𝐼𝐶))) |