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