# Metamath Proof Explorer

## Theorem coe1pwmulfv

Description: Function value of a right-multiplication by a variable power in the shifted domain. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses coe1pwmul.z
coe1pwmul.p $⊢ P = Poly 1 ⁡ R$
coe1pwmul.x $⊢ X = var 1 ⁡ R$
coe1pwmul.n $⊢ N = mulGrp P$
coe1pwmul.e
coe1pwmul.b $⊢ B = Base P$
coe1pwmul.t
coe1pwmul.r $⊢ φ → R ∈ Ring$
coe1pwmul.a $⊢ φ → A ∈ B$
coe1pwmul.d $⊢ φ → D ∈ ℕ 0$
coe1pwmulfv.y $⊢ φ → Y ∈ ℕ 0$
Assertion coe1pwmulfv

### Proof

Step Hyp Ref Expression
1 coe1pwmul.z
2 coe1pwmul.p $⊢ P = Poly 1 ⁡ R$
3 coe1pwmul.x $⊢ X = var 1 ⁡ R$
4 coe1pwmul.n $⊢ N = mulGrp P$
5 coe1pwmul.e
6 coe1pwmul.b $⊢ B = Base P$
7 coe1pwmul.t
8 coe1pwmul.r $⊢ φ → R ∈ Ring$
9 coe1pwmul.a $⊢ φ → A ∈ B$
10 coe1pwmul.d $⊢ φ → D ∈ ℕ 0$
11 coe1pwmulfv.y $⊢ φ → Y ∈ ℕ 0$
12 1 2 3 4 5 6 7 8 9 10 coe1pwmul
13 12 fveq1d
14 10 11 nn0addcld $⊢ φ → D + Y ∈ ℕ 0$
15 breq2 $⊢ x = D + Y → D ≤ x ↔ D ≤ D + Y$
16 fvoveq1 $⊢ x = D + Y → coe 1 ⁡ A ⁡ x − D = coe 1 ⁡ A ⁡ D + Y - D$
17 15 16 ifbieq1d
18 eqid
19 fvex $⊢ coe 1 ⁡ A ⁡ D + Y - D ∈ V$
20 1 fvexi
21 19 20 ifex
22 17 18 21 fvmpt
23 14 22 syl
24 10 nn0red $⊢ φ → D ∈ ℝ$
25 nn0addge1 $⊢ D ∈ ℝ ∧ Y ∈ ℕ 0 → D ≤ D + Y$
26 24 11 25 syl2anc $⊢ φ → D ≤ D + Y$
27 26 iftrued
28 10 nn0cnd $⊢ φ → D ∈ ℂ$
29 11 nn0cnd $⊢ φ → Y ∈ ℂ$
30 28 29 pncan2d $⊢ φ → D + Y - D = Y$
31 30 fveq2d $⊢ φ → coe 1 ⁡ A ⁡ D + Y - D = coe 1 ⁡ A ⁡ Y$
32 23 27 31 3eqtrd
33 13 32 eqtrd