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. = ( 0g ` Y )
prjcrv0.p 
|- P = ( N PrjSpn K )
prjcrv0.n 
|- ( ph -> N e. NN0 )
prjcrv0.k 
|- ( ph -> K e. Field )
Assertion prjcrv0 
|- ( ph -> ( ( N PrjCrv K ) ` .0. ) = P )

Proof

Step Hyp Ref Expression
1 prjcrv0.y 
 |-  Y = ( ( 0 ... N ) mPoly K )
2 prjcrv0.0 
 |-  .0. = ( 0g ` Y )
3 prjcrv0.p 
 |-  P = ( N PrjSpn K )
4 prjcrv0.n 
 |-  ( ph -> N e. NN0 )
5 prjcrv0.k 
 |-  ( ph -> K e. Field )
6 eqid 
 |-  ( ( 0 ... N ) mHomP K ) = ( ( 0 ... N ) mHomP K )
7 eqid 
 |-  ( ( 0 ... N ) eval K ) = ( ( 0 ... N ) eval K )
8 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
9 funmpt 
 |-  Fun ( n e. NN0 |-> { f e. ( Base ` Y ) | ( f supp ( 0g ` K ) ) C_ { g e. { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } } )
10 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
11 eqid 
 |-  { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin }
12 ovexd 
 |-  ( ph -> ( 0 ... N ) e. _V )
13 6 1 10 8 11 12 5 mhpfval 
 |-  ( ph -> ( ( 0 ... N ) mHomP K ) = ( n e. NN0 |-> { f e. ( Base ` Y ) | ( f supp ( 0g ` K ) ) C_ { g e. { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )
14 13 funeqd 
 |-  ( ph -> ( Fun ( ( 0 ... N ) mHomP K ) <-> Fun ( n e. NN0 |-> { f e. ( Base ` Y ) | ( f supp ( 0g ` K ) ) C_ { g e. { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) ) )
15 9 14 mpbiri 
 |-  ( ph -> Fun ( ( 0 ... N ) mHomP K ) )
16 5 fldcrngd 
 |-  ( ph -> K e. CRing )
17 16 crnggrpd 
 |-  ( ph -> K e. Grp )
18 1 11 8 2 12 17 mpl0 
 |-  ( ph -> .0. = ( { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin } X. { ( 0g ` K ) } ) )
19 0nn0 
 |-  0 e. NN0
20 19 a1i 
 |-  ( ph -> 0 e. NN0 )
21 6 8 11 12 17 20 mhp0cl 
 |-  ( ph -> ( { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin } X. { ( 0g ` K ) } ) e. ( ( ( 0 ... N ) mHomP K ) ` 0 ) )
22 18 21 eqeltrd 
 |-  ( ph -> .0. e. ( ( ( 0 ... N ) mHomP K ) ` 0 ) )
23 elunirn2 
 |-  ( ( Fun ( ( 0 ... N ) mHomP K ) /\ .0. e. ( ( ( 0 ... N ) mHomP K ) ` 0 ) ) -> .0. e. U. ran ( ( 0 ... N ) mHomP K ) )
24 15 22 23 syl2anc 
 |-  ( ph -> .0. e. U. ran ( ( 0 ... N ) mHomP K ) )
25 6 7 3 8 4 5 24 prjcrvval 
 |-  ( ph -> ( ( N PrjCrv K ) ` .0. ) = { p e. P | ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = { ( 0g ` K ) } } )
26 eqid 
 |-  ( Base ` K ) = ( Base ` K )
27 ovexd 
 |-  ( ( ph /\ p e. P ) -> ( 0 ... N ) e. _V )
28 16 adantr 
 |-  ( ( ph /\ p e. P ) -> K e. CRing )
29 7 26 1 8 2 27 28 evl0 
 |-  ( ( ph /\ p e. P ) -> ( ( ( 0 ... N ) eval K ) ` .0. ) = ( ( ( Base ` K ) ^m ( 0 ... N ) ) X. { ( 0g ` K ) } ) )
30 29 imaeq1d 
 |-  ( ( ph /\ p e. P ) -> ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = ( ( ( ( Base ` K ) ^m ( 0 ... N ) ) X. { ( 0g ` K ) } ) " p ) )
31 3 eleq2i 
 |-  ( p e. P <-> p e. ( N PrjSpn K ) )
32 31 biimpi 
 |-  ( p e. P -> p e. ( N PrjSpn K ) )
33 32 adantl 
 |-  ( ( ph /\ p e. P ) -> p e. ( N PrjSpn K ) )
34 4 adantr 
 |-  ( ( ph /\ p e. P ) -> N e. NN0 )
35 isfld 
 |-  ( K e. Field <-> ( K e. DivRing /\ K e. CRing ) )
36 35 simplbi 
 |-  ( K e. Field -> K e. DivRing )
37 5 36 syl 
 |-  ( ph -> K e. DivRing )
38 37 adantr 
 |-  ( ( ph /\ p e. P ) -> K e. DivRing )
39 prjspnval 
 |-  ( ( N e. NN0 /\ K e. DivRing ) -> ( N PrjSpn K ) = ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) )
40 34 38 39 syl2anc 
 |-  ( ( ph /\ p e. P ) -> ( N PrjSpn K ) = ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) )
41 eqid 
 |-  ( K freeLMod ( 0 ... N ) ) = ( K freeLMod ( 0 ... N ) )
42 41 frlmlvec 
 |-  ( ( K e. DivRing /\ ( 0 ... N ) e. _V ) -> ( K freeLMod ( 0 ... N ) ) e. LVec )
43 37 12 42 syl2anc 
 |-  ( ph -> ( K freeLMod ( 0 ... N ) ) e. LVec )
44 43 adantr 
 |-  ( ( ph /\ p e. P ) -> ( K freeLMod ( 0 ... N ) ) e. LVec )
45 eqid 
 |-  ( 0g ` ( K freeLMod ( 0 ... N ) ) ) = ( 0g ` ( K freeLMod ( 0 ... N ) ) )
46 eqid 
 |-  ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) = ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } )
47 eqid 
 |-  ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) = ( LSpan ` ( K freeLMod ( 0 ... N ) ) )
48 45 46 47 prjspval2 
 |-  ( ( K freeLMod ( 0 ... N ) ) e. LVec -> ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) = U_ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } )
49 44 48 syl 
 |-  ( ( ph /\ p e. P ) -> ( PrjSp ` ( K freeLMod ( 0 ... N ) ) ) = U_ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } )
50 40 49 eqtrd 
 |-  ( ( ph /\ p e. P ) -> ( N PrjSpn K ) = U_ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } )
51 33 50 eleqtrd 
 |-  ( ( ph /\ p e. P ) -> p e. U_ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } )
52 eliun 
 |-  ( p e. U_ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } <-> E. a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) p e. { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } )
53 51 52 sylib 
 |-  ( ( ph /\ p e. P ) -> E. a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) p e. { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } )
54 eqid 
 |-  { k e. ( ( Base ` K ) ^m ( 0 ... N ) ) | k finSupp ( 0g ` K ) } = { k e. ( ( Base ` K ) ^m ( 0 ... N ) ) | k finSupp ( 0g ` K ) }
55 41 26 8 54 frlmbas 
 |-  ( ( K e. Field /\ ( 0 ... N ) e. _V ) -> { k e. ( ( Base ` K ) ^m ( 0 ... N ) ) | k finSupp ( 0g ` K ) } = ( Base ` ( K freeLMod ( 0 ... N ) ) ) )
56 5 12 55 syl2anc 
 |-  ( ph -> { k e. ( ( Base ` K ) ^m ( 0 ... N ) ) | k finSupp ( 0g ` K ) } = ( Base ` ( K freeLMod ( 0 ... N ) ) ) )
57 ssrab2 
 |-  { k e. ( ( Base ` K ) ^m ( 0 ... N ) ) | k finSupp ( 0g ` K ) } C_ ( ( Base ` K ) ^m ( 0 ... N ) )
58 56 57 eqsstrrdi 
 |-  ( ph -> ( Base ` ( K freeLMod ( 0 ... N ) ) ) C_ ( ( Base ` K ) ^m ( 0 ... N ) ) )
59 58 ad2antrr 
 |-  ( ( ( ph /\ p e. P ) /\ ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) /\ p e. { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } ) ) -> ( Base ` ( K freeLMod ( 0 ... N ) ) ) C_ ( ( Base ` K ) ^m ( 0 ... N ) ) )
60 eldifi 
 |-  ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) -> a e. ( Base ` ( K freeLMod ( 0 ... N ) ) ) )
61 60 adantl 
 |-  ( ( ( ph /\ p e. P ) /\ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) ) -> a e. ( Base ` ( K freeLMod ( 0 ... N ) ) ) )
62 61 adantrr 
 |-  ( ( ( ph /\ p e. P ) /\ ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) /\ p e. { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } ) ) -> a e. ( Base ` ( K freeLMod ( 0 ... N ) ) ) )
63 59 62 sseldd 
 |-  ( ( ( ph /\ p e. P ) /\ ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) /\ p e. { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } ) ) -> a e. ( ( Base ` K ) ^m ( 0 ... N ) ) )
64 velsn 
 |-  ( p e. { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } <-> p = ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) )
65 64 anbi2i 
 |-  ( ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) /\ p e. { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } ) <-> ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) /\ p = ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) ) )
66 43 lveclmodd 
 |-  ( ph -> ( K freeLMod ( 0 ... N ) ) e. LMod )
67 66 ad2antrr 
 |-  ( ( ( ph /\ p e. P ) /\ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) ) -> ( K freeLMod ( 0 ... N ) ) e. LMod )
68 eqid 
 |-  ( Base ` ( K freeLMod ( 0 ... N ) ) ) = ( Base ` ( K freeLMod ( 0 ... N ) ) )
69 68 47 lspsnid 
 |-  ( ( ( K freeLMod ( 0 ... N ) ) e. LMod /\ a e. ( Base ` ( K freeLMod ( 0 ... N ) ) ) ) -> a e. ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) )
70 67 61 69 syl2anc 
 |-  ( ( ( ph /\ p e. P ) /\ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) ) -> a e. ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) )
71 eldifn 
 |-  ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) -> -. a e. { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } )
72 71 adantl 
 |-  ( ( ( ph /\ p e. P ) /\ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) ) -> -. a e. { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } )
73 70 72 eldifd 
 |-  ( ( ( ph /\ p e. P ) /\ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) ) -> a e. ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) )
74 eleq2 
 |-  ( p = ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) -> ( a e. p <-> a e. ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) ) )
75 73 74 syl5ibrcom 
 |-  ( ( ( ph /\ p e. P ) /\ a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) ) -> ( p = ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) -> a e. p ) )
76 75 impr 
 |-  ( ( ( ph /\ p e. P ) /\ ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) /\ p = ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) ) ) -> a e. p )
77 65 76 sylan2b 
 |-  ( ( ( ph /\ p e. P ) /\ ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) /\ p e. { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } ) ) -> a e. p )
78 63 77 elind 
 |-  ( ( ( ph /\ p e. P ) /\ ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) /\ p e. { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } ) ) -> a e. ( ( ( Base ` K ) ^m ( 0 ... N ) ) i^i p ) )
79 78 ne0d 
 |-  ( ( ( ph /\ p e. P ) /\ ( a e. ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) /\ p e. { ( ( ( LSpan ` ( K freeLMod ( 0 ... N ) ) ) ` { a } ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) } ) ) -> ( ( ( Base ` K ) ^m ( 0 ... N ) ) i^i p ) =/= (/) )
80 53 79 rexlimddv 
 |-  ( ( ph /\ p e. P ) -> ( ( ( Base ` K ) ^m ( 0 ... N ) ) i^i p ) =/= (/) )
81 xpima2 
 |-  ( ( ( ( Base ` K ) ^m ( 0 ... N ) ) i^i p ) =/= (/) -> ( ( ( ( Base ` K ) ^m ( 0 ... N ) ) X. { ( 0g ` K ) } ) " p ) = { ( 0g ` K ) } )
82 80 81 syl 
 |-  ( ( ph /\ p e. P ) -> ( ( ( ( Base ` K ) ^m ( 0 ... N ) ) X. { ( 0g ` K ) } ) " p ) = { ( 0g ` K ) } )
83 30 82 eqtrd 
 |-  ( ( ph /\ p e. P ) -> ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = { ( 0g ` K ) } )
84 83 rabeqcda 
 |-  ( ph -> { p e. P | ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = { ( 0g ` K ) } } = P )
85 25 84 eqtrd 
 |-  ( ph -> ( ( N PrjCrv K ) ` .0. ) = P )