| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > hlln | Structured version Visualization version GIF version | ||
| Description: The half-line relation implies colinearity, part of Theorem 6.4 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 22-Feb-2020.) |
| Ref | Expression |
|---|---|
| ishlg.p | ⊢ 𝑃 = (Base‘𝐺) |
| ishlg.i | ⊢ 𝐼 = (Itv‘𝐺) |
| ishlg.k | ⊢ 𝐾 = (hlG‘𝐺) |
| ishlg.a | ⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| ishlg.b | ⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| ishlg.c | ⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| hlln.1 | ⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| hlln.l | ⊢ 𝐿 = (LineG‘𝐺) |
| hlln.2 | ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) |
| Ref | Expression |
|---|---|
| hlln | ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ishlg.p | . . . . 5 ⊢ 𝑃 = (Base‘𝐺) | |
| 2 | eqid 2765 | . . . . 5 ⊢ (dist‘𝐺) = (dist‘𝐺) | |
| 3 | ishlg.i | . . . . 5 ⊢ 𝐼 = (Itv‘𝐺) | |
| 4 | hlln.1 | . . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG) | |
| 5 | 4 | adantr 486 | . . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐺 ∈ TarskiG) |
| 6 | ishlg.c | . . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑃) | |
| 7 | 6 | adantr 486 | . . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐶 ∈ 𝑃) |
| 8 | ishlg.a | . . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑃) | |
| 9 | 8 | adantr 486 | . . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ 𝑃) |
| 10 | ishlg.b | . . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑃) | |
| 11 | 10 | adantr 486 | . . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐵 ∈ 𝑃) |
| 12 | simpr 490 | . . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐶𝐼𝐵)) | |
| 13 | 1, 2, 3, 5, 7, 9, 11, 12 | tgbtwncom 28808 | . . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐵𝐼𝐶)) |
| 14 | 13 | 3mix1d 1355 | . . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → (𝐴 ∈ (𝐵𝐼𝐶) ∨ 𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝐴))) |
| 15 | 4 | adantr 486 | . . . . 5 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐶𝐼𝐴)) → 𝐺 ∈ TarskiG) |
| 16 | 6 | adantr 486 | . . . . 5 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐶𝐼𝐴)) → 𝐶 ∈ 𝑃) |
| 17 | 10 | adantr 486 | . . . . 5 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐶𝐼𝐴)) → 𝐵 ∈ 𝑃) |
| 18 | 8 | adantr 486 | . . . . 5 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐶𝐼𝐴)) → 𝐴 ∈ 𝑃) |
| 19 | simpr 490 | . . . . 5 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐶𝐼𝐴)) → 𝐵 ∈ (𝐶𝐼𝐴)) | |
| 20 | 1, 2, 3, 15, 16, 17, 18, 19 | tgbtwncom 28808 | . . . 4 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐶𝐼𝐴)) → 𝐵 ∈ (𝐴𝐼𝐶)) |
| 21 | 20 | 3mix2d 1356 | . . 3 ⊢ ((𝜑 ∧ 𝐵 ∈ (𝐶𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐶) ∨ 𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝐴))) |
| 22 | hlln.2 | . . . . 5 ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) | |
| 23 | ishlg.k | . . . . . 6 ⊢ 𝐾 = (hlG‘𝐺) | |
| 24 | 1, 3, 23, 8, 10, 6, 4 | ishlg 28925 | . . . . 5 ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))) |
| 25 | 22, 24 | mpbid 235 | . . . 4 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))) |
| 26 | 25 | simp3d 1162 | . . 3 ⊢ (𝜑 → (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))) |
| 27 | 14, 21, 26 | mpjaodan 973 | . 2 ⊢ (𝜑 → (𝐴 ∈ (𝐵𝐼𝐶) ∨ 𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝐴))) |
| 28 | hlln.l | . . 3 ⊢ 𝐿 = (LineG‘𝐺) | |
| 29 | 25 | simp2d 1161 | . . 3 ⊢ (𝜑 → 𝐵 ≠ 𝐶) |
| 30 | 1, 28, 3, 4, 10, 6, 29, 8 | tgellng 28873 | . 2 ⊢ (𝜑 → (𝐴 ∈ (𝐵𝐿𝐶) ↔ (𝐴 ∈ (𝐵𝐼𝐶) ∨ 𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐵𝐼𝐴)))) |
| 31 | 27, 30 | mpbird 260 | 1 ⊢ (𝜑 → 𝐴 ∈ (𝐵𝐿𝐶)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 class class class wbr 5111 ‘cfv 6540 (class class class)co 7419 Basecbs 17291 distcds 17341 TarskiGcstrkg 28747 Itvcitv 28753 LineGclng 28754 hlGchlg 28920 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7422 df-oprab 7423 df-mpo 7424 df-trkgc 28768 df-trkgb 28769 df-trkgcb 28770 df-trkg 28773 df-hlg 28921 |
| This theorem is used by: hlperpnel 29057 opphllem4 29082 opphl 29086 hlpasch 29089 colhp 29103 hphl 29104 trgcopy 29166 cgracgr 29180 cgraswap 29182 acopy 29195 acopyeu 29196 ragcgra 29197 cgrarag 29198 perpeqlem 29201 tgaaddcpbllem1 29203 tgaaddcpbl 29206 tgasa1 29230 tgaltai 29272 |
| Copyright terms: Public domain | W3C validator |