Theorem prjcrv0 42606

Description: The "curve" (zero set) corresponding to the zero polynomial contains all coordinates. (Contributed by SN, 23-Nov-2024.)

Hypotheses

Ref	Expression
prjcrv0.y	⊢ 𝑌 = ((0...𝑁) mPoly 𝐾)
prjcrv0.0	⊢ 0 = (0g‘𝑌)
prjcrv0.p	⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)
prjcrv0.n	⊢ (𝜑 → 𝑁 ∈ ℕ0)
prjcrv0.k	⊢ (𝜑 → 𝐾 ∈ Field)

Assertion

Ref	Expression
prjcrv0	⊢ (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘ 0 ) = 𝑃)

Proof of Theorem prjcrv0

Dummy variables 𝑘 𝑝 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ ((0...𝑁) mHomP 𝐾) = ((0...𝑁) mHomP 𝐾)
2		eqid 2729	. . 3 ⊢ ((0...𝑁) eval 𝐾) = ((0...𝑁) eval 𝐾)
3		prjcrv0.p	. . 3 ⊢ 𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)
4		eqid 2729	. . 3 ⊢ (0g‘𝐾) = (0g‘𝐾)
5		prjcrv0.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
6		prjcrv0.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ Field)
7		fvssunirn 6857	. . . 4 ⊢ (((0...𝑁) mHomP 𝐾)‘𝑁) ⊆ ∪ ran ((0...𝑁) mHomP 𝐾)
8		prjcrv0.y	. . . . . 6 ⊢ 𝑌 = ((0...𝑁) mPoly 𝐾)
9		eqid 2729	. . . . . 6 ⊢ {ℎ ∈ (ℕ0 ↑m (0...𝑁)) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0 ↑m (0...𝑁)) ∣ (◡ℎ “ ℕ) ∈ Fin}
10		prjcrv0.0	. . . . . 6 ⊢ 0 = (0g‘𝑌)
11		ovexd 7388	. . . . . 6 ⊢ (𝜑 → (0...𝑁) ∈ V)
12	6	fldcrngd 20645	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ CRing)
13	12	crnggrpd 20150	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ Grp)
14	8, 9, 4, 10, 11, 13	mpl0 21931	. . . . 5 ⊢ (𝜑 → 0 = ({ℎ ∈ (ℕ0 ↑m (0...𝑁)) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(0g‘𝐾)}))
15	1, 4, 9, 11, 13, 5	mhp0cl 22049	. . . . 5 ⊢ (𝜑 → ({ℎ ∈ (ℕ0 ↑m (0...𝑁)) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(0g‘𝐾)}) ∈ (((0...𝑁) mHomP 𝐾)‘𝑁))
16	14, 15	eqeltrd 2828	. . . 4 ⊢ (𝜑 → 0 ∈ (((0...𝑁) mHomP 𝐾)‘𝑁))
17	7, 16	sselid 3935	. . 3 ⊢ (𝜑 → 0 ∈ ∪ ran ((0...𝑁) mHomP 𝐾))
18	1, 2, 3, 4, 5, 6, 17	prjcrvval 42605	. 2 ⊢ (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘ 0 ) = {𝑝 ∈ 𝑃 ∣ ((((0...𝑁) eval 𝐾)‘ 0 ) “ 𝑝) = {(0g‘𝐾)}})
19		eqid 2729	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
20		ovexd 7388	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → (0...𝑁) ∈ V)
21	12	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝐾 ∈ CRing)
22	2, 19, 8, 4, 10, 20, 21	evl0 42530	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → (((0...𝑁) eval 𝐾)‘ 0 ) = (((Base‘𝐾) ↑m (0...𝑁)) × {(0g‘𝐾)}))
23	22	imaeq1d 6014	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → ((((0...𝑁) eval 𝐾)‘ 0 ) “ 𝑝) = ((((Base‘𝐾) ↑m (0...𝑁)) × {(0g‘𝐾)}) “ 𝑝))
24		eqid 2729	. . . . . . . . . . 11 ⊢ (𝐾 freeLMod (0...𝑁)) = (𝐾 freeLMod (0...𝑁))
25		eqid 2729	. . . . . . . . . . 11 ⊢ ((Base‘(𝐾 freeLMod (0...𝑁))) ∖ {(0g‘(𝐾 freeLMod (0...𝑁)))}) = ((Base‘(𝐾 freeLMod (0...𝑁))) ∖ {(0g‘(𝐾 freeLMod (0...𝑁)))})
26	6	flddrngd 20644	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ DivRing)
27	3, 24, 25, 5, 26	prjspnssbas 42594	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ⊆ 𝒫 ((Base‘(𝐾 freeLMod (0...𝑁))) ∖ {(0g‘(𝐾 freeLMod (0...𝑁)))}))
28		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ {𝑘 ∈ ((Base‘𝐾) ↑m (0...𝑁)) ∣ 𝑘 finSupp (0g‘𝐾)} = {𝑘 ∈ ((Base‘𝐾) ↑m (0...𝑁)) ∣ 𝑘 finSupp (0g‘𝐾)}
29	24, 19, 4, 28	frlmbas 21680	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Field ∧ (0...𝑁) ∈ V) → {𝑘 ∈ ((Base‘𝐾) ↑m (0...𝑁)) ∣ 𝑘 finSupp (0g‘𝐾)} = (Base‘(𝐾 freeLMod (0...𝑁))))
30	6, 11, 29	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑘 ∈ ((Base‘𝐾) ↑m (0...𝑁)) ∣ 𝑘 finSupp (0g‘𝐾)} = (Base‘(𝐾 freeLMod (0...𝑁))))
31		ssrab2 4033	. . . . . . . . . . . . 13 ⊢ {𝑘 ∈ ((Base‘𝐾) ↑m (0...𝑁)) ∣ 𝑘 finSupp (0g‘𝐾)} ⊆ ((Base‘𝐾) ↑m (0...𝑁))
32	30, 31	eqsstrrdi 3983	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘(𝐾 freeLMod (0...𝑁))) ⊆ ((Base‘𝐾) ↑m (0...𝑁)))
33	32	ssdifssd 4100	. . . . . . . . . . 11 ⊢ (𝜑 → ((Base‘(𝐾 freeLMod (0...𝑁))) ∖ {(0g‘(𝐾 freeLMod (0...𝑁)))}) ⊆ ((Base‘𝐾) ↑m (0...𝑁)))
34	33	sspwd 4566	. . . . . . . . . 10 ⊢ (𝜑 → 𝒫 ((Base‘(𝐾 freeLMod (0...𝑁))) ∖ {(0g‘(𝐾 freeLMod (0...𝑁)))}) ⊆ 𝒫 ((Base‘𝐾) ↑m (0...𝑁)))
35	27, 34	sstrd 3948	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ⊆ 𝒫 ((Base‘𝐾) ↑m (0...𝑁)))
36	35	sselda 3937	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝒫 ((Base‘𝐾) ↑m (0...𝑁)))
37	36	elpwid 4562	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ⊆ ((Base‘𝐾) ↑m (0...𝑁)))
38		sseqin2 4176	. . . . . . 7 ⊢ (𝑝 ⊆ ((Base‘𝐾) ↑m (0...𝑁)) ↔ (((Base‘𝐾) ↑m (0...𝑁)) ∩ 𝑝) = 𝑝)
39	37, 38	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → (((Base‘𝐾) ↑m (0...𝑁)) ∩ 𝑝) = 𝑝)
40	5	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑁 ∈ ℕ0)
41	26	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝐾 ∈ DivRing)
42		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
43	3, 24, 25, 40, 41, 42	prjspnn0 42595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → 𝑝 ≠ ∅)
44	39, 43	eqnetrd 2992	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → (((Base‘𝐾) ↑m (0...𝑁)) ∩ 𝑝) ≠ ∅)
45		xpima2 6137	. . . . 5 ⊢ ((((Base‘𝐾) ↑m (0...𝑁)) ∩ 𝑝) ≠ ∅ → ((((Base‘𝐾) ↑m (0...𝑁)) × {(0g‘𝐾)}) “ 𝑝) = {(0g‘𝐾)})
46	44, 45	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → ((((Base‘𝐾) ↑m (0...𝑁)) × {(0g‘𝐾)}) “ 𝑝) = {(0g‘𝐾)})
47	23, 46	eqtrd 2764	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑃) → ((((0...𝑁) eval 𝐾)‘ 0 ) “ 𝑝) = {(0g‘𝐾)})
48	47	rabeqcda 3408	. 2 ⊢ (𝜑 → {𝑝 ∈ 𝑃 ∣ ((((0...𝑁) eval 𝐾)‘ 0 ) “ 𝑝) = {(0g‘𝐾)}} = 𝑃)
49	18, 48	eqtrd 2764	1 ⊢ (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘ 0 ) = 𝑃)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  {crab 3396  Vcvv 3438   ∖ cdif 3902   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  𝒫 cpw 4553  {csn 4579  ∪ cuni 4861   class class class wbr 5095   × cxp 5621  ^◡ccnv 5622  ran crn 5624   “ cima 5626  ‘cfv 6486  (class class class)co 7353   ↑_m cmap 8760  Fincfn 8879   finSupp cfsupp 9270  0cc0 11028  ℕcn 12146  ℕ₀cn0 12402  ...cfz 13428  Basecbs 17138  0_gc0g 17361  CRingccrg 20137  DivRingcdr 20632  Fieldcfield 20633   freeLMod cfrlm 21671   mPoly cmpl 21831   eval cevl 21996   mHomP cmhp 22032  ℙ𝕣𝕠𝕛_ncprjspn 42587  ℙ𝕣𝕠𝕛Crvcprjcrv 42602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-iin 4947  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7617  df-ofr 7618  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-tpos 8166  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8632  df-ec 8634  df-qs 8638  df-map 8762  df-pm 8763  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9271  df-sup 9351  df-oi 9421  df-card 9854  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-nn 12147  df-2 12209  df-3 12210  df-4 12211  df-5 12212  df-6 12213  df-7 12214  df-8 12215  df-9 12216  df-n0 12403  df-z 12490  df-dec 12610  df-uz 12754  df-fz 13429  df-fzo 13576  df-seq 13927  df-hash 14256  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17139  df-ress 17160  df-plusg 17192  df-mulr 17193  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ds 17201  df-hom 17203  df-cco 17204  df-0g 17363  df-gsum 17364  df-prds 17369  df-pws 17371  df-mre 17506  df-mrc 17507  df-acs 17509  df-mgm 18532  df-sgrp 18611  df-mnd 18627  df-mhm 18675  df-submnd 18676  df-grp 18833  df-minusg 18834  df-sbg 18835  df-mulg 18965  df-subg 19020  df-ghm 19110  df-cntz 19214  df-cmn 19679  df-abl 19680  df-mgp 20044  df-rng 20056  df-ur 20085  df-srg 20090  df-ring 20138  df-cring 20139  df-oppr 20240  df-dvdsr 20260  df-unit 20261  df-invr 20291  df-rhm 20375  df-subrng 20449  df-subrg 20473  df-drng 20634  df-field 20635  df-lmod 20783  df-lss 20853  df-lsp 20893  df-lvec 21025  df-sra 21095  df-rgmod 21096  df-dsmm 21657  df-frlm 21672  df-assa 21778  df-asp 21779  df-ascl 21780  df-psr 21834  df-mvr 21835  df-mpl 21836  df-evls 21997  df-evl 21998  df-mhp 22039  df-prjsp 42575  df-prjspn 42588  df-prjcrv 42603

This theorem is referenced by: (None)