Metamath Proof Explorer

Theorem coe1sclmulval

Description: The value of the coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by AV, 14-Aug-2019)

Ref Expression
Hypotheses coe1sclmulval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
coe1sclmulval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
coe1sclmulval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
coe1sclmulval.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
coe1sclmulval.s ⊢ 𝑆 = ( ·𝑠 ‘ 𝑃 )
coe1sclmulval.t ⊢ ∙ = ( .r ‘ 𝑃 )
coe1sclmulval.u ⊢ · = ( .r ‘ 𝑅 )
Assertion coe1sclmulval ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑌 𝑆 𝑍 ) ) ‘ 𝑁 ) = ( 𝑌 · ( ( coe1 ‘ 𝑍 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 coe1sclmulval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 coe1sclmulval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 coe1sclmulval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 coe1sclmulval.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
5 coe1sclmulval.s ⊢ 𝑆 = ( ·𝑠 ‘ 𝑃 )
6 coe1sclmulval.t ⊢ ∙ = ( .r ‘ 𝑃 )
7 coe1sclmulval.u ⊢ · = ( .r ‘ 𝑅 )
8 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑅 ∈ Ring )
9 simp2l ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑌 ∈ 𝐾 )
10 simp2r ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑍 ∈ 𝐵 )
11 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
12 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
13 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
14 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
15 3 1 2 11 5 6 12 13 14 ply1sclrmsm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑌 ) ∙ 𝑍 ) = ( 𝑌 𝑆 𝑍 ) )
16 8 9 10 15 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑌 ) ∙ 𝑍 ) = ( 𝑌 𝑆 𝑍 ) )
17 16 eqcomd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑌 𝑆 𝑍 ) = ( ( ( algSc ‘ 𝑃 ) ‘ 𝑌 ) ∙ 𝑍 ) )
18 17 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → ( coe1 ‘ ( 𝑌 𝑆 𝑍 ) ) = ( coe1 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑌 ) ∙ 𝑍 ) ) )
19 18 fveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑌 𝑆 𝑍 ) ) ‘ 𝑁 ) = ( ( coe1 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑌 ) ∙ 𝑍 ) ) ‘ 𝑁 ) )
20 1 2 3 14 6 7 coe1sclmulfv ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑌 ) ∙ 𝑍 ) ) ‘ 𝑁 ) = ( 𝑌 · ( ( coe1 ‘ 𝑍 ) ‘ 𝑁 ) ) )
21 19 20 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐾 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑌 𝑆 𝑍 ) ) ‘ 𝑁 ) = ( 𝑌 · ( ( coe1 ‘ 𝑍 ) ‘ 𝑁 ) ) )