![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tgelrnln | Structured version Visualization version GIF version |
Description: The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019.) |
Ref | Expression |
---|---|
tglineelsb2.p | ⊢ 𝐵 = (Base‘𝐺) |
tglineelsb2.i | ⊢ 𝐼 = (Itv‘𝐺) |
tglineelsb2.l | ⊢ 𝐿 = (LineG‘𝐺) |
tglineelsb2.g | ⊢ (𝜑 → 𝐺 ∈ TarskiG) |
tgelrnln.x | ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
tgelrnln.y | ⊢ (𝜑 → 𝑌 ∈ 𝐵) |
tgelrnln.d | ⊢ (𝜑 → 𝑋 ≠ 𝑌) |
Ref | Expression |
---|---|
tgelrnln | ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ov 7026 | . 2 ⊢ (𝑋𝐿𝑌) = (𝐿‘〈𝑋, 𝑌〉) | |
2 | tglineelsb2.g | . . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG) | |
3 | tglineelsb2.p | . . . . 5 ⊢ 𝐵 = (Base‘𝐺) | |
4 | tglineelsb2.l | . . . . 5 ⊢ 𝐿 = (LineG‘𝐺) | |
5 | tglineelsb2.i | . . . . 5 ⊢ 𝐼 = (Itv‘𝐺) | |
6 | 3, 4, 5 | tglnfn 26019 | . . . 4 ⊢ (𝐺 ∈ TarskiG → 𝐿 Fn ((𝐵 × 𝐵) ∖ I )) |
7 | 2, 6 | syl 17 | . . 3 ⊢ (𝜑 → 𝐿 Fn ((𝐵 × 𝐵) ∖ I )) |
8 | tgelrnln.x | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵) | |
9 | tgelrnln.y | . . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵) | |
10 | 8, 9 | opelxpd 5488 | . . . 4 ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
11 | tgelrnln.d | . . . . 5 ⊢ (𝜑 → 𝑋 ≠ 𝑌) | |
12 | df-br 4969 | . . . . . . . 8 ⊢ (𝑋 I 𝑌 ↔ 〈𝑋, 𝑌〉 ∈ I ) | |
13 | ideqg 5615 | . . . . . . . 8 ⊢ (𝑌 ∈ 𝐵 → (𝑋 I 𝑌 ↔ 𝑋 = 𝑌)) | |
14 | 12, 13 | syl5bbr 286 | . . . . . . 7 ⊢ (𝑌 ∈ 𝐵 → (〈𝑋, 𝑌〉 ∈ I ↔ 𝑋 = 𝑌)) |
15 | 14 | necon3bbid 3023 | . . . . . 6 ⊢ (𝑌 ∈ 𝐵 → (¬ 〈𝑋, 𝑌〉 ∈ I ↔ 𝑋 ≠ 𝑌)) |
16 | 15 | biimpar 478 | . . . . 5 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑋 ≠ 𝑌) → ¬ 〈𝑋, 𝑌〉 ∈ I ) |
17 | 9, 11, 16 | syl2anc 584 | . . . 4 ⊢ (𝜑 → ¬ 〈𝑋, 𝑌〉 ∈ I ) |
18 | 10, 17 | eldifd 3876 | . . 3 ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ ((𝐵 × 𝐵) ∖ I )) |
19 | fnfvelrn 6720 | . . 3 ⊢ ((𝐿 Fn ((𝐵 × 𝐵) ∖ I ) ∧ 〈𝑋, 𝑌〉 ∈ ((𝐵 × 𝐵) ∖ I )) → (𝐿‘〈𝑋, 𝑌〉) ∈ ran 𝐿) | |
20 | 7, 18, 19 | syl2anc 584 | . 2 ⊢ (𝜑 → (𝐿‘〈𝑋, 𝑌〉) ∈ ran 𝐿) |
21 | 1, 20 | syl5eqel 2889 | 1 ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1525 ∈ wcel 2083 ≠ wne 2986 ∖ cdif 3862 〈cop 4484 class class class wbr 4968 I cid 5354 × cxp 5448 ran crn 5451 Fn wfn 6227 ‘cfv 6232 (class class class)co 7023 Basecbs 16316 TarskiGcstrkg 25902 Itvcitv 25908 LineGclng 25909 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-fv 6240 df-ov 7026 df-oprab 7027 df-mpo 7028 df-1st 7552 df-2nd 7553 df-trkg 25925 |
This theorem is referenced by: tghilberti1 26109 tglineinteq 26117 colline 26121 tglowdim2ln 26123 footexALT 26190 footexlem2 26192 foot 26194 perprag 26198 colperpexlem3 26204 mideulem2 26206 midex 26209 outpasch 26227 lnopp2hpgb 26235 colopp 26241 lmieu 26256 lmimid 26266 hypcgrlem1 26271 hypcgrlem2 26272 lnperpex 26275 trgcopy 26276 trgcopyeulem 26277 acopy 26306 acopyeu 26307 tgasa1 26331 |
Copyright terms: Public domain | W3C validator |