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 ) ) ) |