Metamath Proof Explorer

Theorem mhpsclcl

Description: A scalar (or constant) polynomial has degree 0. Compare deg1scl . In other contexts, there may be an exception for the zero polynomial, but under df-mhp the zero polynomial can be any degree (see mhp0cl ) so there is no exception. (Contributed by SN, 25-May-2024)

Ref Expression
Hypotheses mhpsclcl.h 
|- H = ( I mHomP R )
mhpsclcl.p 
|- P = ( I mPoly R )
mhpsclcl.a 
|- A = ( algSc ` P )
mhpsclcl.k 
|- K = ( Base ` R )
mhpsclcl.i 
|- ( ph -> I e. V )
mhpsclcl.r 
|- ( ph -> R e. Ring )
mhpsclcl.c 
|- ( ph -> C e. K )
Assertion mhpsclcl 
|- ( ph -> ( A ` C ) e. ( H ` 0 ) )

Proof

Step Hyp Ref Expression
1 mhpsclcl.h 
 |-  H = ( I mHomP R )
2 mhpsclcl.p 
 |-  P = ( I mPoly R )
3 mhpsclcl.a 
 |-  A = ( algSc ` P )
4 mhpsclcl.k 
 |-  K = ( Base ` R )
5 mhpsclcl.i 
 |-  ( ph -> I e. V )
6 mhpsclcl.r 
 |-  ( ph -> R e. Ring )
7 mhpsclcl.c 
 |-  ( ph -> C e. K )
8 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
9 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
10 5 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> I e. V )
11 6 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. Ring )
12 7 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> C e. K )
13 2 8 9 4 3 10 11 12 mplascl 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( A ` C ) = ( y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( y = ( I X. { 0 } ) , C , ( 0g ` R ) ) ) )
14 eqeq1 
 |-  ( y = d -> ( y = ( I X. { 0 } ) <-> d = ( I X. { 0 } ) ) )
15 14 ifbid 
 |-  ( y = d -> if ( y = ( I X. { 0 } ) , C , ( 0g ` R ) ) = if ( d = ( I X. { 0 } ) , C , ( 0g ` R ) ) )
16 15 adantl 
 |-  ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ y = d ) -> if ( y = ( I X. { 0 } ) , C , ( 0g ` R ) ) = if ( d = ( I X. { 0 } ) , C , ( 0g ` R ) ) )
17 simpr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
18 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
19 7 18 ifexd 
 |-  ( ph -> if ( d = ( I X. { 0 } ) , C , ( 0g ` R ) ) e. _V )
20 19 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> if ( d = ( I X. { 0 } ) , C , ( 0g ` R ) ) e. _V )
21 13 16 17 20 fvmptd 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( A ` C ) ` d ) = if ( d = ( I X. { 0 } ) , C , ( 0g ` R ) ) )
22 21 neeq1d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( A ` C ) ` d ) =/= ( 0g ` R ) <-> if ( d = ( I X. { 0 } ) , C , ( 0g ` R ) ) =/= ( 0g ` R ) ) )
23 iffalse 
 |-  ( -. d = ( I X. { 0 } ) -> if ( d = ( I X. { 0 } ) , C , ( 0g ` R ) ) = ( 0g ` R ) )
24 23 necon1ai 
 |-  ( if ( d = ( I X. { 0 } ) , C , ( 0g ` R ) ) =/= ( 0g ` R ) -> d = ( I X. { 0 } ) )
25 fconstmpt 
 |-  ( I X. { 0 } ) = ( k e. I |-> 0 )
26 25 oveq2i 
 |-  ( ( CCfld |`s NN0 ) gsum ( I X. { 0 } ) ) = ( ( CCfld |`s NN0 ) gsum ( k e. I |-> 0 ) )
27 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
28 eqid 
 |-  ( CCfld |`s NN0 ) = ( CCfld |`s NN0 )
29 28 submmnd 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> ( CCfld |`s NN0 ) e. Mnd )
30 27 29 ax-mp 
 |-  ( CCfld |`s NN0 ) e. Mnd
31 cnfld0 
 |-  0 = ( 0g ` CCfld )
32 28 31 subm0 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> 0 = ( 0g ` ( CCfld |`s NN0 ) ) )
33 27 32 ax-mp 
 |-  0 = ( 0g ` ( CCfld |`s NN0 ) )
34 33 gsumz 
 |-  ( ( ( CCfld |`s NN0 ) e. Mnd /\ I e. V ) -> ( ( CCfld |`s NN0 ) gsum ( k e. I |-> 0 ) ) = 0 )
35 30 10 34 sylancr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( CCfld |`s NN0 ) gsum ( k e. I |-> 0 ) ) = 0 )
36 26 35 eqtrid 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( CCfld |`s NN0 ) gsum ( I X. { 0 } ) ) = 0 )
37 oveq2 
 |-  ( d = ( I X. { 0 } ) -> ( ( CCfld |`s NN0 ) gsum d ) = ( ( CCfld |`s NN0 ) gsum ( I X. { 0 } ) ) )
38 37 eqeq1d 
 |-  ( d = ( I X. { 0 } ) -> ( ( ( CCfld |`s NN0 ) gsum d ) = 0 <-> ( ( CCfld |`s NN0 ) gsum ( I X. { 0 } ) ) = 0 ) )
39 36 38 syl5ibrcom 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d = ( I X. { 0 } ) -> ( ( CCfld |`s NN0 ) gsum d ) = 0 ) )
40 24 39 syl5 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( if ( d = ( I X. { 0 } ) , C , ( 0g ` R ) ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = 0 ) )
41 22 40 sylbid 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( A ` C ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = 0 ) )
42 41 ralrimiva 
 |-  ( ph -> A. d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( ( A ` C ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = 0 ) )
43 eqid 
 |-  ( Base ` P ) = ( Base ` P )
44 0nn0 
 |-  0 e. NN0
45 44 a1i 
 |-  ( ph -> 0 e. NN0 )
46 2 43 4 3 5 6 mplasclf 
 |-  ( ph -> A : K --> ( Base ` P ) )
47 46 7 ffvelrnd 
 |-  ( ph -> ( A ` C ) e. ( Base ` P ) )
48 1 2 43 9 8 5 6 45 47 ismhp3 
 |-  ( ph -> ( ( A ` C ) e. ( H ` 0 ) <-> A. d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( ( A ` C ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = 0 ) ) )
49 42 48 mpbird 
 |-  ( ph -> ( A ` C ) e. ( H ` 0 ) )