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

Theorem tglowdim2ln 27148
Description: There is always one point outside of any line. Theorem 6.25 of [Schwabhauser] p. 46. (Contributed by Thierry Arnoux, 16-Nov-2019.)
Hypotheses
Ref Expression
tglineintmo.p 𝑃 = (Base‘𝐺)
tglineintmo.i 𝐼 = (Itv‘𝐺)
tglineintmo.l 𝐿 = (LineG‘𝐺)
tglineintmo.g (𝜑𝐺 ∈ TarskiG)
tglowdim2l.1 (𝜑𝐺DimTarskiG≥2)
tglowdim2ln.a (𝜑𝐴𝑃)
tglowdim2ln.b (𝜑𝐵𝑃)
tglowdim2ln.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
tglowdim2ln (𝜑 → ∃𝑐𝑃 ¬ 𝑐 ∈ (𝐴𝐿𝐵))
Distinct variable groups:   𝐺,𝑐   𝐼,𝑐   𝑃,𝑐   𝜑,𝑐   𝐴,𝑐   𝐵,𝑐   𝐿,𝑐

Proof of Theorem tglowdim2ln
Dummy variables 𝑎 𝑏 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tglineintmo.p . . . . 5 𝑃 = (Base‘𝐺)
2 tglineintmo.i . . . . 5 𝐼 = (Itv‘𝐺)
3 tglineintmo.l . . . . 5 𝐿 = (LineG‘𝐺)
4 tglineintmo.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
5 tglowdim2l.1 . . . . 5 (𝜑𝐺DimTarskiG≥2)
61, 2, 3, 4, 5tglowdim2l 27147 . . . 4 (𝜑 → ∃𝑎𝑃𝑏𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
76adantr 481 . . 3 ((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) → ∃𝑎𝑃𝑏𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
8 eleq1w 2820 . . . . . . . . . 10 (𝑐 = 𝑧 → (𝑐 ∈ (𝐴𝐿𝐵) ↔ 𝑧 ∈ (𝐴𝐿𝐵)))
9 simpllr 773 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵))
10 simplr3 1216 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝑧𝑃)
118, 9, 10rspcdva 3571 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝑧 ∈ (𝐴𝐿𝐵))
124ad3antrrr 727 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝐺 ∈ TarskiG)
13 simplr1 1214 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝑎𝑃)
14 simplr2 1215 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝑏𝑃)
15 simpr 485 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → ¬ 𝑎 = 𝑏)
1615neqned 2948 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝑎𝑏)
17 tglowdim2ln.a . . . . . . . . . . . 12 (𝜑𝐴𝑃)
1817ad3antrrr 727 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝐴𝑃)
19 tglowdim2ln.b . . . . . . . . . . . 12 (𝜑𝐵𝑃)
2019ad3antrrr 727 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝐵𝑃)
21 tglowdim2ln.1 . . . . . . . . . . . 12 (𝜑𝐴𝐵)
2221ad3antrrr 727 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝐴𝐵)
231, 2, 3, 12, 18, 20, 22tgelrnln 27127 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → (𝐴𝐿𝐵) ∈ ran 𝐿)
24 eleq1w 2820 . . . . . . . . . . 11 (𝑐 = 𝑎 → (𝑐 ∈ (𝐴𝐿𝐵) ↔ 𝑎 ∈ (𝐴𝐿𝐵)))
2524, 9, 13rspcdva 3571 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝑎 ∈ (𝐴𝐿𝐵))
26 eleq1w 2820 . . . . . . . . . . 11 (𝑐 = 𝑏 → (𝑐 ∈ (𝐴𝐿𝐵) ↔ 𝑏 ∈ (𝐴𝐿𝐵)))
2726, 9, 14rspcdva 3571 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝑏 ∈ (𝐴𝐿𝐵))
281, 2, 3, 12, 13, 14, 16, 16, 23, 25, 27tglinethru 27133 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → (𝐴𝐿𝐵) = (𝑎𝐿𝑏))
2911, 28eleqtrd 2840 . . . . . . . 8 ((((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) ∧ ¬ 𝑎 = 𝑏) → 𝑧 ∈ (𝑎𝐿𝑏))
3029ex 413 . . . . . . 7 (((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) → (¬ 𝑎 = 𝑏𝑧 ∈ (𝑎𝐿𝑏)))
3130orrd 860 . . . . . 6 (((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) → (𝑎 = 𝑏𝑧 ∈ (𝑎𝐿𝑏)))
3231orcomd 868 . . . . 5 (((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) ∧ (𝑎𝑃𝑏𝑃𝑧𝑃)) → (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
3332ralrimivvva 3197 . . . 4 ((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
34 dfral2 3099 . . . . . . . 8 (∀𝑧𝑃 (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏) ↔ ¬ ∃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
3534ralbii 3093 . . . . . . 7 (∀𝑏𝑃𝑧𝑃 (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏) ↔ ∀𝑏𝑃 ¬ ∃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
36 ralnex 3073 . . . . . . 7 (∀𝑏𝑃 ¬ ∃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏) ↔ ¬ ∃𝑏𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
3735, 36bitri 274 . . . . . 6 (∀𝑏𝑃𝑧𝑃 (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏) ↔ ¬ ∃𝑏𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
3837ralbii 3093 . . . . 5 (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏) ↔ ∀𝑎𝑃 ¬ ∃𝑏𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
39 ralnex 3073 . . . . 5 (∀𝑎𝑃 ¬ ∃𝑏𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏) ↔ ¬ ∃𝑎𝑃𝑏𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
4038, 39bitri 274 . . . 4 (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏) ↔ ¬ ∃𝑎𝑃𝑏𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
4133, 40sylib 217 . . 3 ((𝜑 ∧ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵)) → ¬ ∃𝑎𝑃𝑏𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑎𝐿𝑏) ∨ 𝑎 = 𝑏))
427, 41pm2.65da 814 . 2 (𝜑 → ¬ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵))
43 rexnal 3100 . 2 (∃𝑐𝑃 ¬ 𝑐 ∈ (𝐴𝐿𝐵) ↔ ¬ ∀𝑐𝑃 𝑐 ∈ (𝐴𝐿𝐵))
4442, 43sylibr 233 1 (𝜑 → ∃𝑐𝑃 ¬ 𝑐 ∈ (𝐴𝐿𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 844  w3a 1086   = wceq 1540  wcel 2105  wne 2941  wral 3062  wrex 3071   class class class wbr 5087  cfv 6466  (class class class)co 7317  2c2 12108  Basecbs 16989  TarskiGcstrkg 26924  DimTarskiGcstrkgld 26928  Itvcitv 26930  LineGclng 26931
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 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-om 7760  df-1st 7878  df-2nd 7879  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-oadd 8350  df-er 8548  df-pm 8668  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-dju 9737  df-card 9775  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-nn 12054  df-2 12116  df-3 12117  df-n0 12314  df-xnn0 12386  df-z 12400  df-uz 12663  df-fz 13320  df-fzo 13463  df-hash 14125  df-word 14297  df-concat 14353  df-s1 14380  df-s2 14640  df-s3 14641  df-trkgc 26945  df-trkgb 26946  df-trkgcb 26947  df-trkgld 26949  df-trkg 26950  df-cgrg 27008
This theorem is referenced by:  colperpex  27230  cgrg3col4  27350
  Copyright terms: Public domain W3C validator