Metamath Proof Explorer


Theorem coe1tmmul2fv

Description: Function value of a right-multiplication by a term in the shifted domain. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses coe1tm.z 0 ˙ = 0 R
coe1tm.k K = Base R
coe1tm.p P = Poly 1 R
coe1tm.x X = var 1 R
coe1tm.m · ˙ = P
coe1tm.n N = mulGrp P
coe1tm.e × ˙ = N
coe1tmmul.b B = Base P
coe1tmmul.t ˙ = P
coe1tmmul.u × ˙ = R
coe1tmmul.a φ A B
coe1tmmul.r φ R Ring
coe1tmmul.c φ C K
coe1tmmul.d φ D 0
coe1tmmul2fv.y φ Y 0
Assertion coe1tmmul2fv φ coe 1 A ˙ C · ˙ D × ˙ X D + Y = coe 1 A Y × ˙ C

Proof

Step Hyp Ref Expression
1 coe1tm.z 0 ˙ = 0 R
2 coe1tm.k K = Base R
3 coe1tm.p P = Poly 1 R
4 coe1tm.x X = var 1 R
5 coe1tm.m · ˙ = P
6 coe1tm.n N = mulGrp P
7 coe1tm.e × ˙ = N
8 coe1tmmul.b B = Base P
9 coe1tmmul.t ˙ = P
10 coe1tmmul.u × ˙ = R
11 coe1tmmul.a φ A B
12 coe1tmmul.r φ R Ring
13 coe1tmmul.c φ C K
14 coe1tmmul.d φ D 0
15 coe1tmmul2fv.y φ Y 0
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 coe1tmmul2 φ coe 1 A ˙ C · ˙ D × ˙ X = x 0 if D x coe 1 A x D × ˙ C 0 ˙
17 16 fveq1d φ coe 1 A ˙ C · ˙ D × ˙ X D + Y = x 0 if D x coe 1 A x D × ˙ C 0 ˙ D + Y
18 14 15 nn0addcld φ D + Y 0
19 breq2 x = D + Y D x D D + Y
20 fvoveq1 x = D + Y coe 1 A x D = coe 1 A D + Y - D
21 20 oveq1d x = D + Y coe 1 A x D × ˙ C = coe 1 A D + Y - D × ˙ C
22 19 21 ifbieq1d x = D + Y if D x coe 1 A x D × ˙ C 0 ˙ = if D D + Y coe 1 A D + Y - D × ˙ C 0 ˙
23 eqid x 0 if D x coe 1 A x D × ˙ C 0 ˙ = x 0 if D x coe 1 A x D × ˙ C 0 ˙
24 ovex coe 1 A D + Y - D × ˙ C V
25 1 fvexi 0 ˙ V
26 24 25 ifex if D D + Y coe 1 A D + Y - D × ˙ C 0 ˙ V
27 22 23 26 fvmpt D + Y 0 x 0 if D x coe 1 A x D × ˙ C 0 ˙ D + Y = if D D + Y coe 1 A D + Y - D × ˙ C 0 ˙
28 18 27 syl φ x 0 if D x coe 1 A x D × ˙ C 0 ˙ D + Y = if D D + Y coe 1 A D + Y - D × ˙ C 0 ˙
29 14 nn0red φ D
30 nn0addge1 D Y 0 D D + Y
31 29 15 30 syl2anc φ D D + Y
32 31 iftrued φ if D D + Y coe 1 A D + Y - D × ˙ C 0 ˙ = coe 1 A D + Y - D × ˙ C
33 14 nn0cnd φ D
34 15 nn0cnd φ Y
35 33 34 pncan2d φ D + Y - D = Y
36 35 fveq2d φ coe 1 A D + Y - D = coe 1 A Y
37 36 oveq1d φ coe 1 A D + Y - D × ˙ C = coe 1 A Y × ˙ C
38 28 32 37 3eqtrd φ x 0 if D x coe 1 A x D × ˙ C 0 ˙ D + Y = coe 1 A Y × ˙ C
39 17 38 eqtrd φ coe 1 A ˙ C · ˙ D × ˙ X D + Y = coe 1 A Y × ˙ C