Metamath Proof Explorer

Theorem coe1sclmul

Description: Coefficient vector of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses coe1sclmul.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
coe1sclmul.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
coe1sclmul.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
coe1sclmul.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
coe1sclmul.t ⊢ ∙ = ( .r ‘ 𝑃 )
coe1sclmul.u ⊢ · = ( .r ‘ 𝑅 )
Assertion coe1sclmul ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) = ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 coe1sclmul.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 coe1sclmul.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 coe1sclmul.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 coe1sclmul.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
5 coe1sclmul.t ⊢ ∙ = ( .r ‘ 𝑃 )
6 coe1sclmul.u ⊢ · = ( .r ‘ 𝑅 )
7 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
9 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
10 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
11 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
12 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
13 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Ring )
14 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐾 )
15 0nn0 ⊢ 0 ∈ ℕ0
16 15 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 0 ∈ ℕ0 )
17 7 3 1 8 9 10 11 2 5 6 12 13 14 16 coe1tmmul ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∙ 𝑌 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 0 ≤ 𝑥 , ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) , ( 0g ‘ 𝑅 ) ) ) )
18 3 1 8 9 10 11 4 ply1scltm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
19 18 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
20 19 fvoveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) = ( coe1 ‘ ( ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∙ 𝑌 ) ) )
21 nn0ex ⊢ ℕ0 ∈ V
22 21 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ℕ0 ∈ V )
23 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑋 ∈ 𝐾 )
24 fvexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ∈ V )
25 fconstmpt ⊢ ( ℕ0 × { 𝑋 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝑋 )
26 25 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ℕ0 × { 𝑋 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝑋 ) )
27 eqid ⊢ ( coe1 ‘ 𝑌 ) = ( coe1 ‘ 𝑌 )
28 27 2 1 3 coe1f ⊢ ( 𝑌 ∈ 𝐵 → ( coe1 ‘ 𝑌 ) : ℕ0 ⟶ 𝐾 )
29 28 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ 𝑌 ) : ℕ0 ⟶ 𝐾 )
30 29 feqmptd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ 𝑌 ) = ( 𝑥 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
31 22 23 24 26 30 offval2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) ) )
32 nn0ge0 ⊢ ( 𝑥 ∈ ℕ0 → 0 ≤ 𝑥 )
33 32 iftrued ⊢ ( 𝑥 ∈ ℕ0 → if ( 0 ≤ 𝑥 , ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) , ( 0g ‘ 𝑅 ) ) = ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) )
34 nn0cn ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
35 34 subid1d ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 − 0 ) = 𝑥 )
36 35 fveq2d ⊢ ( 𝑥 ∈ ℕ0 → ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) = ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) )
37 36 oveq2d ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) = ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
38 33 37 eqtrd ⊢ ( 𝑥 ∈ ℕ0 → if ( 0 ≤ 𝑥 , ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) , ( 0g ‘ 𝑅 ) ) = ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
39 38 mpteq2ia ⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 0 ≤ 𝑥 , ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
40 31 39 eqtr4di ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 0 ≤ 𝑥 , ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) , ( 0g ‘ 𝑅 ) ) ) )
41 17 20 40 3eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) = ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) )