prjspnn0 - Mathbox for Steven Nguyen

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

Theorem prjspnn0 43216

Description: A projective point is nonempty. (Contributed by SN, 17-Jan-2025.)

**Hypotheses**
Ref	Expression
prjspnssbas.p	⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛_n𝐾)
prjspnssbas.w	⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))
prjspnssbas.b	⊢ 𝐵 = ((Base‘𝑊) ∖ {(0_g‘𝑊)})
prjspnssbas.n	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
prjspnssbas.k	⊢ (𝜑 → 𝐾 ∈ DivRing)
prjspnn0.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)

**Assertion**
Ref	Expression
prjspnn0	⊢ (𝜑 → 𝐴 ≠ ∅)

Proof of Theorem prjspnn0 Dummy variables 𝑙 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2765	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))}
2		prjspnssbas.w	. . . 4 ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))
3		prjspnssbas.b	. . . 4 ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0_g‘𝑊)})
4		eqid 2765	. . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾)
5		eqid 2765	. . . 4 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
6		prjspnssbas.k	. . . 4 ⊢ (𝜑 → 𝐾 ∈ DivRing)
7	1, 2, 3, 4, 5, 6	prjspner 43213	. . 3 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))} Er 𝐵)
8		erdm 8693	. . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))} Er 𝐵 → dom {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))} = 𝐵)
9	7, 8	syl 18	. 2 ⊢ (𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))} = 𝐵)
10		prjspnn0.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
11		prjspnssbas.p	. . . 4 ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛_n𝐾)
12		prjspnssbas.n	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13	1, 2, 3, 4, 5	prjspnval2 43212	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛_n𝐾) = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))}))
14	12, 6, 13	syl2anc 595	. . . 4 ⊢ (𝜑 → (𝑁ℙ𝕣𝕠𝕛_n𝐾) = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))}))
15	11, 14	eqtrid 2812	. . 3 ⊢ (𝜑 → 𝑃 = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))}))
16	10, 15	eleqtrd 2867	. 2 ⊢ (𝜑 → 𝐴 ∈ (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))}))
17		elqsn0 8770	. 2 ⊢ ((dom {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))} = 𝐵 ∧ 𝐴 ∈ (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘𝐾)𝑥 = (𝑙( ·_𝑠 ‘𝑊)𝑦))})) → 𝐴 ≠ ∅)
18	9, 16, 17	syl2anc 595	1 ⊢ (𝜑 → 𝐴 ≠ ∅)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∃wrex 3089 ∖ cdif 3904 ∅c0 4288 {csn 4585 {copab 5167 dom cdm 5652 ‘cfv 6525 (class class class)co 7400 Er wer 8679 / cqs 8681 0cc0 11088 ℕ₀cn0 12495 ...cfz 13526 Basecbs 17259 ·_𝑠 cvsca 17304 0_gc0g 17482 DivRingcdr 20804 freeLMod cfrlm 21856 ℙ𝕣𝕠𝕛_ncprjspn 43208

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4869 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-tpos 8210 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-er 8682 df-ec 8684 df-qs 8688 df-map 8814 df-ixp 8884 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-sup 9390 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-nn 12225 df-2 12294 df-3 12295 df-4 12296 df-5 12297 df-6 12298 df-7 12299 df-8 12300 df-9 12301 df-n0 12496 df-z 12583 df-dec 12703 df-uz 12854 df-fz 13527 df-struct 17197 df-sets 17214 df-slot 17232 df-ndx 17244 df-base 17260 df-ress 17281 df-plusg 17313 df-mulr 17314 df-sca 17316 df-vsca 17317 df-ip 17318 df-tset 17319 df-ple 17320 df-ds 17322 df-hom 17324 df-cco 17325 df-0g 17484 df-prds 17490 df-pws 17492 df-mgm 18688 df-sgrp 18767 df-mnd 18783 df-grp 18993 df-minusg 18994 df-sbg 18995 df-subg 19180 df-cmn 19843 df-abl 19844 df-mgp 20208 df-rng 20222 df-ur 20255 df-ring 20308 df-oppr 20410 df-dvdsr 20430 df-unit 20431 df-invr 20461 df-subrg 20646 df-drng 20806 df-lmod 20952 df-lss 21022 df-lvec 21193 df-sra 21263 df-rgmod 21264 df-dsmm 21842 df-frlm 21857 df-prjsp 43196 df-prjspn 43209

This theorem is referenced by: prjcrv0 43227

W3C validator