Metamath Proof Explorer


Theorem coe1tmmul

Description: Coefficient vector of a polynomial multiplied on the left by a term. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses coe1tm.z โŠข 0 = ( 0g โ€˜ ๐‘… )
coe1tm.k โŠข ๐พ = ( Base โ€˜ ๐‘… )
coe1tm.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
coe1tm.x โŠข ๐‘‹ = ( var1 โ€˜ ๐‘… )
coe1tm.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘ƒ )
coe1tm.n โŠข ๐‘ = ( mulGrp โ€˜ ๐‘ƒ )
coe1tm.e โŠข โ†‘ = ( .g โ€˜ ๐‘ )
coe1tmmul.b โŠข ๐ต = ( Base โ€˜ ๐‘ƒ )
coe1tmmul.t โŠข โˆ™ = ( .r โ€˜ ๐‘ƒ )
coe1tmmul.u โŠข ร— = ( .r โ€˜ ๐‘… )
coe1tmmul.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ ๐ต )
coe1tmmul.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
coe1tmmul.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ ๐พ )
coe1tmmul.d โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„•0 )
Assertion coe1tmmul ( ๐œ‘ โ†’ ( coe1 โ€˜ ( ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) โˆ™ ๐ด ) ) = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐ท โ‰ค ๐‘ฅ , ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 coe1tm.z โŠข 0 = ( 0g โ€˜ ๐‘… )
2 coe1tm.k โŠข ๐พ = ( Base โ€˜ ๐‘… )
3 coe1tm.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
4 coe1tm.x โŠข ๐‘‹ = ( var1 โ€˜ ๐‘… )
5 coe1tm.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘ƒ )
6 coe1tm.n โŠข ๐‘ = ( mulGrp โ€˜ ๐‘ƒ )
7 coe1tm.e โŠข โ†‘ = ( .g โ€˜ ๐‘ )
8 coe1tmmul.b โŠข ๐ต = ( Base โ€˜ ๐‘ƒ )
9 coe1tmmul.t โŠข โˆ™ = ( .r โ€˜ ๐‘ƒ )
10 coe1tmmul.u โŠข ร— = ( .r โ€˜ ๐‘… )
11 coe1tmmul.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ ๐ต )
12 coe1tmmul.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
13 coe1tmmul.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ ๐พ )
14 coe1tmmul.d โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„•0 )
15 2 3 4 5 6 7 8 ply1tmcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ถ โˆˆ ๐พ โˆง ๐ท โˆˆ โ„•0 ) โ†’ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) โˆˆ ๐ต )
16 12 13 14 15 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) โˆˆ ๐ต )
17 3 9 10 8 coe1mul โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ต ) โ†’ ( coe1 โ€˜ ( ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) โˆ™ ๐ด ) ) = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) ) )
18 12 16 11 17 syl3anc โŠข ( ๐œ‘ โ†’ ( coe1 โ€˜ ( ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) โˆ™ ๐ด ) ) = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) ) )
19 eqeq2 โŠข ( ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) = if ( ๐ท โ‰ค ๐‘ฅ , ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) , 0 ) โ†’ ( ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) โ†” ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = if ( ๐ท โ‰ค ๐‘ฅ , ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) , 0 ) ) )
20 eqeq2 โŠข ( 0 = if ( ๐ท โ‰ค ๐‘ฅ , ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) , 0 ) โ†’ ( ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = 0 โ†” ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = if ( ๐ท โ‰ค ๐‘ฅ , ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) , 0 ) ) )
21 12 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ๐‘… โˆˆ Ring )
22 ringmnd โŠข ( ๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Mnd )
23 21 22 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ๐‘… โˆˆ Mnd )
24 ovexd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( 0 ... ๐‘ฅ ) โˆˆ V )
25 14 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ๐ท โˆˆ โ„•0 )
26 simpr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ๐ท โ‰ค ๐‘ฅ )
27 fznn0 โŠข ( ๐‘ฅ โˆˆ โ„•0 โ†’ ( ๐ท โˆˆ ( 0 ... ๐‘ฅ ) โ†” ( ๐ท โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) )
28 27 ad2antlr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐ท โˆˆ ( 0 ... ๐‘ฅ ) โ†” ( ๐ท โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) )
29 25 26 28 mpbir2and โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ๐ท โˆˆ ( 0 ... ๐‘ฅ ) )
30 12 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐‘… โˆˆ Ring )
31 eqid โŠข ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) = ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) )
32 31 8 3 2 coe1f โŠข ( ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) โˆˆ ๐ต โ†’ ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) : โ„•0 โŸถ ๐พ )
33 16 32 syl โŠข ( ๐œ‘ โ†’ ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) : โ„•0 โŸถ ๐พ )
34 33 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) : โ„•0 โŸถ ๐พ )
35 elfznn0 โŠข ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
36 ffvelcdm โŠข ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) : โ„•0 โŸถ ๐พ โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) โˆˆ ๐พ )
37 34 35 36 syl2an โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) โˆˆ ๐พ )
38 eqid โŠข ( coe1 โ€˜ ๐ด ) = ( coe1 โ€˜ ๐ด )
39 38 8 3 2 coe1f โŠข ( ๐ด โˆˆ ๐ต โ†’ ( coe1 โ€˜ ๐ด ) : โ„•0 โŸถ ๐พ )
40 11 39 syl โŠข ( ๐œ‘ โ†’ ( coe1 โ€˜ ๐ด ) : โ„•0 โŸถ ๐พ )
41 40 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( coe1 โ€˜ ๐ด ) : โ„•0 โŸถ ๐พ )
42 fznn0sub โŠข ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„•0 )
43 ffvelcdm โŠข ( ( ( coe1 โ€˜ ๐ด ) : โ„•0 โŸถ ๐พ โˆง ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„•0 ) โ†’ ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) โˆˆ ๐พ )
44 41 42 43 syl2an โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) โˆˆ ๐พ )
45 2 10 ringcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) โˆˆ ๐พ โˆง ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) โˆˆ ๐พ ) โ†’ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) โˆˆ ๐พ )
46 30 37 44 45 syl3anc โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) โˆˆ ๐พ )
47 46 fmpttd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) : ( 0 ... ๐‘ฅ ) โŸถ ๐พ )
48 47 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) : ( 0 ... ๐‘ฅ ) โŸถ ๐พ )
49 12 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) ) โ†’ ๐‘… โˆˆ Ring )
50 13 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) ) โ†’ ๐ถ โˆˆ ๐พ )
51 14 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) ) โ†’ ๐ท โˆˆ โ„•0 )
52 eldifi โŠข ( ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) โ†’ ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) )
53 52 35 syl โŠข ( ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
54 53 adantl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
55 eldifsni โŠข ( ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) โ†’ ๐‘ฆ โ‰  ๐ท )
56 55 necomd โŠข ( ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) โ†’ ๐ท โ‰  ๐‘ฆ )
57 56 adantl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) ) โ†’ ๐ท โ‰  ๐‘ฆ )
58 1 2 3 4 5 6 7 49 50 51 54 57 coe1tmfv2 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) = 0 )
59 58 oveq1d โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) ) โ†’ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = ( 0 ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) )
60 2 10 1 ringlz โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) โˆˆ ๐พ ) โ†’ ( 0 ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = 0 )
61 30 44 60 syl2anc โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( 0 ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = 0 )
62 52 61 sylan2 โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) ) โ†’ ( 0 ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = 0 )
63 62 adantlr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) ) โ†’ ( 0 ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = 0 )
64 59 63 eqtrd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ๐ท } ) ) โ†’ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = 0 )
65 64 24 suppss2 โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) supp 0 ) โІ { ๐ท } )
66 2 1 23 24 29 48 65 gsumpt โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = ( ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) โ€˜ ๐ท ) )
67 fveq2 โŠข ( ๐‘ฆ = ๐ท โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) = ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) )
68 oveq2 โŠข ( ๐‘ฆ = ๐ท โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) = ( ๐‘ฅ โˆ’ ๐ท ) )
69 68 fveq2d โŠข ( ๐‘ฆ = ๐ท โ†’ ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) = ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) )
70 67 69 oveq12d โŠข ( ๐‘ฆ = ๐ท โ†’ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) )
71 eqid โŠข ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) = ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) )
72 ovex โŠข ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) โˆˆ V
73 70 71 72 fvmpt โŠข ( ๐ท โˆˆ ( 0 ... ๐‘ฅ ) โ†’ ( ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) โ€˜ ๐ท ) = ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) )
74 29 73 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) โ€˜ ๐ท ) = ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) )
75 1 2 3 4 5 6 7 coe1tmfv1 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ถ โˆˆ ๐พ โˆง ๐ท โˆˆ โ„•0 ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) = ๐ถ )
76 12 13 14 75 syl3anc โŠข ( ๐œ‘ โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) = ๐ถ )
77 76 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) = ๐ถ )
78 77 oveq1d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) = ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) )
79 74 78 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) โ€˜ ๐ท ) = ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) )
80 66 79 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) )
81 12 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐‘… โˆˆ Ring )
82 13 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐ถ โˆˆ ๐พ )
83 14 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐ท โˆˆ โ„•0 )
84 35 adantl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
85 elfzle2 โŠข ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†’ ๐‘ฆ โ‰ค ๐‘ฅ )
86 85 adantl โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐‘ฆ โ‰ค ๐‘ฅ )
87 breq1 โŠข ( ๐ท = ๐‘ฆ โ†’ ( ๐ท โ‰ค ๐‘ฅ โ†” ๐‘ฆ โ‰ค ๐‘ฅ ) )
88 86 87 syl5ibrcom โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ๐ท = ๐‘ฆ โ†’ ๐ท โ‰ค ๐‘ฅ ) )
89 88 necon3bd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ยฌ ๐ท โ‰ค ๐‘ฅ โ†’ ๐ท โ‰  ๐‘ฆ ) )
90 89 imp โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ๐ท โ‰  ๐‘ฆ )
91 90 an32s โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐ท โ‰  ๐‘ฆ )
92 1 2 3 4 5 6 7 81 82 83 84 91 coe1tmfv2 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) = 0 )
93 92 oveq1d โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = ( 0 ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) )
94 61 adantlr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( 0 ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = 0 )
95 93 94 eqtrd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = 0 )
96 95 mpteq2dva โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) = ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ 0 ) )
97 96 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ 0 ) ) )
98 12 22 syl โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Mnd )
99 98 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ๐‘… โˆˆ Mnd )
100 ovexd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ( 0 ... ๐‘ฅ ) โˆˆ V )
101 1 gsumz โŠข ( ( ๐‘… โˆˆ Mnd โˆง ( 0 ... ๐‘ฅ ) โˆˆ V ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ 0 ) ) = 0 )
102 99 100 101 syl2anc โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ 0 ) ) = 0 )
103 97 102 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = 0 )
104 19 20 80 103 ifbothda โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = if ( ๐ท โ‰ค ๐‘ฅ , ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) , 0 ) )
105 104 mpteq2dva โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) ) = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐ท โ‰ค ๐‘ฅ , ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) , 0 ) ) )
106 18 105 eqtrd โŠข ( ๐œ‘ โ†’ ( coe1 โ€˜ ( ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) โˆ™ ๐ด ) ) = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐ท โ‰ค ๐‘ฅ , ( ๐ถ ร— ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ) , 0 ) ) )