Metamath Proof Explorer


Theorem coe1tm

Description: Coefficient vector of a polynomial 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
Assertion coe1tm R Ring C K D 0 coe 1 C · ˙ D × ˙ X = x 0 if 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 eqid Base P = Base P
9 2 3 4 5 6 7 8 ply1tmcl R Ring C K D 0 C · ˙ D × ˙ X Base P
10 eqid coe 1 C · ˙ D × ˙ X = coe 1 C · ˙ D × ˙ X
11 eqid x 0 1 𝑜 × x = x 0 1 𝑜 × x
12 10 8 3 11 coe1fval2 C · ˙ D × ˙ X Base P coe 1 C · ˙ D × ˙ X = C · ˙ D × ˙ X x 0 1 𝑜 × x
13 9 12 syl R Ring C K D 0 coe 1 C · ˙ D × ˙ X = C · ˙ D × ˙ X x 0 1 𝑜 × x
14 fconst6g x 0 1 𝑜 × x : 1 𝑜 0
15 nn0ex 0 V
16 1oex 1 𝑜 V
17 15 16 elmap 1 𝑜 × x 0 1 𝑜 1 𝑜 × x : 1 𝑜 0
18 14 17 sylibr x 0 1 𝑜 × x 0 1 𝑜
19 18 adantl R Ring C K D 0 x 0 1 𝑜 × x 0 1 𝑜
20 eqidd R Ring C K D 0 x 0 1 𝑜 × x = x 0 1 𝑜 × x
21 eqid mulGrp 1 𝑜 mPoly R = mulGrp 1 𝑜 mPoly R
22 6 8 mgpbas Base P = Base N
23 22 a1i R Ring Base P = Base N
24 eqid mulGrp 1 𝑜 mPoly R = mulGrp 1 𝑜 mPoly R
25 eqid PwSer 1 R = PwSer 1 R
26 3 25 8 ply1bas Base P = Base 1 𝑜 mPoly R
27 24 26 mgpbas Base P = Base mulGrp 1 𝑜 mPoly R
28 27 a1i R Ring Base P = Base mulGrp 1 𝑜 mPoly R
29 ssv Base P V
30 29 a1i R Ring Base P V
31 ovexd R Ring x V y V x + N y V
32 eqid P = P
33 6 32 mgpplusg P = + N
34 eqid 1 𝑜 mPoly R = 1 𝑜 mPoly R
35 3 34 32 ply1mulr P = 1 𝑜 mPoly R
36 24 35 mgpplusg P = + mulGrp 1 𝑜 mPoly R
37 33 36 eqtr3i + N = + mulGrp 1 𝑜 mPoly R
38 37 a1i R Ring + N = + mulGrp 1 𝑜 mPoly R
39 38 oveqdr R Ring x V y V x + N y = x + mulGrp 1 𝑜 mPoly R y
40 7 21 23 28 30 31 39 mulgpropd R Ring × ˙ = mulGrp 1 𝑜 mPoly R
41 40 3ad2ant1 R Ring C K D 0 × ˙ = mulGrp 1 𝑜 mPoly R
42 eqidd R Ring C K D 0 D = D
43 4 vr1val X = 1 𝑜 mVar R
44 43 a1i R Ring C K D 0 X = 1 𝑜 mVar R
45 41 42 44 oveq123d R Ring C K D 0 D × ˙ X = D mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R
46 45 oveq2d R Ring C K D 0 C · ˙ D × ˙ X = C · ˙ D mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R
47 psr1baslem 0 1 𝑜 = a 0 1 𝑜 | a -1 Fin
48 eqid 1 R = 1 R
49 1on 1 𝑜 On
50 49 a1i R Ring C K D 0 1 𝑜 On
51 eqid 1 𝑜 mVar R = 1 𝑜 mVar R
52 simp1 R Ring C K D 0 R Ring
53 0lt1o 1 𝑜
54 53 a1i R Ring C K D 0 1 𝑜
55 simp3 R Ring C K D 0 D 0
56 34 47 1 48 50 24 21 51 52 54 55 mplcoe3 R Ring C K D 0 y 0 1 𝑜 if y = b 1 𝑜 if b = D 0 1 R 0 ˙ = D mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R
57 56 oveq2d R Ring C K D 0 C · ˙ y 0 1 𝑜 if y = b 1 𝑜 if b = D 0 1 R 0 ˙ = C · ˙ D mulGrp 1 𝑜 mPoly R 1 𝑜 mVar R
58 3 34 5 ply1vsca · ˙ = 1 𝑜 mPoly R
59 elsni b b =
60 df1o2 1 𝑜 =
61 59 60 eleq2s b 1 𝑜 b =
62 61 iftrued b 1 𝑜 if b = D 0 = D
63 62 adantl R Ring C K D 0 b 1 𝑜 if b = D 0 = D
64 63 mpteq2dva R Ring C K D 0 b 1 𝑜 if b = D 0 = b 1 𝑜 D
65 fconstmpt 1 𝑜 × D = b 1 𝑜 D
66 64 65 eqtr4di R Ring C K D 0 b 1 𝑜 if b = D 0 = 1 𝑜 × D
67 fconst6g D 0 1 𝑜 × D : 1 𝑜 0
68 15 16 elmap 1 𝑜 × D 0 1 𝑜 1 𝑜 × D : 1 𝑜 0
69 67 68 sylibr D 0 1 𝑜 × D 0 1 𝑜
70 69 3ad2ant3 R Ring C K D 0 1 𝑜 × D 0 1 𝑜
71 66 70 eqeltrd R Ring C K D 0 b 1 𝑜 if b = D 0 0 1 𝑜
72 simp2 R Ring C K D 0 C K
73 34 58 47 48 1 2 50 52 71 72 mplmon2 R Ring C K D 0 C · ˙ y 0 1 𝑜 if y = b 1 𝑜 if b = D 0 1 R 0 ˙ = y 0 1 𝑜 if y = b 1 𝑜 if b = D 0 C 0 ˙
74 46 57 73 3eqtr2d R Ring C K D 0 C · ˙ D × ˙ X = y 0 1 𝑜 if y = b 1 𝑜 if b = D 0 C 0 ˙
75 eqeq1 y = 1 𝑜 × x y = b 1 𝑜 if b = D 0 1 𝑜 × x = b 1 𝑜 if b = D 0
76 75 ifbid y = 1 𝑜 × x if y = b 1 𝑜 if b = D 0 C 0 ˙ = if 1 𝑜 × x = b 1 𝑜 if b = D 0 C 0 ˙
77 19 20 74 76 fmptco R Ring C K D 0 C · ˙ D × ˙ X x 0 1 𝑜 × x = x 0 if 1 𝑜 × x = b 1 𝑜 if b = D 0 C 0 ˙
78 66 adantr R Ring C K D 0 x 0 b 1 𝑜 if b = D 0 = 1 𝑜 × D
79 78 eqeq2d R Ring C K D 0 x 0 1 𝑜 × x = b 1 𝑜 if b = D 0 1 𝑜 × x = 1 𝑜 × D
80 fveq1 1 𝑜 × x = 1 𝑜 × D 1 𝑜 × x = 1 𝑜 × D
81 vex x V
82 81 fvconst2 1 𝑜 1 𝑜 × x = x
83 53 82 mp1i R Ring C K D 0 x 0 1 𝑜 × x = x
84 simpl3 R Ring C K D 0 x 0 D 0
85 fvconst2g D 0 1 𝑜 1 𝑜 × D = D
86 84 53 85 sylancl R Ring C K D 0 x 0 1 𝑜 × D = D
87 83 86 eqeq12d R Ring C K D 0 x 0 1 𝑜 × x = 1 𝑜 × D x = D
88 80 87 syl5ib R Ring C K D 0 x 0 1 𝑜 × x = 1 𝑜 × D x = D
89 sneq x = D x = D
90 89 xpeq2d x = D 1 𝑜 × x = 1 𝑜 × D
91 88 90 impbid1 R Ring C K D 0 x 0 1 𝑜 × x = 1 𝑜 × D x = D
92 79 91 bitrd R Ring C K D 0 x 0 1 𝑜 × x = b 1 𝑜 if b = D 0 x = D
93 92 ifbid R Ring C K D 0 x 0 if 1 𝑜 × x = b 1 𝑜 if b = D 0 C 0 ˙ = if x = D C 0 ˙
94 93 mpteq2dva R Ring C K D 0 x 0 if 1 𝑜 × x = b 1 𝑜 if b = D 0 C 0 ˙ = x 0 if x = D C 0 ˙
95 13 77 94 3eqtrd R Ring C K D 0 coe 1 C · ˙ D × ˙ X = x 0 if x = D C 0 ˙