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

Theorem tgelrnln 25746
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 6796 . 2 (𝑋𝐿𝑌) = (𝐿‘⟨𝑋, 𝑌⟩)
2 tglineelsb2.g . . . 4 (𝜑𝐺 ∈ TarskiG)
3 tglineelsb2.p . . . . 5 𝐵 = (Base‘𝐺)
4 tglineelsb2.l . . . . 5 𝐿 = (LineG‘𝐺)
5 tglineelsb2.i . . . . 5 𝐼 = (Itv‘𝐺)
63, 4, 5tglnfn 25663 . . . 4 (𝐺 ∈ TarskiG → 𝐿 Fn ((𝐵 × 𝐵) ∖ I ))
72, 6syl 17 . . 3 (𝜑𝐿 Fn ((𝐵 × 𝐵) ∖ I ))
8 tgelrnln.x . . . . 5 (𝜑𝑋𝐵)
9 tgelrnln.y . . . . 5 (𝜑𝑌𝐵)
10 opelxpi 5288 . . . . 5 ((𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
118, 9, 10syl2anc 573 . . . 4 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
12 tgelrnln.d . . . . 5 (𝜑𝑋𝑌)
13 df-br 4787 . . . . . . . 8 (𝑋 I 𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ I )
14 ideqg 5412 . . . . . . . 8 (𝑌𝐵 → (𝑋 I 𝑌𝑋 = 𝑌))
1513, 14syl5bbr 274 . . . . . . 7 (𝑌𝐵 → (⟨𝑋, 𝑌⟩ ∈ I ↔ 𝑋 = 𝑌))
1615necon3bbid 2980 . . . . . 6 (𝑌𝐵 → (¬ ⟨𝑋, 𝑌⟩ ∈ I ↔ 𝑋𝑌))
1716biimpar 463 . . . . 5 ((𝑌𝐵𝑋𝑌) → ¬ ⟨𝑋, 𝑌⟩ ∈ I )
189, 12, 17syl2anc 573 . . . 4 (𝜑 → ¬ ⟨𝑋, 𝑌⟩ ∈ I )
1911, 18eldifd 3734 . . 3 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ ((𝐵 × 𝐵) ∖ I ))
20 fnfvelrn 6499 . . 3 ((𝐿 Fn ((𝐵 × 𝐵) ∖ I ) ∧ ⟨𝑋, 𝑌⟩ ∈ ((𝐵 × 𝐵) ∖ I )) → (𝐿‘⟨𝑋, 𝑌⟩) ∈ ran 𝐿)
217, 19, 20syl2anc 573 . 2 (𝜑 → (𝐿‘⟨𝑋, 𝑌⟩) ∈ ran 𝐿)
221, 21syl5eqel 2854 1 (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1631  wcel 2145  wne 2943  cdif 3720  cop 4322   class class class wbr 4786   I cid 5156   × cxp 5247  ran crn 5250   Fn wfn 6026  cfv 6031  (class class class)co 6793  Basecbs 16064  TarskiGcstrkg 25550  Itvcitv 25556  LineGclng 25557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-1st 7315  df-2nd 7316  df-trkg 25573
This theorem is referenced by:  tghilberti1  25753  tglineinteq  25761  colline  25765  tglowdim2ln  25767  footex  25834  foot  25835  perprag  25839  colperpexlem3  25845  mideulem2  25847  midex  25850  opphllem5  25864  opphllem6  25865  outpasch  25868  lnopp2hpgb  25876  colopp  25882  lmieu  25897  lmimid  25907  hypcgrlem1  25912  hypcgrlem2  25913  lnperpex  25916  trgcopy  25917  trgcopyeulem  25918  acopy  25945  acopyeu  25946  tgasa1  25960
  Copyright terms: Public domain W3C validator