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 = ( 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 coe1tmmul2 ( ๐œ‘ โ†’ ( 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 11 16 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 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ๐‘… โˆˆ Ring )
22 ringmnd โŠข ( ๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Mnd )
23 21 22 syl โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ๐‘… โˆˆ Mnd )
24 ovex โŠข ( 0 ... ๐‘ฅ ) โˆˆ V
25 24 a1i โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( 0 ... ๐‘ฅ ) โˆˆ V )
26 simprr โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ๐ท โ‰ค ๐‘ฅ )
27 14 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ๐ท โˆˆ โ„•0 )
28 simprl โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„•0 )
29 nn0sub โŠข ( ( ๐ท โˆˆ โ„•0 โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ๐ท โ‰ค ๐‘ฅ โ†” ( ๐‘ฅ โˆ’ ๐ท ) โˆˆ โ„•0 ) )
30 27 28 29 syl2anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ๐ท โ‰ค ๐‘ฅ โ†” ( ๐‘ฅ โˆ’ ๐ท ) โˆˆ โ„•0 ) )
31 26 30 mpbid โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ๐‘ฅ โˆ’ ๐ท ) โˆˆ โ„•0 )
32 27 nn0ge0d โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ 0 โ‰ค ๐ท )
33 nn0re โŠข ( ๐‘ฅ โˆˆ โ„•0 โ†’ ๐‘ฅ โˆˆ โ„ )
34 33 ad2antrl โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„ )
35 14 nn0red โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„ )
36 35 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ๐ท โˆˆ โ„ )
37 34 36 subge02d โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( 0 โ‰ค ๐ท โ†” ( ๐‘ฅ โˆ’ ๐ท ) โ‰ค ๐‘ฅ ) )
38 32 37 mpbid โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ๐‘ฅ โˆ’ ๐ท ) โ‰ค ๐‘ฅ )
39 fznn0 โŠข ( ๐‘ฅ โˆˆ โ„•0 โ†’ ( ( ๐‘ฅ โˆ’ ๐ท ) โˆˆ ( 0 ... ๐‘ฅ ) โ†” ( ( ๐‘ฅ โˆ’ ๐ท ) โˆˆ โ„•0 โˆง ( ๐‘ฅ โˆ’ ๐ท ) โ‰ค ๐‘ฅ ) ) )
40 39 ad2antrl โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ( ๐‘ฅ โˆ’ ๐ท ) โˆˆ ( 0 ... ๐‘ฅ ) โ†” ( ( ๐‘ฅ โˆ’ ๐ท ) โˆˆ โ„•0 โˆง ( ๐‘ฅ โˆ’ ๐ท ) โ‰ค ๐‘ฅ ) ) )
41 31 38 40 mpbir2and โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ๐‘ฅ โˆ’ ๐ท ) โˆˆ ( 0 ... ๐‘ฅ ) )
42 12 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐‘… โˆˆ Ring )
43 eqid โŠข ( coe1 โ€˜ ๐ด ) = ( coe1 โ€˜ ๐ด )
44 43 8 3 2 coe1f โŠข ( ๐ด โˆˆ ๐ต โ†’ ( coe1 โ€˜ ๐ด ) : โ„•0 โŸถ ๐พ )
45 11 44 syl โŠข ( ๐œ‘ โ†’ ( coe1 โ€˜ ๐ด ) : โ„•0 โŸถ ๐พ )
46 45 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( coe1 โ€˜ ๐ด ) : โ„•0 โŸถ ๐พ )
47 elfznn0 โŠข ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
48 47 adantl โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
49 46 48 ffvelcdmd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) โˆˆ ๐พ )
50 eqid โŠข ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) = ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) )
51 50 8 3 2 coe1f โŠข ( ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) โˆˆ ๐ต โ†’ ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) : โ„•0 โŸถ ๐พ )
52 16 51 syl โŠข ( ๐œ‘ โ†’ ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) : โ„•0 โŸถ ๐พ )
53 52 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) : โ„•0 โŸถ ๐พ )
54 fznn0sub โŠข ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„•0 )
55 54 adantl โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„•0 )
56 53 55 ffvelcdmd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) โˆˆ ๐พ )
57 2 10 ringcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) โˆˆ ๐พ โˆง ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) โˆˆ ๐พ ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) โˆˆ ๐พ )
58 42 49 56 57 syl3anc โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) โˆˆ ๐พ )
59 58 fmpttd โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) : ( 0 ... ๐‘ฅ ) โŸถ ๐พ )
60 12 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) ) โ†’ ๐‘… โˆˆ Ring )
61 13 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) ) โ†’ ๐ถ โˆˆ ๐พ )
62 14 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) ) โ†’ ๐ท โˆˆ โ„•0 )
63 eldifi โŠข ( ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) โ†’ ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) )
64 63 54 syl โŠข ( ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„•0 )
65 64 adantl โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„•0 )
66 eldifsn โŠข ( ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) โ†” ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โˆง ๐‘ฆ โ‰  ( ๐‘ฅ โˆ’ ๐ท ) ) )
67 simplrl โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„•0 )
68 67 nn0cnd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
69 47 nn0cnd โŠข ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†’ ๐‘ฆ โˆˆ โ„‚ )
70 69 adantl โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐‘ฆ โˆˆ โ„‚ )
71 68 70 nncand โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) = ๐‘ฆ )
72 71 eqcomd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ๐‘ฆ = ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) )
73 oveq2 โŠข ( ๐ท = ( ๐‘ฅ โˆ’ ๐‘ฆ ) โ†’ ( ๐‘ฅ โˆ’ ๐ท ) = ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) )
74 73 eqeq2d โŠข ( ๐ท = ( ๐‘ฅ โˆ’ ๐‘ฆ ) โ†’ ( ๐‘ฆ = ( ๐‘ฅ โˆ’ ๐ท ) โ†” ๐‘ฆ = ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) )
75 72 74 syl5ibrcom โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ๐ท = ( ๐‘ฅ โˆ’ ๐‘ฆ ) โ†’ ๐‘ฆ = ( ๐‘ฅ โˆ’ ๐ท ) ) )
76 75 necon3d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ๐‘ฆ โ‰  ( ๐‘ฅ โˆ’ ๐ท ) โ†’ ๐ท โ‰  ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) )
77 76 impr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โˆง ๐‘ฆ โ‰  ( ๐‘ฅ โˆ’ ๐ท ) ) ) โ†’ ๐ท โ‰  ( ๐‘ฅ โˆ’ ๐‘ฆ ) )
78 66 77 sylan2b โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) ) โ†’ ๐ท โ‰  ( ๐‘ฅ โˆ’ ๐‘ฆ ) )
79 1 2 3 4 5 6 7 60 61 62 65 78 coe1tmfv2 โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) = 0 )
80 79 oveq2d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— 0 ) )
81 2 10 1 ringrz โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) โˆˆ ๐พ ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— 0 ) = 0 )
82 42 49 81 syl2anc โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— 0 ) = 0 )
83 63 82 sylan2 โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— 0 ) = 0 )
84 80 83 eqtrd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โˆง ๐‘ฆ โˆˆ ( ( 0 ... ๐‘ฅ ) โˆ– { ( ๐‘ฅ โˆ’ ๐ท ) } ) ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = 0 )
85 84 25 suppss2 โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) supp 0 ) โІ { ( ๐‘ฅ โˆ’ ๐ท ) } )
86 2 1 23 25 41 59 85 gsumpt โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = ( ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) )
87 fveq2 โŠข ( ๐‘ฆ = ( ๐‘ฅ โˆ’ ๐ท ) โ†’ ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) = ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) )
88 oveq2 โŠข ( ๐‘ฆ = ( ๐‘ฅ โˆ’ ๐ท ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) = ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐ท ) ) )
89 88 fveq2d โŠข ( ๐‘ฆ = ( ๐‘ฅ โˆ’ ๐ท ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) = ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐ท ) ) ) )
90 87 89 oveq12d โŠข ( ๐‘ฆ = ( ๐‘ฅ โˆ’ ๐ท ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐ท ) ) ) ) )
91 eqid โŠข ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) = ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) )
92 ovex โŠข ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐ท ) ) ) ) โˆˆ V
93 90 91 92 fvmpt โŠข ( ( ๐‘ฅ โˆ’ ๐ท ) โˆˆ ( 0 ... ๐‘ฅ ) โ†’ ( ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) = ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐ท ) ) ) ) )
94 41 93 syl โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) = ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐ท ) ) ) ) )
95 28 nn0cnd โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
96 27 nn0cnd โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ๐ท โˆˆ โ„‚ )
97 95 96 nncand โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐ท ) ) = ๐ท )
98 97 fveq2d โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐ท ) ) ) = ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) )
99 13 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ๐ถ โˆˆ ๐พ )
100 1 2 3 4 5 6 7 coe1tmfv1 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ถ โˆˆ ๐พ โˆง ๐ท โˆˆ โ„•0 ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) = ๐ถ )
101 21 99 27 100 syl3anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ๐ท ) = ๐ถ )
102 98 101 eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐ท ) ) ) = ๐ถ )
103 102 oveq2d โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ( ๐‘ฅ โˆ’ ๐ท ) ) ) ) = ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ๐ถ ) )
104 86 94 103 3eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐ท โ‰ค ๐‘ฅ ) ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ๐ถ ) )
105 104 anassrs โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ๐ถ ) )
106 12 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ๐‘… โˆˆ Ring )
107 13 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ๐ถ โˆˆ ๐พ )
108 14 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ๐ท โˆˆ โ„•0 )
109 54 ad2antll โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„•0 )
110 54 nn0red โŠข ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„ )
111 110 ad2antll โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„ )
112 33 ad2antlr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ๐‘ฅ โˆˆ โ„ )
113 35 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ๐ท โˆˆ โ„ )
114 47 ad2antll โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ๐‘ฆ โˆˆ โ„•0 )
115 114 nn0ge0d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ 0 โ‰ค ๐‘ฆ )
116 47 nn0red โŠข ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†’ ๐‘ฆ โˆˆ โ„ )
117 116 ad2antll โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ๐‘ฆ โˆˆ โ„ )
118 112 117 subge02d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( 0 โ‰ค ๐‘ฆ โ†” ( ๐‘ฅ โˆ’ ๐‘ฆ ) โ‰ค ๐‘ฅ ) )
119 115 118 mpbid โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โ‰ค ๐‘ฅ )
120 simprl โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ยฌ ๐ท โ‰ค ๐‘ฅ )
121 112 113 ltnled โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( ๐‘ฅ < ๐ท โ†” ยฌ ๐ท โ‰ค ๐‘ฅ ) )
122 120 121 mpbird โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ๐‘ฅ < ๐ท )
123 111 112 113 119 122 lelttrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) < ๐ท )
124 111 123 gtned โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ๐ท โ‰  ( ๐‘ฅ โˆ’ ๐‘ฆ ) )
125 1 2 3 4 5 6 7 106 107 108 109 124 coe1tmfv2 โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) = 0 )
126 125 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— 0 ) )
127 45 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( coe1 โ€˜ ๐ด ) : โ„•0 โŸถ ๐พ )
128 127 114 ffvelcdmd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) โˆˆ ๐พ )
129 106 128 81 syl2anc โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— 0 ) = 0 )
130 126 129 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ( ยฌ ๐ท โ‰ค ๐‘ฅ โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = 0 )
131 130 anassrs โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โˆง ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) ) โ†’ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) = 0 )
132 131 mpteq2dva โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) = ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ 0 ) )
133 132 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ 0 ) ) )
134 12 22 syl โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Mnd )
135 1 gsumz โŠข ( ( ๐‘… โˆˆ Mnd โˆง ( 0 ... ๐‘ฅ ) โˆˆ V ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ 0 ) ) = 0 )
136 134 24 135 sylancl โŠข ( ๐œ‘ โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ 0 ) ) = 0 )
137 136 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ 0 ) ) = 0 )
138 133 137 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โˆง ยฌ ๐ท โ‰ค ๐‘ฅ ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = 0 )
139 19 20 105 138 ifbothda โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) = if ( ๐ท โ‰ค ๐‘ฅ , ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ๐ถ ) , 0 ) )
140 139 mpteq2dva โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ ( ๐‘… ฮฃg ( ๐‘ฆ โˆˆ ( 0 ... ๐‘ฅ ) โ†ฆ ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ๐‘ฆ ) ร— ( ( coe1 โ€˜ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) โ€˜ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) ) ) ) ) = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐ท โ‰ค ๐‘ฅ , ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ๐ถ ) , 0 ) ) )
141 18 140 eqtrd โŠข ( ๐œ‘ โ†’ ( coe1 โ€˜ ( ๐ด โˆ™ ( ๐ถ ยท ( ๐ท โ†‘ ๐‘‹ ) ) ) ) = ( ๐‘ฅ โˆˆ โ„•0 โ†ฆ if ( ๐ท โ‰ค ๐‘ฅ , ( ( ( coe1 โ€˜ ๐ด ) โ€˜ ( ๐‘ฅ โˆ’ ๐ท ) ) ร— ๐ถ ) , 0 ) ) )