This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psdascl

Description: The derivative of a constant polynomial is zero. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses psdascl.s 
|- S = ( I mPwSer R )
psdascl.z 
|- .0. = ( 0g ` S )
psdascl.a 
|- A = ( algSc ` S )
psdascl.b 
|- B = ( Base ` R )
psdascl.i 
|- ( ph -> I e. V )
psdascl.r 
|- ( ph -> R e. CRing )
psdascl.x 
|- ( ph -> X e. I )
psdascl.c 
|- ( ph -> C e. B )
Assertion psdascl 
|- ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( A ` C ) ) = .0. )

Proof

Step Hyp Ref Expression
1 psdascl.s 
 |-  S = ( I mPwSer R )
2 psdascl.z 
 |-  .0. = ( 0g ` S )
3 psdascl.a 
 |-  A = ( algSc ` S )
4 psdascl.b 
 |-  B = ( Base ` R )
5 psdascl.i 
 |-  ( ph -> I e. V )
6 psdascl.r 
 |-  ( ph -> R e. CRing )
7 psdascl.x 
 |-  ( ph -> X e. I )
8 psdascl.c 
 |-  ( ph -> C e. B )
9 1 5 6 psrsca 
 |-  ( ph -> R = ( Scalar ` S ) )
10 9 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` S ) ) )
11 4 10 eqtrid 
 |-  ( ph -> B = ( Base ` ( Scalar ` S ) ) )
12 8 11 eleqtrd 
 |-  ( ph -> C e. ( Base ` ( Scalar ` S ) ) )
13 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
14 eqid 
 |-  ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
15 eqid 
 |-  ( .s ` S ) = ( .s ` S )
16 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
17 3 13 14 15 16 asclval 
 |-  ( C e. ( Base ` ( Scalar ` S ) ) -> ( A ` C ) = ( C ( .s ` S ) ( 1r ` S ) ) )
18 12 17 syl 
 |-  ( ph -> ( A ` C ) = ( C ( .s ` S ) ( 1r ` S ) ) )
19 18 fveq2d 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( A ` C ) ) = ( ( ( I mPSDer R ) ` X ) ` ( C ( .s ` S ) ( 1r ` S ) ) ) )
20 eqid 
 |-  ( Base ` S ) = ( Base ` S )
21 6 crngringd 
 |-  ( ph -> R e. Ring )
22 1 5 21 psrring 
 |-  ( ph -> S e. Ring )
23 20 16 ringidcl 
 |-  ( S e. Ring -> ( 1r ` S ) e. ( Base ` S ) )
24 22 23 syl 
 |-  ( ph -> ( 1r ` S ) e. ( Base ` S ) )
25 1 20 15 4 6 7 24 8 psdvsca 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( C ( .s ` S ) ( 1r ` S ) ) ) = ( C ( .s ` S ) ( ( ( I mPSDer R ) ` X ) ` ( 1r ` S ) ) ) )
26 1 16 2 5 6 7 psd1 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( 1r ` S ) ) = .0. )
27 26 oveq2d 
 |-  ( ph -> ( C ( .s ` S ) ( ( ( I mPSDer R ) ` X ) ` ( 1r ` S ) ) ) = ( C ( .s ` S ) .0. ) )
28 1 5 21 psrlmod 
 |-  ( ph -> S e. LMod )
29 13 15 14 2 lmodvs0 
 |-  ( ( S e. LMod /\ C e. ( Base ` ( Scalar ` S ) ) ) -> ( C ( .s ` S ) .0. ) = .0. )
30 28 12 29 syl2anc 
 |-  ( ph -> ( C ( .s ` S ) .0. ) = .0. )
31 27 30 eqtrd 
 |-  ( ph -> ( C ( .s ` S ) ( ( ( I mPSDer R ) ` X ) ` ( 1r ` S ) ) ) = .0. )
32 19 25 31 3eqtrd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( A ` C ) ) = .0. )