MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgelrnln Structured version   Visualization version   GIF version

Theorem tgelrnln 27281
Description: The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019.)
Hypotheses
Ref Expression
tglineelsb2.p 𝐵 = (Base‘𝐺)
tglineelsb2.i 𝐼 = (Itv‘𝐺)
tglineelsb2.l 𝐿 = (LineG‘𝐺)
tglineelsb2.g (𝜑𝐺 ∈ TarskiG)
tgelrnln.x (𝜑𝑋𝐵)
tgelrnln.y (𝜑𝑌𝐵)
tgelrnln.d (𝜑𝑋𝑌)
Assertion
Ref Expression
tgelrnln (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)

Proof of Theorem tgelrnln
StepHypRef Expression
1 df-ov 7341 . 2 (𝑋𝐿𝑌) = (𝐿‘⟨𝑋, 𝑌⟩)
2 tglineelsb2.g . . . 4 (𝜑𝐺 ∈ TarskiG)
3 tglineelsb2.p . . . . 5 𝐵 = (Base‘𝐺)
4 tglineelsb2.l . . . . 5 𝐿 = (LineG‘𝐺)
5 tglineelsb2.i . . . . 5 𝐼 = (Itv‘𝐺)
63, 4, 5tglnfn 27198 . . . 4 (𝐺 ∈ TarskiG → 𝐿 Fn ((𝐵 × 𝐵) ∖ I ))
72, 6syl 17 . . 3 (𝜑𝐿 Fn ((𝐵 × 𝐵) ∖ I ))
8 tgelrnln.x . . . . 5 (𝜑𝑋𝐵)
9 tgelrnln.y . . . . 5 (𝜑𝑌𝐵)
108, 9opelxpd 5659 . . . 4 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
11 tgelrnln.d . . . . 5 (𝜑𝑋𝑌)
12 df-br 5094 . . . . . . . 8 (𝑋 I 𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ I )
13 ideqg 5794 . . . . . . . 8 (𝑌𝐵 → (𝑋 I 𝑌𝑋 = 𝑌))
1412, 13bitr3id 284 . . . . . . 7 (𝑌𝐵 → (⟨𝑋, 𝑌⟩ ∈ I ↔ 𝑋 = 𝑌))
1514necon3bbid 2978 . . . . . 6 (𝑌𝐵 → (¬ ⟨𝑋, 𝑌⟩ ∈ I ↔ 𝑋𝑌))
1615biimpar 478 . . . . 5 ((𝑌𝐵𝑋𝑌) → ¬ ⟨𝑋, 𝑌⟩ ∈ I )
179, 11, 16syl2anc 584 . . . 4 (𝜑 → ¬ ⟨𝑋, 𝑌⟩ ∈ I )
1810, 17eldifd 3909 . . 3 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((𝐵 × 𝐵) ∖ I ))
19 fnfvelrn 7015 . . 3 ((𝐿 Fn ((𝐵 × 𝐵) ∖ I ) ∧ ⟨𝑋, 𝑌⟩ ∈ ((𝐵 × 𝐵) ∖ I )) → (𝐿‘⟨𝑋, 𝑌⟩) ∈ ran 𝐿)
207, 18, 19syl2anc 584 . 2 (𝜑 → (𝐿‘⟨𝑋, 𝑌⟩) ∈ ran 𝐿)
211, 20eqeltrid 2841 1 (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1540  wcel 2105  wne 2940  cdif 3895  cop 4580   class class class wbr 5093   I cid 5518   × cxp 5619  ran crn 5622   Fn wfn 6475  cfv 6480  (class class class)co 7338  Basecbs 17010  TarskiGcstrkg 27078  Itvcitv 27084  LineGclng 27085
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pr 5373  ax-un 7651
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-id 5519  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-fv 6488  df-ov 7341  df-oprab 7342  df-mpo 7343  df-1st 7900  df-2nd 7901  df-trkg 27104
This theorem is referenced by:  tghilberti1  27288  tglineinteq  27296  colline  27300  tglowdim2ln  27302  footexALT  27369  footexlem2  27371  foot  27373  perprag  27377  colperpexlem3  27383  mideulem2  27385  midex  27388  outpasch  27406  lnopp2hpgb  27414  colopp  27420  lmieu  27435  lmimid  27445  hypcgrlem1  27450  hypcgrlem2  27451  lnperpex  27454  trgcopy  27455  trgcopyeulem  27456  acopy  27484  acopyeu  27485  tgasa1  27509
  Copyright terms: Public domain W3C validator