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

Metamath Proof Explorer

Theorem coe1sclmul2

Description: Coefficient vector of a polynomial multiplied on the right 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 coe1sclmul2 ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( 𝑌 ∙ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( coe1 ‘ 𝑌 ) ∘f · ( ℕ0 × { 𝑋 } ) ) )

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 coe1tmmul2 ⊢ ( ( 𝑅 ∈ 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 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∙ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑌 ∙ ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
21 20 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( 𝑌 ∙ ( 𝐴 ‘ 𝑋 ) ) ) = ( coe1 ‘ ( 𝑌 ∙ ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) )
22 nn0ex ⊢ ℕ0 ∈ V
23 22 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ℕ0 ∈ V )
24 fvexd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ∈ V )
25 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑋 ∈ 𝐾 )
26 eqid ⊢ ( coe1 ‘ 𝑌 ) = ( coe1 ‘ 𝑌 )
27 26 2 1 3 coe1f ⊢ ( 𝑌 ∈ 𝐵 → ( coe1 ‘ 𝑌 ) : ℕ0 ⟶ 𝐾 )
28 27 feqmptd ⊢ ( 𝑌 ∈ 𝐵 → ( coe1 ‘ 𝑌 ) = ( 𝑥 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
29 28 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ 𝑌 ) = ( 𝑥 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
30 fconstmpt ⊢ ( ℕ0 × { 𝑋 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝑋 )
31 30 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ℕ0 × { 𝑋 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝑋 ) )
32 23 24 25 29 31 offval2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑌 ) ∘f · ( ℕ0 × { 𝑋 } ) ) = ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) · 𝑋 ) ) )
33 nn0ge0 ⊢ ( 𝑥 ∈ ℕ0 → 0 ≤ 𝑥 )
34 33 iftrued ⊢ ( 𝑥 ∈ ℕ0 → if ( 0 ≤ 𝑥 , ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) , ( 0g ‘ 𝑅 ) ) = ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) )
35 nn0cn ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
36 35 subid1d ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 − 0 ) = 𝑥 )
37 36 fveq2d ⊢ ( 𝑥 ∈ ℕ0 → ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) = ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) )
38 37 oveq1d ⊢ ( 𝑥 ∈ ℕ0 → ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) = ( ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) · 𝑋 ) )
39 34 38 eqtrd ⊢ ( 𝑥 ∈ ℕ0 → if ( 0 ≤ 𝑥 , ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) , ( 0g ‘ 𝑅 ) ) = ( ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) · 𝑋 ) )
40 39 mpteq2ia ⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 0 ≤ 𝑥 , ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) · 𝑋 ) )
41 32 40 eqtr4di ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑌 ) ∘f · ( ℕ0 × { 𝑋 } ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 0 ≤ 𝑥 , ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) , ( 0g ‘ 𝑅 ) ) ) )
42 17 21 41 3eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( 𝑌 ∙ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( coe1 ‘ 𝑌 ) ∘f · ( ℕ0 × { 𝑋 } ) ) )