Metamath Proof Explorer


Theorem coe1mul2

Description: The coefficient vector of multiplication in the univariate power series ring. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses coe1mul2.s S=PwSer1R
coe1mul2.t ˙=S
coe1mul2.u ·˙=R
coe1mul2.b B=BaseS
Assertion coe1mul2 RRingFBGBcoe1F˙G=k0Rx=0kcoe1Fx·˙coe1Gkx

Proof

Step Hyp Ref Expression
1 coe1mul2.s S=PwSer1R
2 coe1mul2.t ˙=S
3 coe1mul2.u ·˙=R
4 coe1mul2.b B=BaseS
5 fconst6g k01𝑜×k:1𝑜0
6 nn0ex 0V
7 1on 1𝑜On
8 7 elexi 1𝑜V
9 6 8 elmap 1𝑜×k01𝑜1𝑜×k:1𝑜0
10 5 9 sylibr k01𝑜×k01𝑜
11 10 adantl RRingFBGBk01𝑜×k01𝑜
12 eqidd RRingFBGBk01𝑜×k=k01𝑜×k
13 eqid 1𝑜mPwSerR=1𝑜mPwSerR
14 1 4 13 psr1bas2 B=Base1𝑜mPwSerR
15 1 13 2 psr1mulr ˙=1𝑜mPwSerR
16 psr1baslem 01𝑜=a01𝑜|a-1Fin
17 simp2 RRingFBGBFB
18 simp3 RRingFBGBGB
19 13 14 3 15 16 17 18 psrmulfval RRingFBGBF˙G=b01𝑜Rcd01𝑜|dfbFc·˙Gbfc
20 breq2 b=1𝑜×kdfbdf1𝑜×k
21 20 rabbidv b=1𝑜×kd01𝑜|dfb=d01𝑜|df1𝑜×k
22 fvoveq1 b=1𝑜×kGbfc=G1𝑜×kfc
23 22 oveq2d b=1𝑜×kFc·˙Gbfc=Fc·˙G1𝑜×kfc
24 21 23 mpteq12dv b=1𝑜×kcd01𝑜|dfbFc·˙Gbfc=cd01𝑜|df1𝑜×kFc·˙G1𝑜×kfc
25 24 oveq2d b=1𝑜×kRcd01𝑜|dfbFc·˙Gbfc=Rcd01𝑜|df1𝑜×kFc·˙G1𝑜×kfc
26 11 12 19 25 fmptco RRingFBGBF˙Gk01𝑜×k=k0Rcd01𝑜|df1𝑜×kFc·˙G1𝑜×kfc
27 1 psr1ring RRingSRing
28 4 2 ringcl SRingFBGBF˙GB
29 27 28 syl3an1 RRingFBGBF˙GB
30 eqid coe1F˙G=coe1F˙G
31 eqid k01𝑜×k=k01𝑜×k
32 30 4 1 31 coe1fval3 F˙GBcoe1F˙G=F˙Gk01𝑜×k
33 29 32 syl RRingFBGBcoe1F˙G=F˙Gk01𝑜×k
34 eqid BaseR=BaseR
35 eqid 0R=0R
36 simpl1 RRingFBGBk0RRing
37 ringcmn RRingRCMnd
38 36 37 syl RRingFBGBk0RCMnd
39 fzfi 0kFin
40 39 a1i RRingFBGBk00kFin
41 simpll1 RRingFBGBk0x0kRRing
42 simpll2 RRingFBGBk0x0kFB
43 eqid coe1F=coe1F
44 43 4 1 34 coe1f2 FBcoe1F:0BaseR
45 42 44 syl RRingFBGBk0x0kcoe1F:0BaseR
46 elfznn0 x0kx0
47 46 adantl RRingFBGBk0x0kx0
48 45 47 ffvelrnd RRingFBGBk0x0kcoe1FxBaseR
49 simpll3 RRingFBGBk0x0kGB
50 eqid coe1G=coe1G
51 50 4 1 34 coe1f2 GBcoe1G:0BaseR
52 49 51 syl RRingFBGBk0x0kcoe1G:0BaseR
53 fznn0sub x0kkx0
54 53 adantl RRingFBGBk0x0kkx0
55 52 54 ffvelrnd RRingFBGBk0x0kcoe1GkxBaseR
56 34 3 ringcl RRingcoe1FxBaseRcoe1GkxBaseRcoe1Fx·˙coe1GkxBaseR
57 41 48 55 56 syl3anc RRingFBGBk0x0kcoe1Fx·˙coe1GkxBaseR
58 57 fmpttd RRingFBGBk0x0kcoe1Fx·˙coe1Gkx:0kBaseR
59 39 elexi 0kV
60 59 mptex x0kcoe1Fx·˙coe1GkxV
61 funmpt Funx0kcoe1Fx·˙coe1Gkx
62 fvex 0RV
63 60 61 62 3pm3.2i x0kcoe1Fx·˙coe1GkxVFunx0kcoe1Fx·˙coe1Gkx0RV
64 suppssdm x0kcoe1Fx·˙coe1Gkxsupp0Rdomx0kcoe1Fx·˙coe1Gkx
65 eqid x0kcoe1Fx·˙coe1Gkx=x0kcoe1Fx·˙coe1Gkx
66 65 dmmptss domx0kcoe1Fx·˙coe1Gkx0k
67 64 66 sstri x0kcoe1Fx·˙coe1Gkxsupp0R0k
68 39 67 pm3.2i 0kFinx0kcoe1Fx·˙coe1Gkxsupp0R0k
69 suppssfifsupp x0kcoe1Fx·˙coe1GkxVFunx0kcoe1Fx·˙coe1Gkx0RV0kFinx0kcoe1Fx·˙coe1Gkxsupp0R0kfinSupp0Rx0kcoe1Fx·˙coe1Gkx
70 63 68 69 mp2an finSupp0Rx0kcoe1Fx·˙coe1Gkx
71 70 a1i RRingFBGBk0finSupp0Rx0kcoe1Fx·˙coe1Gkx
72 eqid d01𝑜|df1𝑜×k=d01𝑜|df1𝑜×k
73 72 coe1mul2lem2 k0cd01𝑜|df1𝑜×kc:d01𝑜|df1𝑜×k1-1 onto0k
74 73 adantl RRingFBGBk0cd01𝑜|df1𝑜×kc:d01𝑜|df1𝑜×k1-1 onto0k
75 34 35 38 40 58 71 74 gsumf1o RRingFBGBk0Rx=0kcoe1Fx·˙coe1Gkx=Rx0kcoe1Fx·˙coe1Gkxcd01𝑜|df1𝑜×kc
76 breq1 d=cdf1𝑜×kcf1𝑜×k
77 76 elrab cd01𝑜|df1𝑜×kc01𝑜cf1𝑜×k
78 77 simprbi cd01𝑜|df1𝑜×kcf1𝑜×k
79 78 adantl RRingFBGBk0cd01𝑜|df1𝑜×kcf1𝑜×k
80 simplr RRingFBGBk0cd01𝑜|df1𝑜×kk0
81 elrabi cd01𝑜|df1𝑜×kc01𝑜
82 81 adantl RRingFBGBk0cd01𝑜|df1𝑜×kc01𝑜
83 coe1mul2lem1 k0c01𝑜cf1𝑜×kc0k
84 80 82 83 syl2anc RRingFBGBk0cd01𝑜|df1𝑜×kcf1𝑜×kc0k
85 79 84 mpbid RRingFBGBk0cd01𝑜|df1𝑜×kc0k
86 eqidd RRingFBGBk0cd01𝑜|df1𝑜×kc=cd01𝑜|df1𝑜×kc
87 eqidd RRingFBGBk0x0kcoe1Fx·˙coe1Gkx=x0kcoe1Fx·˙coe1Gkx
88 fveq2 x=ccoe1Fx=coe1Fc
89 oveq2 x=ckx=kc
90 89 fveq2d x=ccoe1Gkx=coe1Gkc
91 88 90 oveq12d x=ccoe1Fx·˙coe1Gkx=coe1Fc·˙coe1Gkc
92 85 86 87 91 fmptco RRingFBGBk0x0kcoe1Fx·˙coe1Gkxcd01𝑜|df1𝑜×kc=cd01𝑜|df1𝑜×kcoe1Fc·˙coe1Gkc
93 simpll2 RRingFBGBk0cd01𝑜|df1𝑜×kFB
94 43 fvcoe1 FBc01𝑜Fc=coe1Fc
95 93 82 94 syl2anc RRingFBGBk0cd01𝑜|df1𝑜×kFc=coe1Fc
96 df1o2 1𝑜=
97 0ex V
98 96 6 97 mapsnconst c01𝑜c=1𝑜×c
99 82 98 syl RRingFBGBk0cd01𝑜|df1𝑜×kc=1𝑜×c
100 99 oveq2d RRingFBGBk0cd01𝑜|df1𝑜×k1𝑜×kfc=1𝑜×kf1𝑜×c
101 7 a1i RRingFBGBk0cd01𝑜|df1𝑜×k1𝑜On
102 vex kV
103 102 a1i RRingFBGBk0cd01𝑜|df1𝑜×kkV
104 fvexd RRingFBGBk0cd01𝑜|df1𝑜×kcV
105 101 103 104 ofc12 RRingFBGBk0cd01𝑜|df1𝑜×k1𝑜×kf1𝑜×c=1𝑜×kc
106 100 105 eqtrd RRingFBGBk0cd01𝑜|df1𝑜×k1𝑜×kfc=1𝑜×kc
107 106 fveq2d RRingFBGBk0cd01𝑜|df1𝑜×kG1𝑜×kfc=G1𝑜×kc
108 simpll3 RRingFBGBk0cd01𝑜|df1𝑜×kGB
109 fznn0sub c0kkc0
110 85 109 syl RRingFBGBk0cd01𝑜|df1𝑜×kkc0
111 50 coe1fv GBkc0coe1Gkc=G1𝑜×kc
112 108 110 111 syl2anc RRingFBGBk0cd01𝑜|df1𝑜×kcoe1Gkc=G1𝑜×kc
113 107 112 eqtr4d RRingFBGBk0cd01𝑜|df1𝑜×kG1𝑜×kfc=coe1Gkc
114 95 113 oveq12d RRingFBGBk0cd01𝑜|df1𝑜×kFc·˙G1𝑜×kfc=coe1Fc·˙coe1Gkc
115 114 mpteq2dva RRingFBGBk0cd01𝑜|df1𝑜×kFc·˙G1𝑜×kfc=cd01𝑜|df1𝑜×kcoe1Fc·˙coe1Gkc
116 92 115 eqtr4d RRingFBGBk0x0kcoe1Fx·˙coe1Gkxcd01𝑜|df1𝑜×kc=cd01𝑜|df1𝑜×kFc·˙G1𝑜×kfc
117 116 oveq2d RRingFBGBk0Rx0kcoe1Fx·˙coe1Gkxcd01𝑜|df1𝑜×kc=Rcd01𝑜|df1𝑜×kFc·˙G1𝑜×kfc
118 75 117 eqtrd RRingFBGBk0Rx=0kcoe1Fx·˙coe1Gkx=Rcd01𝑜|df1𝑜×kFc·˙G1𝑜×kfc
119 118 mpteq2dva RRingFBGBk0Rx=0kcoe1Fx·˙coe1Gkx=k0Rcd01𝑜|df1𝑜×kFc·˙G1𝑜×kfc
120 26 33 119 3eqtr4d RRingFBGBcoe1F˙G=k0Rx=0kcoe1Fx·˙coe1Gkx