Step | Hyp | Ref
| Expression |
1 | | coe1mul3.r |
. . . 4
โข (๐ โ ๐
โ Ring) |
2 | | coe1mul3.f1 |
. . . 4
โข (๐ โ ๐น โ ๐ต) |
3 | | coe1mul3.g1 |
. . . 4
โข (๐ โ ๐บ โ ๐ต) |
4 | | coe1mul3.s |
. . . . 5
โข ๐ = (Poly1โ๐
) |
5 | | coe1mul3.t |
. . . . 5
โข โ =
(.rโ๐) |
6 | | coe1mul3.u |
. . . . 5
โข ยท =
(.rโ๐
) |
7 | | coe1mul3.b |
. . . . 5
โข ๐ต = (Baseโ๐) |
8 | 4, 5, 6, 7 | coe1mul 21664 |
. . . 4
โข ((๐
โ Ring โง ๐น โ ๐ต โง ๐บ โ ๐ต) โ (coe1โ(๐น โ ๐บ)) = (๐ฅ โ โ0 โฆ (๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ(๐ฅ โ ๐ฆ))))))) |
9 | 1, 2, 3, 8 | syl3anc 1372 |
. . 3
โข (๐ โ
(coe1โ(๐น
โ
๐บ)) = (๐ฅ โ โ0 โฆ (๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ(๐ฅ โ ๐ฆ))))))) |
10 | 9 | fveq1d 6848 |
. 2
โข (๐ โ
((coe1โ(๐น
โ
๐บ))โ(๐ผ + ๐ฝ)) = ((๐ฅ โ โ0 โฆ (๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ(๐ฅ โ ๐ฆ))))))โ(๐ผ + ๐ฝ))) |
11 | | coe1mul3.f2 |
. . . 4
โข (๐ โ ๐ผ โ
โ0) |
12 | | coe1mul3.g2 |
. . . 4
โข (๐ โ ๐ฝ โ
โ0) |
13 | 11, 12 | nn0addcld 12485 |
. . 3
โข (๐ โ (๐ผ + ๐ฝ) โ
โ0) |
14 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = (๐ผ + ๐ฝ) โ (0...๐ฅ) = (0...(๐ผ + ๐ฝ))) |
15 | | fvoveq1 7384 |
. . . . . . 7
โข (๐ฅ = (๐ผ + ๐ฝ) โ ((coe1โ๐บ)โ(๐ฅ โ ๐ฆ)) = ((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) |
16 | 15 | oveq2d 7377 |
. . . . . 6
โข (๐ฅ = (๐ผ + ๐ฝ) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ(๐ฅ โ ๐ฆ))) = (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)))) |
17 | 14, 16 | mpteq12dv 5200 |
. . . . 5
โข (๐ฅ = (๐ผ + ๐ฝ) โ (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ(๐ฅ โ ๐ฆ)))) = (๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))))) |
18 | 17 | oveq2d 7377 |
. . . 4
โข (๐ฅ = (๐ผ + ๐ฝ) โ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ(๐ฅ โ ๐ฆ))))) = (๐
ฮฃg (๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)))))) |
19 | | eqid 2733 |
. . . 4
โข (๐ฅ โ โ0
โฆ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ(๐ฅ โ ๐ฆ)))))) = (๐ฅ โ โ0 โฆ (๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ(๐ฅ โ ๐ฆ)))))) |
20 | | ovex 7394 |
. . . 4
โข (๐
ฮฃg
(๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))))) โ V |
21 | 18, 19, 20 | fvmpt 6952 |
. . 3
โข ((๐ผ + ๐ฝ) โ โ0 โ ((๐ฅ โ โ0
โฆ (๐
ฮฃg (๐ฆ โ (0...๐ฅ) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ(๐ฅ โ ๐ฆ))))))โ(๐ผ + ๐ฝ)) = (๐
ฮฃg (๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)))))) |
22 | 13, 21 | syl 17 |
. 2
โข (๐ โ ((๐ฅ โ โ0 โฆ (๐
ฮฃg
(๐ฆ โ (0...๐ฅ) โฆ
(((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ(๐ฅ โ ๐ฆ))))))โ(๐ผ + ๐ฝ)) = (๐
ฮฃg (๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)))))) |
23 | | eqid 2733 |
. . . 4
โข
(Baseโ๐
) =
(Baseโ๐
) |
24 | | eqid 2733 |
. . . 4
โข
(0gโ๐
) = (0gโ๐
) |
25 | | ringmnd 19982 |
. . . . 5
โข (๐
โ Ring โ ๐
โ Mnd) |
26 | 1, 25 | syl 17 |
. . . 4
โข (๐ โ ๐
โ Mnd) |
27 | | ovexd 7396 |
. . . 4
โข (๐ โ (0...(๐ผ + ๐ฝ)) โ V) |
28 | 11 | nn0red 12482 |
. . . . . 6
โข (๐ โ ๐ผ โ โ) |
29 | | nn0addge1 12467 |
. . . . . 6
โข ((๐ผ โ โ โง ๐ฝ โ โ0)
โ ๐ผ โค (๐ผ + ๐ฝ)) |
30 | 28, 12, 29 | syl2anc 585 |
. . . . 5
โข (๐ โ ๐ผ โค (๐ผ + ๐ฝ)) |
31 | | fznn0 13542 |
. . . . . 6
โข ((๐ผ + ๐ฝ) โ โ0 โ (๐ผ โ (0...(๐ผ + ๐ฝ)) โ (๐ผ โ โ0 โง ๐ผ โค (๐ผ + ๐ฝ)))) |
32 | 13, 31 | syl 17 |
. . . . 5
โข (๐ โ (๐ผ โ (0...(๐ผ + ๐ฝ)) โ (๐ผ โ โ0 โง ๐ผ โค (๐ผ + ๐ฝ)))) |
33 | 11, 30, 32 | mpbir2and 712 |
. . . 4
โข (๐ โ ๐ผ โ (0...(๐ผ + ๐ฝ))) |
34 | 1 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ๐
โ Ring) |
35 | | eqid 2733 |
. . . . . . . . 9
โข
(coe1โ๐น) = (coe1โ๐น) |
36 | 35, 7, 4, 23 | coe1f 21605 |
. . . . . . . 8
โข (๐น โ ๐ต โ (coe1โ๐น):โ0โถ(Baseโ๐
)) |
37 | 2, 36 | syl 17 |
. . . . . . 7
โข (๐ โ
(coe1โ๐น):โ0โถ(Baseโ๐
)) |
38 | | elfznn0 13543 |
. . . . . . 7
โข (๐ฆ โ (0...(๐ผ + ๐ฝ)) โ ๐ฆ โ โ0) |
39 | | ffvelcdm 7036 |
. . . . . . 7
โข
(((coe1โ๐น):โ0โถ(Baseโ๐
) โง ๐ฆ โ โ0) โ
((coe1โ๐น)โ๐ฆ) โ (Baseโ๐
)) |
40 | 37, 38, 39 | syl2an 597 |
. . . . . 6
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ((coe1โ๐น)โ๐ฆ) โ (Baseโ๐
)) |
41 | | eqid 2733 |
. . . . . . . . 9
โข
(coe1โ๐บ) = (coe1โ๐บ) |
42 | 41, 7, 4, 23 | coe1f 21605 |
. . . . . . . 8
โข (๐บ โ ๐ต โ (coe1โ๐บ):โ0โถ(Baseโ๐
)) |
43 | 3, 42 | syl 17 |
. . . . . . 7
โข (๐ โ
(coe1โ๐บ):โ0โถ(Baseโ๐
)) |
44 | | fznn0sub 13482 |
. . . . . . 7
โข (๐ฆ โ (0...(๐ผ + ๐ฝ)) โ ((๐ผ + ๐ฝ) โ ๐ฆ) โ
โ0) |
45 | | ffvelcdm 7036 |
. . . . . . 7
โข
(((coe1โ๐บ):โ0โถ(Baseโ๐
) โง ((๐ผ + ๐ฝ) โ ๐ฆ) โ โ0) โ
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)) โ (Baseโ๐
)) |
46 | 43, 44, 45 | syl2an 597 |
. . . . . 6
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)) โ (Baseโ๐
)) |
47 | 23, 6 | ringcl 19989 |
. . . . . 6
โข ((๐
โ Ring โง
((coe1โ๐น)โ๐ฆ) โ (Baseโ๐
) โง ((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)) โ (Baseโ๐
)) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) โ (Baseโ๐
)) |
48 | 34, 40, 46, 47 | syl3anc 1372 |
. . . . 5
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) โ (Baseโ๐
)) |
49 | 48 | fmpttd 7067 |
. . . 4
โข (๐ โ (๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)))):(0...(๐ผ + ๐ฝ))โถ(Baseโ๐
)) |
50 | | eldifsn 4751 |
. . . . . 6
โข (๐ฆ โ ((0...(๐ผ + ๐ฝ)) โ {๐ผ}) โ (๐ฆ โ (0...(๐ผ + ๐ฝ)) โง ๐ฆ โ ๐ผ)) |
51 | 38 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ๐ฆ โ โ0) |
52 | 51 | nn0red 12482 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ๐ฆ โ โ) |
53 | 28 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ๐ผ โ โ) |
54 | 52, 53 | lttri2d 11302 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ (๐ฆ โ ๐ผ โ (๐ฆ < ๐ผ โจ ๐ผ < ๐ฆ))) |
55 | 3 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ ๐บ โ ๐ต) |
56 | 44 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ((๐ผ + ๐ฝ) โ ๐ฆ) โ
โ0) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ ((๐ผ + ๐ฝ) โ ๐ฆ) โ
โ0) |
58 | | coe1mul3.d |
. . . . . . . . . . . . . . . . 17
โข ๐ท = ( deg1
โ๐
) |
59 | 58, 4, 7 | deg1xrcl 25470 |
. . . . . . . . . . . . . . . 16
โข (๐บ โ ๐ต โ (๐ทโ๐บ) โ
โ*) |
60 | 3, 59 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ทโ๐บ) โ
โ*) |
61 | 60 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ (๐ทโ๐บ) โ
โ*) |
62 | 12 | nn0red 12482 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ฝ โ โ) |
63 | 62 | rexrd 11213 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ฝ โ
โ*) |
64 | 63 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ ๐ฝ โ
โ*) |
65 | 13 | nn0red 12482 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ผ + ๐ฝ) โ โ) |
66 | 65 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ (๐ผ + ๐ฝ) โ โ) |
67 | 66, 52 | resubcld 11591 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ((๐ผ + ๐ฝ) โ ๐ฆ) โ โ) |
68 | 67 | rexrd 11213 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ((๐ผ + ๐ฝ) โ ๐ฆ) โ
โ*) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ ((๐ผ + ๐ฝ) โ ๐ฆ) โ
โ*) |
70 | | coe1mul3.g3 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ทโ๐บ) โค ๐ฝ) |
71 | 70 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ (๐ทโ๐บ) โค ๐ฝ) |
72 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ๐ฝ โ โ) |
73 | 52, 53, 72 | ltadd1d 11756 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ (๐ฆ < ๐ผ โ (๐ฆ + ๐ฝ) < (๐ผ + ๐ฝ))) |
74 | 52, 72, 66 | ltaddsub2d 11764 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ((๐ฆ + ๐ฝ) < (๐ผ + ๐ฝ) โ ๐ฝ < ((๐ผ + ๐ฝ) โ ๐ฆ))) |
75 | 73, 74 | bitrd 279 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ (๐ฆ < ๐ผ โ ๐ฝ < ((๐ผ + ๐ฝ) โ ๐ฆ))) |
76 | 75 | biimpa 478 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ ๐ฝ < ((๐ผ + ๐ฝ) โ ๐ฆ)) |
77 | 61, 64, 69, 71, 76 | xrlelttrd 13088 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ (๐ทโ๐บ) < ((๐ผ + ๐ฝ) โ ๐ฆ)) |
78 | 58, 4, 7, 24, 41 | deg1lt 25485 |
. . . . . . . . . . . . 13
โข ((๐บ โ ๐ต โง ((๐ผ + ๐ฝ) โ ๐ฆ) โ โ0 โง (๐ทโ๐บ) < ((๐ผ + ๐ฝ) โ ๐ฆ)) โ ((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)) = (0gโ๐
)) |
79 | 55, 57, 77, 78 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ ((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)) = (0gโ๐
)) |
80 | 79 | oveq2d 7377 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (((coe1โ๐น)โ๐ฆ) ยท
(0gโ๐
))) |
81 | 23, 6, 24 | ringrz 20020 |
. . . . . . . . . . . . 13
โข ((๐
โ Ring โง
((coe1โ๐น)โ๐ฆ) โ (Baseโ๐
)) โ (((coe1โ๐น)โ๐ฆ) ยท
(0gโ๐
)) =
(0gโ๐
)) |
82 | 34, 40, 81 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ (((coe1โ๐น)โ๐ฆ) ยท
(0gโ๐
)) =
(0gโ๐
)) |
83 | 82 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ (((coe1โ๐น)โ๐ฆ) ยท
(0gโ๐
)) =
(0gโ๐
)) |
84 | 80, 83 | eqtrd 2773 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ฆ < ๐ผ) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (0gโ๐
)) |
85 | 2 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ ๐น โ ๐ต) |
86 | 51 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ ๐ฆ โ โ0) |
87 | 58, 4, 7 | deg1xrcl 25470 |
. . . . . . . . . . . . . . . 16
โข (๐น โ ๐ต โ (๐ทโ๐น) โ
โ*) |
88 | 2, 87 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ทโ๐น) โ
โ*) |
89 | 88 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ (๐ทโ๐น) โ
โ*) |
90 | 28 | rexrd 11213 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ผ โ
โ*) |
91 | 90 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ ๐ผ โ
โ*) |
92 | 52 | rexrd 11213 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ๐ฆ โ โ*) |
93 | 92 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ ๐ฆ โ โ*) |
94 | | coe1mul3.f3 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ทโ๐น) โค ๐ผ) |
95 | 94 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ (๐ทโ๐น) โค ๐ผ) |
96 | | simpr 486 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ ๐ผ < ๐ฆ) |
97 | 89, 91, 93, 95, 96 | xrlelttrd 13088 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ (๐ทโ๐น) < ๐ฆ) |
98 | 58, 4, 7, 24, 35 | deg1lt 25485 |
. . . . . . . . . . . . 13
โข ((๐น โ ๐ต โง ๐ฆ โ โ0 โง (๐ทโ๐น) < ๐ฆ) โ ((coe1โ๐น)โ๐ฆ) = (0gโ๐
)) |
99 | 85, 86, 97, 98 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ ((coe1โ๐น)โ๐ฆ) = (0gโ๐
)) |
100 | 99 | oveq1d 7376 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = ((0gโ๐
) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)))) |
101 | 23, 6, 24 | ringlz 20019 |
. . . . . . . . . . . . 13
โข ((๐
โ Ring โง
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)) โ (Baseโ๐
)) โ ((0gโ๐
) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (0gโ๐
)) |
102 | 34, 46, 101 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ((0gโ๐
) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (0gโ๐
)) |
103 | 102 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ ((0gโ๐
) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (0gโ๐
)) |
104 | 100, 103 | eqtrd 2773 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง ๐ผ < ๐ฆ) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (0gโ๐
)) |
105 | 84, 104 | jaodan 957 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โง (๐ฆ < ๐ผ โจ ๐ผ < ๐ฆ)) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (0gโ๐
)) |
106 | 105 | ex 414 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ ((๐ฆ < ๐ผ โจ ๐ผ < ๐ฆ) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (0gโ๐
))) |
107 | 54, 106 | sylbid 239 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ (0...(๐ผ + ๐ฝ))) โ (๐ฆ โ ๐ผ โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (0gโ๐
))) |
108 | 107 | impr 456 |
. . . . . 6
โข ((๐ โง (๐ฆ โ (0...(๐ผ + ๐ฝ)) โง ๐ฆ โ ๐ผ)) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (0gโ๐
)) |
109 | 50, 108 | sylan2b 595 |
. . . . 5
โข ((๐ โง ๐ฆ โ ((0...(๐ผ + ๐ฝ)) โ {๐ผ})) โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (0gโ๐
)) |
110 | 109, 27 | suppss2 8135 |
. . . 4
โข (๐ โ ((๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)))) supp (0gโ๐
)) โ {๐ผ}) |
111 | 23, 24, 26, 27, 33, 49, 110 | gsumpt 19747 |
. . 3
โข (๐ โ (๐
ฮฃg (๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))))) = ((๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))))โ๐ผ)) |
112 | | fveq2 6846 |
. . . . . 6
โข (๐ฆ = ๐ผ โ ((coe1โ๐น)โ๐ฆ) = ((coe1โ๐น)โ๐ผ)) |
113 | | oveq2 7369 |
. . . . . . 7
โข (๐ฆ = ๐ผ โ ((๐ผ + ๐ฝ) โ ๐ฆ) = ((๐ผ + ๐ฝ) โ ๐ผ)) |
114 | 113 | fveq2d 6850 |
. . . . . 6
โข (๐ฆ = ๐ผ โ ((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)) = ((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ผ))) |
115 | 112, 114 | oveq12d 7379 |
. . . . 5
โข (๐ฆ = ๐ผ โ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))) = (((coe1โ๐น)โ๐ผ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ผ)))) |
116 | | eqid 2733 |
. . . . 5
โข (๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)))) = (๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ)))) |
117 | | ovex 7394 |
. . . . 5
โข
(((coe1โ๐น)โ๐ผ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ผ))) โ V |
118 | 115, 116,
117 | fvmpt 6952 |
. . . 4
โข (๐ผ โ (0...(๐ผ + ๐ฝ)) โ ((๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))))โ๐ผ) = (((coe1โ๐น)โ๐ผ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ผ)))) |
119 | 33, 118 | syl 17 |
. . 3
โข (๐ โ ((๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))))โ๐ผ) = (((coe1โ๐น)โ๐ผ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ผ)))) |
120 | 11 | nn0cnd 12483 |
. . . . . 6
โข (๐ โ ๐ผ โ โ) |
121 | 12 | nn0cnd 12483 |
. . . . . 6
โข (๐ โ ๐ฝ โ โ) |
122 | 120, 121 | pncan2d 11522 |
. . . . 5
โข (๐ โ ((๐ผ + ๐ฝ) โ ๐ผ) = ๐ฝ) |
123 | 122 | fveq2d 6850 |
. . . 4
โข (๐ โ
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ผ)) = ((coe1โ๐บ)โ๐ฝ)) |
124 | 123 | oveq2d 7377 |
. . 3
โข (๐ โ
(((coe1โ๐น)โ๐ผ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ผ))) = (((coe1โ๐น)โ๐ผ) ยท
((coe1โ๐บ)โ๐ฝ))) |
125 | 111, 119,
124 | 3eqtrd 2777 |
. 2
โข (๐ โ (๐
ฮฃg (๐ฆ โ (0...(๐ผ + ๐ฝ)) โฆ (((coe1โ๐น)โ๐ฆ) ยท
((coe1โ๐บ)โ((๐ผ + ๐ฝ) โ ๐ฆ))))) = (((coe1โ๐น)โ๐ผ) ยท
((coe1โ๐บ)โ๐ฝ))) |
126 | 10, 22, 125 | 3eqtrd 2777 |
1
โข (๐ โ
((coe1โ(๐น
โ
๐บ))โ(๐ผ + ๐ฝ)) = (((coe1โ๐น)โ๐ผ) ยท
((coe1โ๐บ)โ๐ฝ))) |