Metamath Proof Explorer


Theorem prjcrv0

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

Ref Expression
Hypotheses prjcrv0.y Y = 0 N mPoly K
prjcrv0.0 0 ˙ = 0 Y
prjcrv0.p P = N ℙ𝕣𝕠𝕛 n K
prjcrv0.n φ N 0
prjcrv0.k φ K Field
Assertion prjcrv0 Could not format assertion : No typesetting found for |- ( ph -> ( ( N PrjCrv K ) ` .0. ) = P ) with typecode |-

Proof

Step Hyp Ref Expression
1 prjcrv0.y Y = 0 N mPoly K
2 prjcrv0.0 0 ˙ = 0 Y
3 prjcrv0.p P = N ℙ𝕣𝕠𝕛 n K
4 prjcrv0.n φ N 0
5 prjcrv0.k φ K Field
6 eqid 0 N mHomP K = 0 N mHomP K
7 eqid 0 N eval K = 0 N eval K
8 eqid 0 K = 0 K
9 fvssunirn 0 N mHomP K N ran 0 N mHomP K
10 eqid h 0 0 N | h -1 Fin = h 0 0 N | h -1 Fin
11 ovexd φ 0 N V
12 5 fldcrngd φ K CRing
13 12 crnggrpd φ K Grp
14 1 10 8 2 11 13 mpl0 φ 0 ˙ = h 0 0 N | h -1 Fin × 0 K
15 6 8 10 11 13 4 mhp0cl φ h 0 0 N | h -1 Fin × 0 K 0 N mHomP K N
16 14 15 eqeltrd φ 0 ˙ 0 N mHomP K N
17 9 16 sselid φ 0 ˙ ran 0 N mHomP K
18 6 7 3 8 4 5 17 prjcrvval Could not format ( ph -> ( ( N PrjCrv K ) ` .0. ) = { p e. P | ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = { ( 0g ` K ) } } ) : No typesetting found for |- ( ph -> ( ( N PrjCrv K ) ` .0. ) = { p e. P | ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = { ( 0g ` K ) } } ) with typecode |-
19 eqid Base K = Base K
20 ovexd φ p P 0 N V
21 12 adantr φ p P K CRing
22 7 19 1 8 2 20 21 evl0 φ p P 0 N eval K 0 ˙ = Base K 0 N × 0 K
23 22 imaeq1d φ p P 0 N eval K 0 ˙ p = Base K 0 N × 0 K p
24 eqid K freeLMod 0 N = K freeLMod 0 N
25 eqid Base K freeLMod 0 N 0 K freeLMod 0 N = Base K freeLMod 0 N 0 K freeLMod 0 N
26 5 flddrngd φ K DivRing
27 3 24 25 4 26 prjspnssbas φ P 𝒫 Base K freeLMod 0 N 0 K freeLMod 0 N
28 eqid k Base K 0 N | finSupp 0 K k = k Base K 0 N | finSupp 0 K k
29 24 19 8 28 frlmbas K Field 0 N V k Base K 0 N | finSupp 0 K k = Base K freeLMod 0 N
30 5 11 29 syl2anc φ k Base K 0 N | finSupp 0 K k = Base K freeLMod 0 N
31 ssrab2 k Base K 0 N | finSupp 0 K k Base K 0 N
32 30 31 eqsstrrdi φ Base K freeLMod 0 N Base K 0 N
33 32 ssdifssd φ Base K freeLMod 0 N 0 K freeLMod 0 N Base K 0 N
34 33 sspwd φ 𝒫 Base K freeLMod 0 N 0 K freeLMod 0 N 𝒫 Base K 0 N
35 27 34 sstrd φ P 𝒫 Base K 0 N
36 35 sselda φ p P p 𝒫 Base K 0 N
37 36 elpwid φ p P p Base K 0 N
38 sseqin2 p Base K 0 N Base K 0 N p = p
39 37 38 sylib φ p P Base K 0 N p = p
40 4 adantr φ p P N 0
41 26 adantr φ p P K DivRing
42 simpr φ p P p P
43 3 24 25 40 41 42 prjspnn0 φ p P p
44 39 43 eqnetrd φ p P Base K 0 N p
45 xpima2 Base K 0 N p Base K 0 N × 0 K p = 0 K
46 44 45 syl φ p P Base K 0 N × 0 K p = 0 K
47 23 46 eqtrd φ p P 0 N eval K 0 ˙ p = 0 K
48 47 rabeqcda φ p P | 0 N eval K 0 ˙ p = 0 K = P
49 18 48 eqtrd Could not format ( ph -> ( ( N PrjCrv K ) ` .0. ) = P ) : No typesetting found for |- ( ph -> ( ( N PrjCrv K ) ` .0. ) = P ) with typecode |-