Users' Mathboxes Mathbox for Steven Nguyen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  0prjspn Structured version   Visualization version   GIF version

Theorem 0prjspn 40681
Description: A zero-dimensional projective space has only 1 point. (Contributed by Steven Nguyen, 9-Jun-2023.)
Hypotheses
Ref Expression
0prjspn.w 𝑊 = (𝐾 freeLMod (0...0))
0prjspn.b 𝐵 = ((Base‘𝑊) ∖ {(0g𝑊)})
Assertion
Ref Expression
0prjspn (𝐾 ∈ DivRing → (0ℙ𝕣𝕠𝕛n𝐾) = {𝐵})

Proof of Theorem 0prjspn
Dummy variables 𝑎 𝑏 𝑙 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0nn0 12328 . . 3 0 ∈ ℕ0
2 eqid 2737 . . . 4 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦))}
3 0prjspn.w . . . 4 𝑊 = (𝐾 freeLMod (0...0))
4 0prjspn.b . . . 4 𝐵 = ((Base‘𝑊) ∖ {(0g𝑊)})
5 eqid 2737 . . . 4 (Base‘𝐾) = (Base‘𝐾)
6 eqid 2737 . . . 4 ( ·𝑠𝑊) = ( ·𝑠𝑊)
72, 3, 4, 5, 6prjspnval2 40673 . . 3 ((0 ∈ ℕ0𝐾 ∈ DivRing) → (0ℙ𝕣𝕠𝕛n𝐾) = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦))}))
81, 7mpan 687 . 2 (𝐾 ∈ DivRing → (0ℙ𝕣𝕠𝕛n𝐾) = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦))}))
9 ovex 7350 . . . . . . . 8 (0...0) ∈ V
103frlmsca 21043 . . . . . . . 8 ((𝐾 ∈ DivRing ∧ (0...0) ∈ V) → 𝐾 = (Scalar‘𝑊))
119, 10mpan2 688 . . . . . . 7 (𝐾 ∈ DivRing → 𝐾 = (Scalar‘𝑊))
1211fveq2d 6816 . . . . . 6 (𝐾 ∈ DivRing → (Base‘𝐾) = (Base‘(Scalar‘𝑊)))
1312rexeqdv 3311 . . . . 5 (𝐾 ∈ DivRing → (∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦) ↔ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦)))
1413anbi2d 629 . . . 4 (𝐾 ∈ DivRing → (((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦)) ↔ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))))
1514opabbidv 5153 . . 3 (𝐾 ∈ DivRing → {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))})
1615qseq2d 8605 . 2 (𝐾 ∈ DivRing → (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦))}) = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))}))
173frlmlvec 21051 . . . . . . 7 ((𝐾 ∈ DivRing ∧ (0...0) ∈ V) → 𝑊 ∈ LVec)
189, 17mpan2 688 . . . . . 6 (𝐾 ∈ DivRing → 𝑊 ∈ LVec)
19 lveclmod 20451 . . . . . 6 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
2018, 19syl 17 . . . . 5 (𝐾 ∈ DivRing → 𝑊 ∈ LMod)
2120adantr 481 . . . 4 ((𝐾 ∈ DivRing ∧ (𝑎𝐵𝑏𝐵)) → 𝑊 ∈ LMod)
2215adantr 481 . . . . . 6 ((𝐾 ∈ DivRing ∧ 𝑎𝐵) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))})
23 eqid 2737 . . . . . . 7 ((𝐾 unitVec (0...0))‘0) = ((𝐾 unitVec (0...0))‘0)
242, 4, 6, 5, 3, 230prjspnrel 40680 . . . . . 6 ((𝐾 ∈ DivRing ∧ 𝑎𝐵) → 𝑎{⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0))
2522, 24breqdi 5102 . . . . 5 ((𝐾 ∈ DivRing ∧ 𝑎𝐵) → 𝑎{⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0))
2625adantrr 714 . . . 4 ((𝐾 ∈ DivRing ∧ (𝑎𝐵𝑏𝐵)) → 𝑎{⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0))
2715adantr 481 . . . . . . 7 ((𝐾 ∈ DivRing ∧ 𝑏𝐵) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))})
282, 4, 6, 5, 3, 230prjspnrel 40680 . . . . . . 7 ((𝐾 ∈ DivRing ∧ 𝑏𝐵) → 𝑏{⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·𝑠𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0))
2927, 28breqdi 5102 . . . . . 6 ((𝐾 ∈ DivRing ∧ 𝑏𝐵) → 𝑏{⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0))
30 eqid 2737 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))}
31 eqid 2737 . . . . . . 7 (Scalar‘𝑊) = (Scalar‘𝑊)
32 eqid 2737 . . . . . . 7 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
3330, 4, 31, 6, 32prjspersym 40662 . . . . . 6 ((𝑊 ∈ LVec ∧ 𝑏{⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0)) → ((𝐾 unitVec (0...0))‘0){⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))}𝑏)
3418, 29, 33syl2an2r 682 . . . . 5 ((𝐾 ∈ DivRing ∧ 𝑏𝐵) → ((𝐾 unitVec (0...0))‘0){⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))}𝑏)
3534adantrl 713 . . . 4 ((𝐾 ∈ DivRing ∧ (𝑎𝐵𝑏𝐵)) → ((𝐾 unitVec (0...0))‘0){⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))}𝑏)
3630, 4, 31, 6, 32prjspertr 40660 . . . 4 ((𝑊 ∈ LMod ∧ (𝑎{⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))} ((𝐾 unitVec (0...0))‘0) ∧ ((𝐾 unitVec (0...0))‘0){⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))}𝑏)) → 𝑎{⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))}𝑏)
3721, 26, 35, 36syl12anc 834 . . 3 ((𝐾 ∈ DivRing ∧ (𝑎𝐵𝑏𝐵)) → 𝑎{⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))}𝑏)
3830, 4, 31, 6, 32prjsper 40663 . . . 4 (𝑊 ∈ LVec → {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))} Er 𝐵)
3918, 38syl 17 . . 3 (𝐾 ∈ DivRing → {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))} Er 𝐵)
404, 3, 230prjspnlem 40676 . . 3 (𝐾 ∈ DivRing → ((𝐾 unitVec (0...0))‘0) ∈ 𝐵)
4137, 39, 40qsalrel 40434 . 2 (𝐾 ∈ DivRing → (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐵𝑦𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙( ·𝑠𝑊)𝑦))}) = {𝐵})
428, 16, 413eqtrd 2781 1 (𝐾 ∈ DivRing → (0ℙ𝕣𝕠𝕛n𝐾) = {𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  wrex 3071  Vcvv 3441  cdif 3894  {csn 4571   class class class wbr 5087  {copab 5149  cfv 6466  (class class class)co 7317   Er wer 8545   / cqs 8547  0cc0 10951  0cn0 12313  ...cfz 13319  Basecbs 16989  Scalarcsca 17042   ·𝑠 cvsca 17043  0gc0g 17227  DivRingcdr 20070  LModclmod 20206  LVecclvec 20447   freeLMod cfrlm 21036   unitVec cuvc 21072  ℙ𝕣𝕠𝕛ncprjspn 40669
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-rmo 3350  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-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-of 7575  df-om 7760  df-1st 7878  df-2nd 7879  df-supp 8027  df-tpos 8091  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-er 8548  df-ec 8550  df-qs 8554  df-map 8667  df-ixp 8736  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-fsupp 9206  df-sup 9278  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-4 12118  df-5 12119  df-6 12120  df-7 12121  df-8 12122  df-9 12123  df-n0 12314  df-z 12400  df-dec 12518  df-uz 12663  df-fz 13320  df-struct 16925  df-sets 16942  df-slot 16960  df-ndx 16972  df-base 16990  df-ress 17019  df-plusg 17052  df-mulr 17053  df-sca 17055  df-vsca 17056  df-ip 17057  df-tset 17058  df-ple 17059  df-ds 17061  df-hom 17063  df-cco 17064  df-0g 17229  df-prds 17235  df-pws 17237  df-mgm 18403  df-sgrp 18452  df-mnd 18463  df-grp 18656  df-minusg 18657  df-sbg 18658  df-subg 18828  df-mgp 19796  df-ur 19813  df-ring 19860  df-oppr 19937  df-dvdsr 19958  df-unit 19959  df-invr 19989  df-drng 20072  df-subrg 20104  df-lmod 20208  df-lss 20277  df-lvec 20448  df-sra 20517  df-rgmod 20518  df-nzr 20612  df-dsmm 21022  df-frlm 21037  df-uvc 21073  df-prjsp 40657  df-prjspn 40670
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator