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 ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psdascl.z ⊢ 0 = ( 0g ‘ 𝑆 )
psdascl.a ⊢ 𝐴 = ( algSc ‘ 𝑆 )
psdascl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
psdascl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psdascl.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
psdascl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
psdascl.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion psdascl ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝐶 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 psdascl.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psdascl.z ⊢ 0 = ( 0g ‘ 𝑆 )
3 psdascl.a ⊢ 𝐴 = ( algSc ‘ 𝑆 )
4 psdascl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
5 psdascl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 psdascl.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
7 psdascl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
8 psdascl.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
9 1 5 6 psrsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) )
10 9 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
11 4 10 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
12 8 11 eleqtrd ⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
13 eqid ⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
14 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
15 eqid ⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
16 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
17 3 13 14 15 16 asclval ⊢ ( 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) → ( 𝐴 ‘ 𝐶 ) = ( 𝐶 ( ·𝑠 ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
18 12 17 syl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) = ( 𝐶 ( ·𝑠 ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
19 18 fveq2d ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝐶 ) ) = ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶 ( ·𝑠 ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) )
20 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
21 6 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
22 1 5 21 psrring ⊢ ( 𝜑 → 𝑆 ∈ Ring )
23 20 16 ringidcl ⊢ ( 𝑆 ∈ Ring → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
24 22 23 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
25 1 20 15 4 6 7 24 8 psdvsca ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶 ( ·𝑠 ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) = ( 𝐶 ( ·𝑠 ‘ 𝑆 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 1r ‘ 𝑆 ) ) ) )
26 1 16 2 5 6 7 psd1 ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 1r ‘ 𝑆 ) ) = 0 )
27 26 oveq2d ⊢ ( 𝜑 → ( 𝐶 ( ·𝑠 ‘ 𝑆 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 1r ‘ 𝑆 ) ) ) = ( 𝐶 ( ·𝑠 ‘ 𝑆 ) 0 ) )
28 1 5 21 psrlmod ⊢ ( 𝜑 → 𝑆 ∈ LMod )
29 13 15 14 2 lmodvs0 ⊢ ( ( 𝑆 ∈ LMod ∧ 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) → ( 𝐶 ( ·𝑠 ‘ 𝑆 ) 0 ) = 0 )
30 28 12 29 syl2anc ⊢ ( 𝜑 → ( 𝐶 ( ·𝑠 ‘ 𝑆 ) 0 ) = 0 )
31 27 30 eqtrd ⊢ ( 𝜑 → ( 𝐶 ( ·𝑠 ‘ 𝑆 ) ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 1r ‘ 𝑆 ) ) ) = 0 )
32 19 25 31 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝐶 ) ) = 0 )