Step | Hyp | Ref
| Expression |
1 | | ply1mulgsum.p |
. . 3
โข ๐ = (Poly1โ๐
) |
2 | | ply1mulgsum.b |
. . 3
โข ๐ต = (Baseโ๐) |
3 | | ply1mulgsum.a |
. . 3
โข ๐ด = (coe1โ๐พ) |
4 | | ply1mulgsum.c |
. . 3
โข ๐ถ = (coe1โ๐ฟ) |
5 | | ply1mulgsum.x |
. . 3
โข ๐ = (var1โ๐
) |
6 | | ply1mulgsum.pm |
. . 3
โข ร =
(.rโ๐) |
7 | | ply1mulgsum.sm |
. . 3
โข ยท = (
ยท๐ โ๐) |
8 | | ply1mulgsum.rm |
. . 3
โข โ =
(.rโ๐
) |
9 | | ply1mulgsum.m |
. . 3
โข ๐ = (mulGrpโ๐) |
10 | | ply1mulgsum.e |
. . 3
โข โ =
(.gโ๐) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | ply1mulgsumlem1 47020 |
. 2
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ง โ โ0 โ๐ฅ โ โ0
(๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) |
12 | | 2nn0 12485 |
. . . . . . . 8
โข 2 โ
โ0 |
13 | 12 | a1i 11 |
. . . . . . 7
โข (๐ง โ โ0
โ 2 โ โ0) |
14 | | id 22 |
. . . . . . 7
โข (๐ง โ โ0
โ ๐ง โ
โ0) |
15 | 13, 14 | nn0mulcld 12533 |
. . . . . 6
โข (๐ง โ โ0
โ (2 ยท ๐ง)
โ โ0) |
16 | 15 | ad2antrr 724 |
. . . . 5
โข (((๐ง โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โ (2 ยท ๐ง) โ
โ0) |
17 | | breq1 5150 |
. . . . . . . 8
โข (๐ = (2 ยท ๐ง) โ (๐ < ๐ โ (2 ยท ๐ง) < ๐)) |
18 | 17 | imbi1d 341 |
. . . . . . 7
โข (๐ = (2 ยท ๐ง) โ ((๐ < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) โ ((2 ยท ๐ง) < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)))) |
19 | 18 | ralbidv 3177 |
. . . . . 6
โข (๐ = (2 ยท ๐ง) โ (โ๐ โ โ0
(๐ < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) โ โ๐ โ โ0 ((2
ยท ๐ง) < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)))) |
20 | 19 | adantl 482 |
. . . . 5
โข ((((๐ง โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ = (2 ยท ๐ง)) โ (โ๐ โ โ0 (๐ < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) โ โ๐ โ โ0 ((2
ยท ๐ง) < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)))) |
21 | | 2re 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 2 โ
โ |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ง โ โ0
โ 2 โ โ) |
23 | | nn0re 12477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ง โ โ0
โ ๐ง โ
โ) |
24 | 22, 23 | remulcld 11240 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ง โ โ0
โ (2 ยท ๐ง)
โ โ) |
25 | 24 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ (2 ยท ๐ง) โ โ) |
26 | | nn0re 12477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ0
โ ๐ โ
โ) |
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ง โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ ๐ โ โ) |
29 | | elfznn0 13590 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (0...๐) โ ๐ โ โ0) |
30 | | nn0re 12477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ0
โ ๐ โ
โ) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (0...๐) โ ๐ โ โ) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ ๐ โ โ) |
33 | 25, 28, 32 | ltsub1d 11819 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ ((2 ยท ๐ง) < ๐ โ ((2 ยท ๐ง) โ ๐) < (๐ โ ๐))) |
34 | 23 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ ๐ง โ โ) |
35 | 32, 34, 25 | lesub2d 11818 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ (๐ โค ๐ง โ ((2 ยท ๐ง) โ ๐ง) โค ((2 ยท ๐ง) โ ๐))) |
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โง ((2 ยท ๐ง) โ ๐) < (๐ โ ๐)) โ (๐ โค ๐ง โ ((2 ยท ๐ง) โ ๐ง) โค ((2 ยท ๐ง) โ ๐))) |
37 | 24, 23 | resubcld 11638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ง โ โ0
โ ((2 ยท ๐ง)
โ ๐ง) โ
โ) |
38 | 37 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ ((2 ยท ๐ง) โ ๐ง) โ โ) |
39 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ง โ โ0
โง ๐ โ
โ0) โ (2 ยท ๐ง) โ โ) |
40 | | resubcl 11520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((2
ยท ๐ง) โ โ
โง ๐ โ โ)
โ ((2 ยท ๐ง)
โ ๐) โ
โ) |
41 | 39, 31, 40 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ ((2 ยท ๐ง) โ ๐) โ โ) |
42 | | resubcl 11520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โ ๐) โ โ) |
43 | 27, 31, 42 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ (๐ โ ๐) โ โ) |
44 | | lelttr 11300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((2
ยท ๐ง) โ ๐ง) โ โ โง ((2
ยท ๐ง) โ ๐) โ โ โง (๐ โ ๐) โ โ) โ ((((2 ยท ๐ง) โ ๐ง) โค ((2 ยท ๐ง) โ ๐) โง ((2 ยท ๐ง) โ ๐) < (๐ โ ๐)) โ ((2 ยท ๐ง) โ ๐ง) < (๐ โ ๐))) |
45 | 38, 41, 43, 44 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ ((((2 ยท ๐ง) โ ๐ง) โค ((2 ยท ๐ง) โ ๐) โง ((2 ยท ๐ง) โ ๐) < (๐ โ ๐)) โ ((2 ยท ๐ง) โ ๐ง) < (๐ โ ๐))) |
46 | | nn0cn 12478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ง โ โ0
โ ๐ง โ
โ) |
47 | | 2txmxeqx 12348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ง โ โ โ ((2
ยท ๐ง) โ ๐ง) = ๐ง) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ง โ โ0
โ ((2 ยท ๐ง)
โ ๐ง) = ๐ง) |
49 | 48 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ ((2 ยท ๐ง) โ ๐ง) = ๐ง) |
50 | 49 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ (((2 ยท ๐ง) โ ๐ง) < (๐ โ ๐) โ ๐ง < (๐ โ ๐))) |
51 | 45, 50 | sylibd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ ((((2 ยท ๐ง) โ ๐ง) โค ((2 ยท ๐ง) โ ๐) โง ((2 ยท ๐ง) โ ๐) < (๐ โ ๐)) โ ๐ง < (๐ โ ๐))) |
52 | 51 | expcomd 417 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ (((2 ยท ๐ง) โ ๐) < (๐ โ ๐) โ (((2 ยท ๐ง) โ ๐ง) โค ((2 ยท ๐ง) โ ๐) โ ๐ง < (๐ โ ๐)))) |
53 | 52 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โง ((2 ยท ๐ง) โ ๐) < (๐ โ ๐)) โ (((2 ยท ๐ง) โ ๐ง) โค ((2 ยท ๐ง) โ ๐) โ ๐ง < (๐ โ ๐))) |
54 | 36, 53 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โง ((2 ยท ๐ง) โ ๐) < (๐ โ ๐)) โ (๐ โค ๐ง โ ๐ง < (๐ โ ๐))) |
55 | 54 | ex 413 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ (((2 ยท ๐ง) โ ๐) < (๐ โ ๐) โ (๐ โค ๐ง โ ๐ง < (๐ โ ๐)))) |
56 | 33, 55 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง ๐ โ (0...๐)) โ ((2 ยท ๐ง) < ๐ โ (๐ โค ๐ง โ ๐ง < (๐ โ ๐)))) |
57 | 56 | ex 413 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ง โ โ0
โง ๐ โ
โ0) โ (๐ โ (0...๐) โ ((2 ยท ๐ง) < ๐ โ (๐ โค ๐ง โ ๐ง < (๐ โ ๐))))) |
58 | 57 | com23 86 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ง โ โ0
โง ๐ โ
โ0) โ ((2 ยท ๐ง) < ๐ โ (๐ โ (0...๐) โ (๐ โค ๐ง โ ๐ง < (๐ โ ๐))))) |
59 | 58 | ex 413 |
. . . . . . . . . . . . . . . . 17
โข (๐ง โ โ0
โ (๐ โ
โ0 โ ((2 ยท ๐ง) < ๐ โ (๐ โ (0...๐) โ (๐ โค ๐ง โ ๐ง < (๐ โ ๐)))))) |
60 | 59 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
โข (((๐ง โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โ (๐ โ โ0 โ ((2
ยท ๐ง) < ๐ โ (๐ โ (0...๐) โ (๐ โค ๐ง โ ๐ง < (๐ โ ๐)))))) |
61 | 60 | imp41 426 |
. . . . . . . . . . . . . . 15
โข
((((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐)) โ (๐ โค ๐ง โ ๐ง < (๐ โ ๐))) |
62 | 61 | impcom 408 |
. . . . . . . . . . . . . 14
โข ((๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ ๐ง < (๐ โ ๐)) |
63 | | fznn0sub2 13604 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (0...๐) โ (๐ โ ๐) โ (0...๐)) |
64 | | elfznn0 13590 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ ๐) โ (0...๐) โ (๐ โ ๐) โ
โ0) |
65 | | breq2 5151 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ = (๐ โ ๐) โ (๐ง < ๐ฅ โ ๐ง < (๐ โ ๐))) |
66 | | fveqeq2 6897 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ = (๐ โ ๐) โ ((๐ดโ๐ฅ) = (0gโ๐
) โ (๐ดโ(๐ โ ๐)) = (0gโ๐
))) |
67 | | fveqeq2 6897 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ = (๐ โ ๐) โ ((๐ถโ๐ฅ) = (0gโ๐
) โ (๐ถโ(๐ โ ๐)) = (0gโ๐
))) |
68 | 66, 67 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ = (๐ โ ๐) โ (((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)) โ ((๐ดโ(๐ โ ๐)) = (0gโ๐
) โง (๐ถโ(๐ โ ๐)) = (0gโ๐
)))) |
69 | 65, 68 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ = (๐ โ ๐) โ ((๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
))) โ (๐ง < (๐ โ ๐) โ ((๐ดโ(๐ โ ๐)) = (0gโ๐
) โง (๐ถโ(๐ โ ๐)) = (0gโ๐
))))) |
70 | 69 | rspcva 3610 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ ๐) โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โ (๐ง < (๐ โ ๐) โ ((๐ดโ(๐ โ ๐)) = (0gโ๐
) โง (๐ถโ(๐ โ ๐)) = (0gโ๐
)))) |
71 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ดโ(๐ โ ๐)) = (0gโ๐
) โง (๐ถโ(๐ โ ๐)) = (0gโ๐
)) โ (๐ถโ(๐ โ ๐)) = (0gโ๐
)) |
72 | 70, 71 | syl6 35 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ ๐) โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โ (๐ง < (๐ โ ๐) โ (๐ถโ(๐ โ ๐)) = (0gโ๐
))) |
73 | 72 | ex 413 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ ๐) โ โ0 โ
(โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
))) โ (๐ง < (๐ โ ๐) โ (๐ถโ(๐ โ ๐)) = (0gโ๐
)))) |
74 | 63, 64, 73 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (0...๐) โ (โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
))) โ (๐ง < (๐ โ ๐) โ (๐ถโ(๐ โ ๐)) = (0gโ๐
)))) |
75 | 74 | com12 32 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
))) โ (๐ โ (0...๐) โ (๐ง < (๐ โ ๐) โ (๐ถโ(๐ โ ๐)) = (0gโ๐
)))) |
76 | 75 | ad4antlr 731 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โ (๐ โ (0...๐) โ (๐ง < (๐ โ ๐) โ (๐ถโ(๐ โ ๐)) = (0gโ๐
)))) |
77 | 76 | imp 407 |
. . . . . . . . . . . . . . 15
โข
((((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐)) โ (๐ง < (๐ โ ๐) โ (๐ถโ(๐ โ ๐)) = (0gโ๐
))) |
78 | 77 | adantl 482 |
. . . . . . . . . . . . . 14
โข ((๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ (๐ง < (๐ โ ๐) โ (๐ถโ(๐ โ ๐)) = (0gโ๐
))) |
79 | 62, 78 | mpd 15 |
. . . . . . . . . . . . 13
โข ((๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ (๐ถโ(๐ โ ๐)) = (0gโ๐
)) |
80 | 79 | oveq2d 7421 |
. . . . . . . . . . . 12
โข ((๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))) = ((๐ดโ๐) โ
(0gโ๐
))) |
81 | | simplr1 1215 |
. . . . . . . . . . . . . . 15
โข ((((๐ง โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ๐
โ Ring) |
82 | 81 | ad2antrr 724 |
. . . . . . . . . . . . . 14
โข
((((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐)) โ ๐
โ Ring) |
83 | 82 | adantl 482 |
. . . . . . . . . . . . 13
โข ((๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ ๐
โ Ring) |
84 | | simplr2 1216 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ง โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ๐พ โ ๐ต) |
85 | 84 | adantr 481 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โ ๐พ โ ๐ต) |
86 | 85, 29 | anim12i 613 |
. . . . . . . . . . . . . . 15
โข
((((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐)) โ (๐พ โ ๐ต โง ๐ โ
โ0)) |
87 | 86 | adantl 482 |
. . . . . . . . . . . . . 14
โข ((๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ (๐พ โ ๐ต โง ๐ โ
โ0)) |
88 | | eqid 2732 |
. . . . . . . . . . . . . . 15
โข
(Baseโ๐
) =
(Baseโ๐
) |
89 | 3, 2, 1, 88 | coe1fvalcl 21727 |
. . . . . . . . . . . . . 14
โข ((๐พ โ ๐ต โง ๐ โ โ0) โ (๐ดโ๐) โ (Baseโ๐
)) |
90 | 87, 89 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ (๐ดโ๐) โ (Baseโ๐
)) |
91 | | eqid 2732 |
. . . . . . . . . . . . . 14
โข
(0gโ๐
) = (0gโ๐
) |
92 | 88, 8, 91 | ringrz 20101 |
. . . . . . . . . . . . 13
โข ((๐
โ Ring โง (๐ดโ๐) โ (Baseโ๐
)) โ ((๐ดโ๐) โ
(0gโ๐
)) =
(0gโ๐
)) |
93 | 83, 90, 92 | syl2anc 584 |
. . . . . . . . . . . 12
โข ((๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ ((๐ดโ๐) โ
(0gโ๐
)) =
(0gโ๐
)) |
94 | 80, 93 | eqtrd 2772 |
. . . . . . . . . . 11
โข ((๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))) = (0gโ๐
)) |
95 | | ltnle 11289 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ง โ โ โง ๐ โ โ) โ (๐ง < ๐ โ ยฌ ๐ โค ๐ง)) |
96 | 23, 30, 95 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ง โ โ0
โง ๐ โ
โ0) โ (๐ง < ๐ โ ยฌ ๐ โค ๐ง)) |
97 | 96 | bicomd 222 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ง โ โ0
โง ๐ โ
โ0) โ (ยฌ ๐ โค ๐ง โ ๐ง < ๐)) |
98 | 97 | expcom 414 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ (๐ง โ
โ0 โ (ยฌ ๐ โค ๐ง โ ๐ง < ๐))) |
99 | 98, 29 | syl11 33 |
. . . . . . . . . . . . . . . . 17
โข (๐ง โ โ0
โ (๐ โ (0...๐) โ (ยฌ ๐ โค ๐ง โ ๐ง < ๐))) |
100 | 99 | ad4antr 730 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โ (๐ โ (0...๐) โ (ยฌ ๐ โค ๐ง โ ๐ง < ๐))) |
101 | 100 | imp 407 |
. . . . . . . . . . . . . . 15
โข
((((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐)) โ (ยฌ ๐ โค ๐ง โ ๐ง < ๐)) |
102 | | breq2 5151 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ = ๐ โ (๐ง < ๐ฅ โ ๐ง < ๐)) |
103 | | fveqeq2 6897 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ = ๐ โ ((๐ดโ๐ฅ) = (0gโ๐
) โ (๐ดโ๐) = (0gโ๐
))) |
104 | | fveqeq2 6897 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ = ๐ โ ((๐ถโ๐ฅ) = (0gโ๐
) โ (๐ถโ๐) = (0gโ๐
))) |
105 | 103, 104 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ = ๐ โ (((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)) โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))) |
106 | 102, 105 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ = ๐ โ ((๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
))) โ (๐ง < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
))))) |
107 | 106 | rspcva 3610 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โ (๐ง < ๐ โ ((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)))) |
108 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ดโ๐) = (0gโ๐
) โง (๐ถโ๐) = (0gโ๐
)) โ (๐ดโ๐) = (0gโ๐
)) |
109 | 107, 108 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โ (๐ง < ๐ โ (๐ดโ๐) = (0gโ๐
))) |
110 | 109 | ex 413 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ0
โ (โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
))) โ (๐ง < ๐ โ (๐ดโ๐) = (0gโ๐
)))) |
111 | 110, 29 | syl11 33 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
))) โ (๐ โ (0...๐) โ (๐ง < ๐ โ (๐ดโ๐) = (0gโ๐
)))) |
112 | 111 | ad4antlr 731 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โ (๐ โ (0...๐) โ (๐ง < ๐ โ (๐ดโ๐) = (0gโ๐
)))) |
113 | 112 | imp 407 |
. . . . . . . . . . . . . . 15
โข
((((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐)) โ (๐ง < ๐ โ (๐ดโ๐) = (0gโ๐
))) |
114 | 101, 113 | sylbid 239 |
. . . . . . . . . . . . . 14
โข
((((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐)) โ (ยฌ ๐ โค ๐ง โ (๐ดโ๐) = (0gโ๐
))) |
115 | 114 | impcom 408 |
. . . . . . . . . . . . 13
โข ((ยฌ
๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ (๐ดโ๐) = (0gโ๐
)) |
116 | 115 | oveq1d 7420 |
. . . . . . . . . . . 12
โข ((ยฌ
๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))) = ((0gโ๐
) โ (๐ถโ(๐ โ ๐)))) |
117 | 82 | adantl 482 |
. . . . . . . . . . . . 13
โข ((ยฌ
๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ ๐
โ Ring) |
118 | | simplr3 1217 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ง โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ๐ฟ โ ๐ต) |
119 | 118 | adantr 481 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โ ๐ฟ โ ๐ต) |
120 | | fznn0sub 13529 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (0...๐) โ (๐ โ ๐) โ
โ0) |
121 | 119, 120 | anim12i 613 |
. . . . . . . . . . . . . . 15
โข
((((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐)) โ (๐ฟ โ ๐ต โง (๐ โ ๐) โ
โ0)) |
122 | 121 | adantl 482 |
. . . . . . . . . . . . . 14
โข ((ยฌ
๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ (๐ฟ โ ๐ต โง (๐ โ ๐) โ
โ0)) |
123 | 4, 2, 1, 88 | coe1fvalcl 21727 |
. . . . . . . . . . . . . 14
โข ((๐ฟ โ ๐ต โง (๐ โ ๐) โ โ0) โ (๐ถโ(๐ โ ๐)) โ (Baseโ๐
)) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . 13
โข ((ยฌ
๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ (๐ถโ(๐ โ ๐)) โ (Baseโ๐
)) |
125 | 88, 8, 91 | ringlz 20100 |
. . . . . . . . . . . . 13
โข ((๐
โ Ring โง (๐ถโ(๐ โ ๐)) โ (Baseโ๐
)) โ ((0gโ๐
) โ (๐ถโ(๐ โ ๐))) = (0gโ๐
)) |
126 | 117, 124,
125 | syl2anc 584 |
. . . . . . . . . . . 12
โข ((ยฌ
๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ ((0gโ๐
) โ (๐ถโ(๐ โ ๐))) = (0gโ๐
)) |
127 | 116, 126 | eqtrd 2772 |
. . . . . . . . . . 11
โข ((ยฌ
๐ โค ๐ง โง (((((๐ง โ โ0 โง
โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐))) โ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))) = (0gโ๐
)) |
128 | 94, 127 | pm2.61ian 810 |
. . . . . . . . . 10
โข
((((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โง ๐ โ (0...๐)) โ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))) = (0gโ๐
)) |
129 | 128 | mpteq2dva 5247 |
. . . . . . . . 9
โข
(((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โ (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐)))) = (๐ โ (0...๐) โฆ (0gโ๐
))) |
130 | 129 | oveq2d 7421 |
. . . . . . . 8
โข
(((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (๐
ฮฃg (๐ โ (0...๐) โฆ (0gโ๐
)))) |
131 | | ringmnd 20059 |
. . . . . . . . . . . 12
โข (๐
โ Ring โ ๐
โ Mnd) |
132 | 131 | 3ad2ant1 1133 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ ๐
โ Mnd) |
133 | | ovex 7438 |
. . . . . . . . . . 11
โข
(0...๐) โ
V |
134 | 132, 133 | jctir 521 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ (๐
โ Mnd โง (0...๐) โ V)) |
135 | 134 | ad3antlr 729 |
. . . . . . . . 9
โข
(((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โ (๐
โ Mnd โง (0...๐) โ V)) |
136 | 91 | gsumz 18713 |
. . . . . . . . 9
โข ((๐
โ Mnd โง (0...๐) โ V) โ (๐
ฮฃg
(๐ โ (0...๐) โฆ
(0gโ๐
))) =
(0gโ๐
)) |
137 | 135, 136 | syl 17 |
. . . . . . . 8
โข
(((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โ (๐
ฮฃg (๐ โ (0...๐) โฆ (0gโ๐
))) = (0gโ๐
)) |
138 | 130, 137 | eqtrd 2772 |
. . . . . . 7
โข
(((((๐ง โ
โ0 โง โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โง (2
ยท ๐ง) < ๐) โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)) |
139 | 138 | ex 413 |
. . . . . 6
โข ((((๐ง โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โง ๐ โ โ0) โ ((2
ยท ๐ง) < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
))) |
140 | 139 | ralrimiva 3146 |
. . . . 5
โข (((๐ง โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โ โ๐ โ โ0 ((2 ยท
๐ง) < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
))) |
141 | 16, 20, 140 | rspcedvd 3614 |
. . . 4
โข (((๐ง โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โง (๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต)) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
))) |
142 | 141 | ex 413 |
. . 3
โข ((๐ง โ โ0
โง โ๐ฅ โ
โ0 (๐ง <
๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
)))) โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)))) |
143 | 142 | rexlimiva 3147 |
. 2
โข
(โ๐ง โ
โ0 โ๐ฅ โ โ0 (๐ง < ๐ฅ โ ((๐ดโ๐ฅ) = (0gโ๐
) โง (๐ถโ๐ฅ) = (0gโ๐
))) โ ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
)))) |
144 | 11, 143 | mpcom 38 |
1
โข ((๐
โ Ring โง ๐พ โ ๐ต โง ๐ฟ โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐
ฮฃg (๐ โ (0...๐) โฆ ((๐ดโ๐) โ (๐ถโ(๐ โ ๐))))) = (0gโ๐
))) |