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 fvssunirn 
 |-  ( ( ( 0 ... N ) mHomP K ) ` N ) C_ U. ran ( ( 0 ... N ) mHomP K )
10 eqid 
 |-  { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin }
11 ovexd 
 |-  ( ph -> ( 0 ... N ) e. _V )
12 5 fldcrngd 
 |-  ( ph -> K e. CRing )
13 12 crnggrpd 
 |-  ( ph -> K e. Grp )
14 1 10 8 2 11 13 mpl0 
 |-  ( ph -> .0. = ( { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin } X. { ( 0g ` K ) } ) )
15 6 8 10 11 13 4 mhp0cl 
 |-  ( ph -> ( { h e. ( NN0 ^m ( 0 ... N ) ) | ( `' h " NN ) e. Fin } X. { ( 0g ` K ) } ) e. ( ( ( 0 ... N ) mHomP K ) ` N ) )
16 14 15 eqeltrd 
 |-  ( ph -> .0. e. ( ( ( 0 ... N ) mHomP K ) ` N ) )
17 9 16 sselid 
 |-  ( ph -> .0. e. U. ran ( ( 0 ... N ) mHomP K ) )
18 6 7 3 8 4 5 17 prjcrvval 
 |-  ( ph -> ( ( N PrjCrv K ) ` .0. ) = { p e. P | ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = { ( 0g ` K ) } } )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 ovexd 
 |-  ( ( ph /\ p e. P ) -> ( 0 ... N ) e. _V )
21 12 adantr 
 |-  ( ( ph /\ p e. P ) -> K e. CRing )
22 7 19 1 8 2 20 21 evl0 
 |-  ( ( ph /\ p e. P ) -> ( ( ( 0 ... N ) eval K ) ` .0. ) = ( ( ( Base ` K ) ^m ( 0 ... N ) ) X. { ( 0g ` K ) } ) )
23 22 imaeq1d 
 |-  ( ( ph /\ p e. P ) -> ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = ( ( ( ( Base ` K ) ^m ( 0 ... N ) ) X. { ( 0g ` K ) } ) " p ) )
24 eqid 
 |-  ( K freeLMod ( 0 ... N ) ) = ( K freeLMod ( 0 ... N ) )
25 eqid 
 |-  ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) = ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } )
26 5 flddrngd 
 |-  ( ph -> K e. DivRing )
27 3 24 25 4 26 prjspnssbas 
 |-  ( ph -> P C_ ~P ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) )
28 eqid 
 |-  { k e. ( ( Base ` K ) ^m ( 0 ... N ) ) | k finSupp ( 0g ` K ) } = { k e. ( ( Base ` K ) ^m ( 0 ... N ) ) | k finSupp ( 0g ` K ) }
29 24 19 8 28 frlmbas 
 |-  ( ( K e. Field /\ ( 0 ... N ) e. _V ) -> { k e. ( ( Base ` K ) ^m ( 0 ... N ) ) | k finSupp ( 0g ` K ) } = ( Base ` ( K freeLMod ( 0 ... N ) ) ) )
30 5 11 29 syl2anc 
 |-  ( ph -> { k e. ( ( Base ` K ) ^m ( 0 ... N ) ) | k finSupp ( 0g ` K ) } = ( Base ` ( K freeLMod ( 0 ... N ) ) ) )
31 ssrab2 
 |-  { k e. ( ( Base ` K ) ^m ( 0 ... N ) ) | k finSupp ( 0g ` K ) } C_ ( ( Base ` K ) ^m ( 0 ... N ) )
32 30 31 eqsstrrdi 
 |-  ( ph -> ( Base ` ( K freeLMod ( 0 ... N ) ) ) C_ ( ( Base ` K ) ^m ( 0 ... N ) ) )
33 32 ssdifssd 
 |-  ( ph -> ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) C_ ( ( Base ` K ) ^m ( 0 ... N ) ) )
34 33 sspwd 
 |-  ( ph -> ~P ( ( Base ` ( K freeLMod ( 0 ... N ) ) ) \ { ( 0g ` ( K freeLMod ( 0 ... N ) ) ) } ) C_ ~P ( ( Base ` K ) ^m ( 0 ... N ) ) )
35 27 34 sstrd 
 |-  ( ph -> P C_ ~P ( ( Base ` K ) ^m ( 0 ... N ) ) )
36 35 sselda 
 |-  ( ( ph /\ p e. P ) -> p e. ~P ( ( Base ` K ) ^m ( 0 ... N ) ) )
37 36 elpwid 
 |-  ( ( ph /\ p e. P ) -> p C_ ( ( Base ` K ) ^m ( 0 ... N ) ) )
38 sseqin2 
 |-  ( p C_ ( ( Base ` K ) ^m ( 0 ... N ) ) <-> ( ( ( Base ` K ) ^m ( 0 ... N ) ) i^i p ) = p )
39 37 38 sylib 
 |-  ( ( ph /\ p e. P ) -> ( ( ( Base ` K ) ^m ( 0 ... N ) ) i^i p ) = p )
40 4 adantr 
 |-  ( ( ph /\ p e. P ) -> N e. NN0 )
41 26 adantr 
 |-  ( ( ph /\ p e. P ) -> K e. DivRing )
42 simpr 
 |-  ( ( ph /\ p e. P ) -> p e. P )
43 3 24 25 40 41 42 prjspnn0 
 |-  ( ( ph /\ p e. P ) -> p =/= (/) )
44 39 43 eqnetrd 
 |-  ( ( ph /\ p e. P ) -> ( ( ( Base ` K ) ^m ( 0 ... N ) ) i^i p ) =/= (/) )
45 xpima2 
 |-  ( ( ( ( Base ` K ) ^m ( 0 ... N ) ) i^i p ) =/= (/) -> ( ( ( ( Base ` K ) ^m ( 0 ... N ) ) X. { ( 0g ` K ) } ) " p ) = { ( 0g ` K ) } )
46 44 45 syl 
 |-  ( ( ph /\ p e. P ) -> ( ( ( ( Base ` K ) ^m ( 0 ... N ) ) X. { ( 0g ` K ) } ) " p ) = { ( 0g ` K ) } )
47 23 46 eqtrd 
 |-  ( ( ph /\ p e. P ) -> ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = { ( 0g ` K ) } )
48 47 rabeqcda 
 |-  ( ph -> { p e. P | ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = { ( 0g ` K ) } } = P )
49 18 48 eqtrd 
 |-  ( ph -> ( ( N PrjCrv K ) ` .0. ) = P )