Step | Hyp | Ref
| Expression |
1 | | coe1tmmul.r |
. . 3
โข (๐ โ ๐
โ Ring) |
2 | | coe1tmmul.a |
. . 3
โข (๐ โ ๐ด โ ๐ต) |
3 | | coe1tmmul.c |
. . . 4
โข (๐ โ ๐ถ โ ๐พ) |
4 | | coe1tmmul.d |
. . . 4
โข (๐ โ ๐ท โ
โ0) |
5 | | coe1tm.k |
. . . . 5
โข ๐พ = (Baseโ๐
) |
6 | | coe1tm.p |
. . . . 5
โข ๐ = (Poly1โ๐
) |
7 | | coe1tm.x |
. . . . 5
โข ๐ = (var1โ๐
) |
8 | | coe1tm.m |
. . . . 5
โข ยท = (
ยท๐ โ๐) |
9 | | coe1tm.n |
. . . . 5
โข ๐ = (mulGrpโ๐) |
10 | | coe1tm.e |
. . . . 5
โข โ =
(.gโ๐) |
11 | | coe1tmmul.b |
. . . . 5
โข ๐ต = (Baseโ๐) |
12 | 5, 6, 7, 8, 9, 10,
11 | ply1tmcl 21643 |
. . . 4
โข ((๐
โ Ring โง ๐ถ โ ๐พ โง ๐ท โ โ0) โ (๐ถ ยท (๐ท โ ๐)) โ ๐ต) |
13 | 1, 3, 4, 12 | syl3anc 1371 |
. . 3
โข (๐ โ (๐ถ ยท (๐ท โ ๐)) โ ๐ต) |
14 | | coe1tmmul.t |
. . . 4
โข โ =
(.rโ๐) |
15 | | coe1tmmul.u |
. . . 4
โข ร =
(.rโ๐
) |
16 | 6, 14, 15, 11 | coe1mul 21641 |
. . 3
โข ((๐
โ Ring โง ๐ด โ ๐ต โง (๐ถ ยท (๐ท โ ๐)) โ ๐ต) โ (coe1โ(๐ด โ (๐ถ ยท (๐ท โ ๐)))) = (๐ฅ โ โ0 โฆ (๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))))) |
17 | 1, 2, 13, 16 | syl3anc 1371 |
. 2
โข (๐ โ
(coe1โ(๐ด
โ
(๐ถ ยท (๐ท โ ๐)))) = (๐ฅ โ โ0 โฆ (๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))))) |
18 | | eqeq2 2748 |
. . . 4
โข
((((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ) = if(๐ท โค ๐ฅ, (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ), 0 ) โ ((๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))) = (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ) โ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))) = if(๐ท โค ๐ฅ, (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ), 0 ))) |
19 | | eqeq2 2748 |
. . . 4
โข ( 0 = if(๐ท โค ๐ฅ, (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ), 0 ) โ ((๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))) = 0 โ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))) = if(๐ท โค ๐ฅ, (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ), 0 ))) |
20 | | coe1tm.z |
. . . . . . 7
โข 0 =
(0gโ๐
) |
21 | 1 | adantr 481 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ๐
โ Ring) |
22 | | ringmnd 19974 |
. . . . . . . 8
โข (๐
โ Ring โ ๐
โ Mnd) |
23 | 21, 22 | syl 17 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ๐
โ Mnd) |
24 | | ovex 7390 |
. . . . . . . 8
โข
(0...๐ฅ) โ
V |
25 | 24 | a1i 11 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (0...๐ฅ) โ V) |
26 | | simprr 771 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ๐ท โค ๐ฅ) |
27 | 4 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ๐ท โ
โ0) |
28 | | simprl 769 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ๐ฅ โ โ0) |
29 | | nn0sub 12463 |
. . . . . . . . . 10
โข ((๐ท โ โ0
โง ๐ฅ โ
โ0) โ (๐ท โค ๐ฅ โ (๐ฅ โ ๐ท) โ
โ0)) |
30 | 27, 28, 29 | syl2anc 584 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (๐ท โค ๐ฅ โ (๐ฅ โ ๐ท) โ
โ0)) |
31 | 26, 30 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (๐ฅ โ ๐ท) โ
โ0) |
32 | 27 | nn0ge0d 12476 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ 0 โค ๐ท) |
33 | | nn0re 12422 |
. . . . . . . . . . 11
โข (๐ฅ โ โ0
โ ๐ฅ โ
โ) |
34 | 33 | ad2antrl 726 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ๐ฅ โ โ) |
35 | 4 | nn0red 12474 |
. . . . . . . . . . 11
โข (๐ โ ๐ท โ โ) |
36 | 35 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ๐ท โ โ) |
37 | 34, 36 | subge02d 11747 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (0 โค ๐ท โ (๐ฅ โ ๐ท) โค ๐ฅ)) |
38 | 32, 37 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (๐ฅ โ ๐ท) โค ๐ฅ) |
39 | | fznn0 13533 |
. . . . . . . . 9
โข (๐ฅ โ โ0
โ ((๐ฅ โ ๐ท) โ (0...๐ฅ) โ ((๐ฅ โ ๐ท) โ โ0 โง (๐ฅ โ ๐ท) โค ๐ฅ))) |
40 | 39 | ad2antrl 726 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ((๐ฅ โ ๐ท) โ (0...๐ฅ) โ ((๐ฅ โ ๐ท) โ โ0 โง (๐ฅ โ ๐ท) โค ๐ฅ))) |
41 | 31, 38, 40 | mpbir2and 711 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (๐ฅ โ ๐ท) โ (0...๐ฅ)) |
42 | 1 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ ๐
โ Ring) |
43 | | eqid 2736 |
. . . . . . . . . . . . 13
โข
(coe1โ๐ด) = (coe1โ๐ด) |
44 | 43, 11, 6, 5 | coe1f 21582 |
. . . . . . . . . . . 12
โข (๐ด โ ๐ต โ (coe1โ๐ด):โ0โถ๐พ) |
45 | 2, 44 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ
(coe1โ๐ด):โ0โถ๐พ) |
46 | 45 | ad2antrr 724 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ (coe1โ๐ด):โ0โถ๐พ) |
47 | | elfznn0 13534 |
. . . . . . . . . . 11
โข (๐ฆ โ (0...๐ฅ) โ ๐ฆ โ โ0) |
48 | 47 | adantl 482 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ ๐ฆ โ โ0) |
49 | 46, 48 | ffvelcdmd 7036 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ ((coe1โ๐ด)โ๐ฆ) โ ๐พ) |
50 | | eqid 2736 |
. . . . . . . . . . . . 13
โข
(coe1โ(๐ถ ยท (๐ท โ ๐))) = (coe1โ(๐ถ ยท (๐ท โ ๐))) |
51 | 50, 11, 6, 5 | coe1f 21582 |
. . . . . . . . . . . 12
โข ((๐ถ ยท (๐ท โ ๐)) โ ๐ต โ (coe1โ(๐ถ ยท (๐ท โ ๐))):โ0โถ๐พ) |
52 | 13, 51 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ
(coe1โ(๐ถ
ยท
(๐ท โ ๐))):โ0โถ๐พ) |
53 | 52 | ad2antrr 724 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ (coe1โ(๐ถ ยท (๐ท โ ๐))):โ0โถ๐พ) |
54 | | fznn0sub 13473 |
. . . . . . . . . . 11
โข (๐ฆ โ (0...๐ฅ) โ (๐ฅ โ ๐ฆ) โ
โ0) |
55 | 54 | adantl 482 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ (๐ฅ โ ๐ฆ) โ
โ0) |
56 | 53, 55 | ffvelcdmd 7036 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ ((coe1โ(๐ถ ยท (๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)) โ ๐พ) |
57 | 5, 15 | ringcl 19981 |
. . . . . . . . 9
โข ((๐
โ Ring โง
((coe1โ๐ด)โ๐ฆ) โ ๐พ โง ((coe1โ(๐ถ ยท (๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)) โ ๐พ) โ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))) โ ๐พ) |
58 | 42, 49, 56, 57 | syl3anc 1371 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))) โ ๐พ) |
59 | 58 | fmpttd 7063 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)))):(0...๐ฅ)โถ๐พ) |
60 | 1 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)})) โ ๐
โ Ring) |
61 | 3 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)})) โ ๐ถ โ ๐พ) |
62 | 4 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)})) โ ๐ท โ
โ0) |
63 | | eldifi 4086 |
. . . . . . . . . . . . 13
โข (๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)}) โ ๐ฆ โ (0...๐ฅ)) |
64 | 63, 54 | syl 17 |
. . . . . . . . . . . 12
โข (๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)}) โ (๐ฅ โ ๐ฆ) โ
โ0) |
65 | 64 | adantl 482 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)})) โ (๐ฅ โ ๐ฆ) โ
โ0) |
66 | | eldifsn 4747 |
. . . . . . . . . . . 12
โข (๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)}) โ (๐ฆ โ (0...๐ฅ) โง ๐ฆ โ (๐ฅ โ ๐ท))) |
67 | | simplrl 775 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ ๐ฅ โ โ0) |
68 | 67 | nn0cnd 12475 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ ๐ฅ โ โ) |
69 | 47 | nn0cnd 12475 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ (0...๐ฅ) โ ๐ฆ โ โ) |
70 | 69 | adantl 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ ๐ฆ โ โ) |
71 | 68, 70 | nncand 11517 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ (๐ฅ โ (๐ฅ โ ๐ฆ)) = ๐ฆ) |
72 | 71 | eqcomd 2742 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ ๐ฆ = (๐ฅ โ (๐ฅ โ ๐ฆ))) |
73 | | oveq2 7365 |
. . . . . . . . . . . . . . . 16
โข (๐ท = (๐ฅ โ ๐ฆ) โ (๐ฅ โ ๐ท) = (๐ฅ โ (๐ฅ โ ๐ฆ))) |
74 | 73 | eqeq2d 2747 |
. . . . . . . . . . . . . . 15
โข (๐ท = (๐ฅ โ ๐ฆ) โ (๐ฆ = (๐ฅ โ ๐ท) โ ๐ฆ = (๐ฅ โ (๐ฅ โ ๐ฆ)))) |
75 | 72, 74 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ (๐ท = (๐ฅ โ ๐ฆ) โ ๐ฆ = (๐ฅ โ ๐ท))) |
76 | 75 | necon3d 2964 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ (๐ฆ โ (๐ฅ โ ๐ท) โ ๐ท โ (๐ฅ โ ๐ฆ))) |
77 | 76 | impr 455 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง (๐ฆ โ (0...๐ฅ) โง ๐ฆ โ (๐ฅ โ ๐ท))) โ ๐ท โ (๐ฅ โ ๐ฆ)) |
78 | 66, 77 | sylan2b 594 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)})) โ ๐ท โ (๐ฅ โ ๐ฆ)) |
79 | 20, 5, 6, 7, 8, 9, 10, 60, 61, 62, 65, 78 | coe1tmfv2 21646 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)})) โ ((coe1โ(๐ถ ยท (๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)) = 0 ) |
80 | 79 | oveq2d 7373 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)})) โ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))) = (((coe1โ๐ด)โ๐ฆ) ร 0 )) |
81 | 5, 15, 20 | ringrz 20012 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง
((coe1โ๐ด)โ๐ฆ) โ ๐พ) โ (((coe1โ๐ด)โ๐ฆ) ร 0 ) = 0 ) |
82 | 42, 49, 81 | syl2anc 584 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ (0...๐ฅ)) โ (((coe1โ๐ด)โ๐ฆ) ร 0 ) = 0 ) |
83 | 63, 82 | sylan2 593 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)})) โ (((coe1โ๐ด)โ๐ฆ) ร 0 ) = 0 ) |
84 | 80, 83 | eqtrd 2776 |
. . . . . . . 8
โข (((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โง ๐ฆ โ ((0...๐ฅ) โ {(๐ฅ โ ๐ท)})) โ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))) = 0 ) |
85 | 84, 25 | suppss2 8131 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ((๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)))) supp 0 ) โ {(๐ฅ โ ๐ท)}) |
86 | 5, 20, 23, 25, 41, 59, 85 | gsumpt 19739 |
. . . . . 6
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))) = ((๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))โ(๐ฅ โ ๐ท))) |
87 | | fveq2 6842 |
. . . . . . . . 9
โข (๐ฆ = (๐ฅ โ ๐ท) โ ((coe1โ๐ด)โ๐ฆ) = ((coe1โ๐ด)โ(๐ฅ โ ๐ท))) |
88 | | oveq2 7365 |
. . . . . . . . . 10
โข (๐ฆ = (๐ฅ โ ๐ท) โ (๐ฅ โ ๐ฆ) = (๐ฅ โ (๐ฅ โ ๐ท))) |
89 | 88 | fveq2d 6846 |
. . . . . . . . 9
โข (๐ฆ = (๐ฅ โ ๐ท) โ ((coe1โ(๐ถ ยท (๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)) = ((coe1โ(๐ถ ยท (๐ท โ ๐)))โ(๐ฅ โ (๐ฅ โ ๐ท)))) |
90 | 87, 89 | oveq12d 7375 |
. . . . . . . 8
โข (๐ฆ = (๐ฅ โ ๐ท) โ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))) = (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ (๐ฅ โ ๐ท))))) |
91 | | eqid 2736 |
. . . . . . . 8
โข (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)))) = (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)))) |
92 | | ovex 7390 |
. . . . . . . 8
โข
(((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ (๐ฅ โ ๐ท)))) โ V |
93 | 90, 91, 92 | fvmpt 6948 |
. . . . . . 7
โข ((๐ฅ โ ๐ท) โ (0...๐ฅ) โ ((๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))โ(๐ฅ โ ๐ท)) = (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ (๐ฅ โ ๐ท))))) |
94 | 41, 93 | syl 17 |
. . . . . 6
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ((๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))โ(๐ฅ โ ๐ท)) = (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ (๐ฅ โ ๐ท))))) |
95 | 28 | nn0cnd 12475 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ๐ฅ โ โ) |
96 | 27 | nn0cnd 12475 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ๐ท โ โ) |
97 | 95, 96 | nncand 11517 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (๐ฅ โ (๐ฅ โ ๐ท)) = ๐ท) |
98 | 97 | fveq2d 6846 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ((coe1โ(๐ถ ยท (๐ท โ ๐)))โ(๐ฅ โ (๐ฅ โ ๐ท))) = ((coe1โ(๐ถ ยท (๐ท โ ๐)))โ๐ท)) |
99 | 3 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ๐ถ โ ๐พ) |
100 | 20, 5, 6, 7, 8, 9, 10 | coe1tmfv1 21645 |
. . . . . . . . 9
โข ((๐
โ Ring โง ๐ถ โ ๐พ โง ๐ท โ โ0) โ
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ๐ท) = ๐ถ) |
101 | 21, 99, 27, 100 | syl3anc 1371 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ((coe1โ(๐ถ ยท (๐ท โ ๐)))โ๐ท) = ๐ถ) |
102 | 98, 101 | eqtrd 2776 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ ((coe1โ(๐ถ ยท (๐ท โ ๐)))โ(๐ฅ โ (๐ฅ โ ๐ท))) = ๐ถ) |
103 | 102 | oveq2d 7373 |
. . . . . 6
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ (๐ฅ โ ๐ท)))) = (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ)) |
104 | 86, 94, 103 | 3eqtrd 2780 |
. . . . 5
โข ((๐ โง (๐ฅ โ โ0 โง ๐ท โค ๐ฅ)) โ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))) = (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ)) |
105 | 104 | anassrs 468 |
. . . 4
โข (((๐ โง ๐ฅ โ โ0) โง ๐ท โค ๐ฅ) โ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))) = (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ)) |
106 | 1 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ๐
โ Ring) |
107 | 3 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ๐ถ โ ๐พ) |
108 | 4 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ๐ท โ
โ0) |
109 | 54 | ad2antll 727 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ (๐ฅ โ ๐ฆ) โ
โ0) |
110 | 54 | nn0red 12474 |
. . . . . . . . . . . . 13
โข (๐ฆ โ (0...๐ฅ) โ (๐ฅ โ ๐ฆ) โ โ) |
111 | 110 | ad2antll 727 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ (๐ฅ โ ๐ฆ) โ โ) |
112 | 33 | ad2antlr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ๐ฅ โ โ) |
113 | 35 | ad2antrr 724 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ๐ท โ โ) |
114 | 47 | ad2antll 727 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ๐ฆ โ โ0) |
115 | 114 | nn0ge0d 12476 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ 0 โค ๐ฆ) |
116 | 47 | nn0red 12474 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ (0...๐ฅ) โ ๐ฆ โ โ) |
117 | 116 | ad2antll 727 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ๐ฆ โ โ) |
118 | 112, 117 | subge02d 11747 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ (0 โค ๐ฆ โ (๐ฅ โ ๐ฆ) โค ๐ฅ)) |
119 | 115, 118 | mpbid 231 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ (๐ฅ โ ๐ฆ) โค ๐ฅ) |
120 | | simprl 769 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ยฌ ๐ท โค ๐ฅ) |
121 | 112, 113 | ltnled 11302 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ (๐ฅ < ๐ท โ ยฌ ๐ท โค ๐ฅ)) |
122 | 120, 121 | mpbird 256 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ๐ฅ < ๐ท) |
123 | 111, 112,
113, 119, 122 | lelttrd 11313 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ (๐ฅ โ ๐ฆ) < ๐ท) |
124 | 111, 123 | gtned 11290 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ๐ท โ (๐ฅ โ ๐ฆ)) |
125 | 20, 5, 6, 7, 8, 9, 10, 106, 107, 108, 109, 124 | coe1tmfv2 21646 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ((coe1โ(๐ถ ยท (๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)) = 0 ) |
126 | 125 | oveq2d 7373 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))) = (((coe1โ๐ด)โ๐ฆ) ร 0 )) |
127 | 45 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ (coe1โ๐ด):โ0โถ๐พ) |
128 | 127, 114 | ffvelcdmd 7036 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ ((coe1โ๐ด)โ๐ฆ) โ ๐พ) |
129 | 106, 128,
81 | syl2anc 584 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ (((coe1โ๐ด)โ๐ฆ) ร 0 ) = 0 ) |
130 | 126, 129 | eqtrd 2776 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ โ0) โง (ยฌ
๐ท โค ๐ฅ โง ๐ฆ โ (0...๐ฅ))) โ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))) = 0 ) |
131 | 130 | anassrs 468 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ0) โง ยฌ
๐ท โค ๐ฅ) โง ๐ฆ โ (0...๐ฅ)) โ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))) = 0 ) |
132 | 131 | mpteq2dva 5205 |
. . . . . 6
โข (((๐ โง ๐ฅ โ โ0) โง ยฌ
๐ท โค ๐ฅ) โ (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)))) = (๐ฆ โ (0...๐ฅ) โฆ 0 )) |
133 | 132 | oveq2d 7373 |
. . . . 5
โข (((๐ โง ๐ฅ โ โ0) โง ยฌ
๐ท โค ๐ฅ) โ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))) = (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ 0 ))) |
134 | 1, 22 | syl 17 |
. . . . . . 7
โข (๐ โ ๐
โ Mnd) |
135 | 20 | gsumz 18646 |
. . . . . . 7
โข ((๐
โ Mnd โง (0...๐ฅ) โ V) โ (๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ 0 )) = 0 ) |
136 | 134, 24, 135 | sylancl 586 |
. . . . . 6
โข (๐ โ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ 0 )) = 0 ) |
137 | 136 | ad2antrr 724 |
. . . . 5
โข (((๐ โง ๐ฅ โ โ0) โง ยฌ
๐ท โค ๐ฅ) โ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ 0 )) = 0 ) |
138 | 133, 137 | eqtrd 2776 |
. . . 4
โข (((๐ โง ๐ฅ โ โ0) โง ยฌ
๐ท โค ๐ฅ) โ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))) = 0 ) |
139 | 18, 19, 105, 138 | ifbothda 4524 |
. . 3
โข ((๐ โง ๐ฅ โ โ0) โ (๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ))))) = if(๐ท โค ๐ฅ, (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ), 0 )) |
140 | 139 | mpteq2dva 5205 |
. 2
โข (๐ โ (๐ฅ โ โ0 โฆ (๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐ด)โ๐ฆ) ร
((coe1โ(๐ถ
ยท
(๐ท โ ๐)))โ(๐ฅ โ ๐ฆ)))))) = (๐ฅ โ โ0 โฆ if(๐ท โค ๐ฅ, (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ), 0 ))) |
141 | 17, 140 | eqtrd 2776 |
1
โข (๐ โ
(coe1โ(๐ด
โ
(๐ถ ยท (๐ท โ ๐)))) = (๐ฅ โ โ0 โฆ if(๐ท โค ๐ฅ, (((coe1โ๐ด)โ(๐ฅ โ ๐ท)) ร ๐ถ), 0 ))) |