Metamath Proof Explorer


Theorem coe1tmmul2

Description: Coefficient vector of a polynomial multiplied on the right by a term. (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
Assertion coe1tmmul2 φ coe 1 A ˙ C · ˙ D × ˙ X = x 0 if D x coe 1 A x D × ˙ C 0 ˙

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 2 3 4 5 6 7 8 ply1tmcl R Ring C K D 0 C · ˙ D × ˙ X B
16 12 13 14 15 syl3anc φ C · ˙ D × ˙ X B
17 3 9 10 8 coe1mul R Ring A B C · ˙ D × ˙ X B coe 1 A ˙ C · ˙ D × ˙ X = x 0 R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y
18 12 11 16 17 syl3anc φ coe 1 A ˙ C · ˙ D × ˙ X = x 0 R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y
19 eqeq2 coe 1 A x D × ˙ C = if D x coe 1 A x D × ˙ C 0 ˙ R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = coe 1 A x D × ˙ C R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = if D x coe 1 A x D × ˙ C 0 ˙
20 eqeq2 0 ˙ = if D x coe 1 A x D × ˙ C 0 ˙ R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = 0 ˙ R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = if D x coe 1 A x D × ˙ C 0 ˙
21 12 adantr φ x 0 D x R Ring
22 ringmnd R Ring R Mnd
23 21 22 syl φ x 0 D x R Mnd
24 ovex 0 x V
25 24 a1i φ x 0 D x 0 x V
26 simprr φ x 0 D x D x
27 14 adantr φ x 0 D x D 0
28 simprl φ x 0 D x x 0
29 nn0sub D 0 x 0 D x x D 0
30 27 28 29 syl2anc φ x 0 D x D x x D 0
31 26 30 mpbid φ x 0 D x x D 0
32 27 nn0ge0d φ x 0 D x 0 D
33 nn0re x 0 x
34 33 ad2antrl φ x 0 D x x
35 14 nn0red φ D
36 35 adantr φ x 0 D x D
37 34 36 subge02d φ x 0 D x 0 D x D x
38 32 37 mpbid φ x 0 D x x D x
39 fznn0 x 0 x D 0 x x D 0 x D x
40 39 ad2antrl φ x 0 D x x D 0 x x D 0 x D x
41 31 38 40 mpbir2and φ x 0 D x x D 0 x
42 12 ad2antrr φ x 0 D x y 0 x R Ring
43 eqid coe 1 A = coe 1 A
44 43 8 3 2 coe1f A B coe 1 A : 0 K
45 11 44 syl φ coe 1 A : 0 K
46 45 ad2antrr φ x 0 D x y 0 x coe 1 A : 0 K
47 elfznn0 y 0 x y 0
48 47 adantl φ x 0 D x y 0 x y 0
49 46 48 ffvelrnd φ x 0 D x y 0 x coe 1 A y K
50 eqid coe 1 C · ˙ D × ˙ X = coe 1 C · ˙ D × ˙ X
51 50 8 3 2 coe1f C · ˙ D × ˙ X B coe 1 C · ˙ D × ˙ X : 0 K
52 16 51 syl φ coe 1 C · ˙ D × ˙ X : 0 K
53 52 ad2antrr φ x 0 D x y 0 x coe 1 C · ˙ D × ˙ X : 0 K
54 fznn0sub y 0 x x y 0
55 54 adantl φ x 0 D x y 0 x x y 0
56 53 55 ffvelrnd φ x 0 D x y 0 x coe 1 C · ˙ D × ˙ X x y K
57 2 10 ringcl R Ring coe 1 A y K coe 1 C · ˙ D × ˙ X x y K coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y K
58 42 49 56 57 syl3anc φ x 0 D x y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y K
59 58 fmpttd φ x 0 D x y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y : 0 x K
60 12 ad2antrr φ x 0 D x y 0 x x D R Ring
61 13 ad2antrr φ x 0 D x y 0 x x D C K
62 14 ad2antrr φ x 0 D x y 0 x x D D 0
63 eldifi y 0 x x D y 0 x
64 63 54 syl y 0 x x D x y 0
65 64 adantl φ x 0 D x y 0 x x D x y 0
66 eldifsn y 0 x x D y 0 x y x D
67 simplrl φ x 0 D x y 0 x x 0
68 67 nn0cnd φ x 0 D x y 0 x x
69 47 nn0cnd y 0 x y
70 69 adantl φ x 0 D x y 0 x y
71 68 70 nncand φ x 0 D x y 0 x x x y = y
72 71 eqcomd φ x 0 D x y 0 x y = x x y
73 oveq2 D = x y x D = x x y
74 73 eqeq2d D = x y y = x D y = x x y
75 72 74 syl5ibrcom φ x 0 D x y 0 x D = x y y = x D
76 75 necon3d φ x 0 D x y 0 x y x D D x y
77 76 impr φ x 0 D x y 0 x y x D D x y
78 66 77 sylan2b φ x 0 D x y 0 x x D D x y
79 1 2 3 4 5 6 7 60 61 62 65 78 coe1tmfv2 φ x 0 D x y 0 x x D coe 1 C · ˙ D × ˙ X x y = 0 ˙
80 79 oveq2d φ x 0 D x y 0 x x D coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = coe 1 A y × ˙ 0 ˙
81 2 10 1 ringrz R Ring coe 1 A y K coe 1 A y × ˙ 0 ˙ = 0 ˙
82 42 49 81 syl2anc φ x 0 D x y 0 x coe 1 A y × ˙ 0 ˙ = 0 ˙
83 63 82 sylan2 φ x 0 D x y 0 x x D coe 1 A y × ˙ 0 ˙ = 0 ˙
84 80 83 eqtrd φ x 0 D x y 0 x x D coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = 0 ˙
85 84 25 suppss2 φ x 0 D x y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y supp 0 ˙ x D
86 2 1 23 25 41 59 85 gsumpt φ x 0 D x R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y x D
87 fveq2 y = x D coe 1 A y = coe 1 A x D
88 oveq2 y = x D x y = x x D
89 88 fveq2d y = x D coe 1 C · ˙ D × ˙ X x y = coe 1 C · ˙ D × ˙ X x x D
90 87 89 oveq12d y = x D coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = coe 1 A x D × ˙ coe 1 C · ˙ D × ˙ X x x D
91 eqid y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y
92 ovex coe 1 A x D × ˙ coe 1 C · ˙ D × ˙ X x x D V
93 90 91 92 fvmpt x D 0 x y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y x D = coe 1 A x D × ˙ coe 1 C · ˙ D × ˙ X x x D
94 41 93 syl φ x 0 D x y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y x D = coe 1 A x D × ˙ coe 1 C · ˙ D × ˙ X x x D
95 28 nn0cnd φ x 0 D x x
96 27 nn0cnd φ x 0 D x D
97 95 96 nncand φ x 0 D x x x D = D
98 97 fveq2d φ x 0 D x coe 1 C · ˙ D × ˙ X x x D = coe 1 C · ˙ D × ˙ X D
99 13 adantr φ x 0 D x C K
100 1 2 3 4 5 6 7 coe1tmfv1 R Ring C K D 0 coe 1 C · ˙ D × ˙ X D = C
101 21 99 27 100 syl3anc φ x 0 D x coe 1 C · ˙ D × ˙ X D = C
102 98 101 eqtrd φ x 0 D x coe 1 C · ˙ D × ˙ X x x D = C
103 102 oveq2d φ x 0 D x coe 1 A x D × ˙ coe 1 C · ˙ D × ˙ X x x D = coe 1 A x D × ˙ C
104 86 94 103 3eqtrd φ x 0 D x R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = coe 1 A x D × ˙ C
105 104 anassrs φ x 0 D x R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = coe 1 A x D × ˙ C
106 12 ad2antrr φ x 0 ¬ D x y 0 x R Ring
107 13 ad2antrr φ x 0 ¬ D x y 0 x C K
108 14 ad2antrr φ x 0 ¬ D x y 0 x D 0
109 54 ad2antll φ x 0 ¬ D x y 0 x x y 0
110 54 nn0red y 0 x x y
111 110 ad2antll φ x 0 ¬ D x y 0 x x y
112 33 ad2antlr φ x 0 ¬ D x y 0 x x
113 35 ad2antrr φ x 0 ¬ D x y 0 x D
114 47 ad2antll φ x 0 ¬ D x y 0 x y 0
115 114 nn0ge0d φ x 0 ¬ D x y 0 x 0 y
116 47 nn0red y 0 x y
117 116 ad2antll φ x 0 ¬ D x y 0 x y
118 112 117 subge02d φ x 0 ¬ D x y 0 x 0 y x y x
119 115 118 mpbid φ x 0 ¬ D x y 0 x x y x
120 simprl φ x 0 ¬ D x y 0 x ¬ D x
121 112 113 ltnled φ x 0 ¬ D x y 0 x x < D ¬ D x
122 120 121 mpbird φ x 0 ¬ D x y 0 x x < D
123 111 112 113 119 122 lelttrd φ x 0 ¬ D x y 0 x x y < D
124 111 123 gtned φ x 0 ¬ D x y 0 x D x y
125 1 2 3 4 5 6 7 106 107 108 109 124 coe1tmfv2 φ x 0 ¬ D x y 0 x coe 1 C · ˙ D × ˙ X x y = 0 ˙
126 125 oveq2d φ x 0 ¬ D x y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = coe 1 A y × ˙ 0 ˙
127 45 ad2antrr φ x 0 ¬ D x y 0 x coe 1 A : 0 K
128 127 114 ffvelrnd φ x 0 ¬ D x y 0 x coe 1 A y K
129 106 128 81 syl2anc φ x 0 ¬ D x y 0 x coe 1 A y × ˙ 0 ˙ = 0 ˙
130 126 129 eqtrd φ x 0 ¬ D x y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = 0 ˙
131 130 anassrs φ x 0 ¬ D x y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = 0 ˙
132 131 mpteq2dva φ x 0 ¬ D x y 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = y 0 x 0 ˙
133 132 oveq2d φ x 0 ¬ D x R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = R y = 0 x 0 ˙
134 12 22 syl φ R Mnd
135 1 gsumz R Mnd 0 x V R y = 0 x 0 ˙ = 0 ˙
136 134 24 135 sylancl φ R y = 0 x 0 ˙ = 0 ˙
137 136 ad2antrr φ x 0 ¬ D x R y = 0 x 0 ˙ = 0 ˙
138 133 137 eqtrd φ x 0 ¬ D x R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = 0 ˙
139 19 20 105 138 ifbothda φ x 0 R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = if D x coe 1 A x D × ˙ C 0 ˙
140 139 mpteq2dva φ x 0 R y = 0 x coe 1 A y × ˙ coe 1 C · ˙ D × ˙ X x y = x 0 if D x coe 1 A x D × ˙ C 0 ˙
141 18 140 eqtrd φ coe 1 A ˙ C · ˙ D × ˙ X = x 0 if D x coe 1 A x D × ˙ C 0 ˙