Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))) โ ๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))) |
2 | | pmatcollpw.p |
. . . . . . . . . . 11
โข ๐ = (Poly1โ๐
) |
3 | | pmatcollpw.c |
. . . . . . . . . . 11
โข ๐ถ = (๐ Mat ๐) |
4 | 2, 3 | pmatring 22057 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ถ โ Ring) |
5 | | ringmnd 19979 |
. . . . . . . . . 10
โข (๐ถ โ Ring โ ๐ถ โ Mnd) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ถ โ Mnd) |
7 | 6 | adantr 482 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ ๐ถ โ Mnd) |
8 | | pmatcollpw.b |
. . . . . . . . 9
โข ๐ต = (Baseโ๐ถ) |
9 | | ringcmn 20008 |
. . . . . . . . . . 11
โข (๐ถ โ Ring โ ๐ถ โ CMnd) |
10 | 4, 9 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ถ โ CMnd) |
11 | 10 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ ๐ถ โ CMnd) |
12 | | snfi 8991 |
. . . . . . . . . 10
โข {0}
โ Fin |
13 | 12 | a1i 11 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ {0} โ
Fin) |
14 | | simplll 774 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ ๐ โ Fin) |
15 | | simpllr 775 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ ๐
โ Ring) |
16 | | elmapi 8790 |
. . . . . . . . . . . . 13
โข (๐บ โ (๐ท โm {0}) โ ๐บ:{0}โถ๐ท) |
17 | 16 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ ๐บ:{0}โถ๐ท) |
18 | 17 | ffvelcdmda 7036 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ (๐บโ๐) โ ๐ท) |
19 | | elsni 4604 |
. . . . . . . . . . . . 13
โข (๐ โ {0} โ ๐ = 0) |
20 | | 0nn0 12433 |
. . . . . . . . . . . . 13
โข 0 โ
โ0 |
21 | 19, 20 | eqeltrdi 2842 |
. . . . . . . . . . . 12
โข (๐ โ {0} โ ๐ โ
โ0) |
22 | 21 | adantl 483 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ ๐ โ
โ0) |
23 | | pmatcollpw3.a |
. . . . . . . . . . . 12
โข ๐ด = (๐ Mat ๐
) |
24 | | pmatcollpw3.d |
. . . . . . . . . . . 12
โข ๐ท = (Baseโ๐ด) |
25 | | pmatcollpw.t |
. . . . . . . . . . . 12
โข ๐ = (๐ matToPolyMat ๐
) |
26 | | pmatcollpw.m |
. . . . . . . . . . . 12
โข โ = (
ยท๐ โ๐ถ) |
27 | | pmatcollpw.e |
. . . . . . . . . . . 12
โข โ =
(.gโ(mulGrpโ๐)) |
28 | | pmatcollpw.x |
. . . . . . . . . . . 12
โข ๐ = (var1โ๐
) |
29 | 23, 24, 25, 2, 3, 8,
26, 27, 28 | mat2pmatscmxcl 22105 |
. . . . . . . . . . 11
โข (((๐ โ Fin โง ๐
โ Ring) โง ((๐บโ๐) โ ๐ท โง ๐ โ โ0)) โ ((๐ โ ๐) โ (๐โ(๐บโ๐))) โ ๐ต) |
30 | 14, 15, 18, 22, 29 | syl22anc 838 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ ((๐ โ ๐) โ (๐โ(๐บโ๐))) โ ๐ต) |
31 | 30 | ralrimiva 3140 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ
โ๐ โ {0}
((๐ โ ๐) โ (๐โ(๐บโ๐))) โ ๐ต) |
32 | 8, 11, 13, 31 | gsummptcl 19749 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ (๐ถ ฮฃg
(๐ โ {0} โฆ
((๐ โ ๐) โ (๐โ(๐บโ๐))))) โ ๐ต) |
33 | | eqid 2733 |
. . . . . . . . 9
โข
(+gโ๐ถ) = (+gโ๐ถ) |
34 | | eqid 2733 |
. . . . . . . . 9
โข
(0gโ๐ถ) = (0gโ๐ถ) |
35 | 8, 33, 34 | mndrid 18582 |
. . . . . . . 8
โข ((๐ถ โ Mnd โง (๐ถ ฮฃg
(๐ โ {0} โฆ
((๐ โ ๐) โ (๐โ(๐บโ๐))))) โ ๐ต) โ ((๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))(+gโ๐ถ)(0gโ๐ถ)) = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))) |
36 | 7, 32, 35 | syl2anc 585 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ ((๐ถ ฮฃg
(๐ โ {0} โฆ
((๐ โ ๐) โ (๐โ(๐บโ๐)))))(+gโ๐ถ)(0gโ๐ถ)) = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))) |
37 | | fz0sn 13547 |
. . . . . . . . . . . 12
โข (0...0) =
{0} |
38 | 37 | eqcomi 2742 |
. . . . . . . . . . 11
โข {0} =
(0...0) |
39 | 38 | a1i 11 |
. . . . . . . . . 10
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ {0} =
(0...0)) |
40 | | pmatcollpw3fi1lem1.h |
. . . . . . . . . . . . . 14
โข ๐ป = (๐ โ (0...1) โฆ if(๐ = 0, (๐บโ0), 0 )) |
41 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โง ๐ = ๐) โ ๐ = ๐) |
42 | 19 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โง ๐ = ๐) โ ๐ = 0) |
43 | 41, 42 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โง ๐ = ๐) โ ๐ = 0) |
44 | 43 | iftrued 4495 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โง ๐ = ๐) โ if(๐ = 0, (๐บโ0), 0 ) = (๐บโ0)) |
45 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = 0 โ (๐บโ๐) = (๐บโ0)) |
46 | 45 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 0 โ (๐บโ0) = (๐บโ๐)) |
47 | 19, 46 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {0} โ (๐บโ0) = (๐บโ๐)) |
48 | 47 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โง ๐ = ๐) โ (๐บโ0) = (๐บโ๐)) |
49 | 44, 48 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โง ๐ = ๐) โ if(๐ = 0, (๐บโ0), 0 ) = (๐บโ๐)) |
50 | | 1nn0 12434 |
. . . . . . . . . . . . . . . . . . . 20
โข 1 โ
โ0 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = 0 โ 1 โ
โ0) |
52 | | nn0uz 12810 |
. . . . . . . . . . . . . . . . . . 19
โข
โ0 = (โคโฅโ0) |
53 | 51, 52 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = 0 โ 1 โ
(โคโฅโ0)) |
54 | | eluzfz1 13454 |
. . . . . . . . . . . . . . . . . 18
โข (1 โ
(โคโฅโ0) โ 0 โ (0...1)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 0 โ 0 โ
(0...1)) |
56 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 0 โ (๐ โ (0...1) โ 0 โ
(0...1))) |
57 | 55, 56 | mpbird 257 |
. . . . . . . . . . . . . . . 16
โข (๐ = 0 โ ๐ โ (0...1)) |
58 | 19, 57 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ {0} โ ๐ โ
(0...1)) |
59 | 58 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ ๐ โ
(0...1)) |
60 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . 18
โข ((๐บ:{0}โถ๐ท โง ๐ โ {0}) โ (๐บโ๐) โ ๐ท) |
61 | 60 | ex 414 |
. . . . . . . . . . . . . . . . 17
โข (๐บ:{0}โถ๐ท โ (๐ โ {0} โ (๐บโ๐) โ ๐ท)) |
62 | 16, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐บ โ (๐ท โm {0}) โ (๐ โ {0} โ (๐บโ๐) โ ๐ท)) |
63 | 62 | adantl 483 |
. . . . . . . . . . . . . . 15
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ (๐ โ {0} โ (๐บโ๐) โ ๐ท)) |
64 | 63 | imp 408 |
. . . . . . . . . . . . . 14
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ (๐บโ๐) โ ๐ท) |
65 | 40, 49, 59, 64 | fvmptd2 6957 |
. . . . . . . . . . . . 13
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ (๐ปโ๐) = (๐บโ๐)) |
66 | 65 | eqcomd 2739 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ (๐บโ๐) = (๐ปโ๐)) |
67 | 66 | fveq2d 6847 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ (๐โ(๐บโ๐)) = (๐โ(๐ปโ๐))) |
68 | 67 | oveq2d 7374 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ {0}) โ ((๐ โ ๐) โ (๐โ(๐บโ๐))) = ((๐ โ ๐) โ (๐โ(๐ปโ๐)))) |
69 | 39, 68 | mpteq12dva 5195 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))) = (๐ โ (0...0) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐))))) |
70 | 69 | oveq2d 7374 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ (๐ถ ฮฃg
(๐ โ {0} โฆ
((๐ โ ๐) โ (๐โ(๐บโ๐))))) = (๐ถ ฮฃg (๐ โ (0...0) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))))) |
71 | | ovexd 7393 |
. . . . . . . . . 10
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ (0 + 1)
โ V) |
72 | 8, 34 | mndidcl 18576 |
. . . . . . . . . . . 12
โข (๐ถ โ Mnd โ
(0gโ๐ถ)
โ ๐ต) |
73 | 6, 72 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring) โ
(0gโ๐ถ)
โ ๐ต) |
74 | 73 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ
(0gโ๐ถ)
โ ๐ต) |
75 | | 0p1e1 12280 |
. . . . . . . . . . . . . . . . . . . . 21
โข (0 + 1) =
1 |
76 | 75 | eqeq2i 2746 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (0 + 1) โ ๐ = 1) |
77 | | ax-1ne0 11125 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 1 โ
0 |
78 | 77 | neii 2942 |
. . . . . . . . . . . . . . . . . . . . 21
โข ยฌ 1
= 0 |
79 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = 1 โ (๐ = 0 โ 1 = 0)) |
80 | 78, 79 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = 1 โ ยฌ ๐ = 0) |
81 | 76, 80 | sylbi 216 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (0 + 1) โ ยฌ ๐ = 0) |
82 | 81 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โง ๐ = ๐) โ ยฌ ๐ = 0) |
83 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ (๐ = 0 โ ๐ = 0)) |
84 | 83 | notbid 318 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = ๐ โ (ยฌ ๐ = 0 โ ยฌ ๐ = 0)) |
85 | 84 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โง ๐ = ๐) โ (ยฌ ๐ = 0 โ ยฌ ๐ = 0)) |
86 | 82, 85 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โง ๐ = ๐) โ ยฌ ๐ = 0) |
87 | 86 | iffalsed 4498 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โง ๐ = ๐) โ if(๐ = 0, (๐บโ0), 0 ) = 0 ) |
88 | | pmatcollpw3fi1lem1.0 |
. . . . . . . . . . . . . . . 16
โข 0 =
(0gโ๐ด) |
89 | 87, 88 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โง ๐ = ๐) โ if(๐ = 0, (๐บโ0), 0 ) =
(0gโ๐ด)) |
90 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = 1 โ 1 โ
โ0) |
91 | 90, 52 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = 1 โ 1 โ
(โคโฅโ0)) |
92 | | eluzfz2 13455 |
. . . . . . . . . . . . . . . . . . 19
โข (1 โ
(โคโฅโ0) โ 1 โ (0...1)) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = 1 โ 1 โ
(0...1)) |
94 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = 1 โ (๐ โ (0...1) โ 1 โ
(0...1))) |
95 | 93, 94 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 1 โ ๐ โ (0...1)) |
96 | 76, 95 | sylbi 216 |
. . . . . . . . . . . . . . . 16
โข (๐ = (0 + 1) โ ๐ โ
(0...1)) |
97 | 96 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ ๐ โ
(0...1)) |
98 | | fvexd 6858 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ
(0gโ๐ด)
โ V) |
99 | 40, 89, 97, 98 | fvmptd2 6957 |
. . . . . . . . . . . . . 14
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ (๐ปโ๐) = (0gโ๐ด)) |
100 | 99 | fveq2d 6847 |
. . . . . . . . . . . . 13
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ (๐โ(๐ปโ๐)) = (๐โ(0gโ๐ด))) |
101 | 23 | fveq2i 6846 |
. . . . . . . . . . . . . . . 16
โข
(0gโ๐ด) = (0gโ(๐ Mat ๐
)) |
102 | 3 | fveq2i 6846 |
. . . . . . . . . . . . . . . 16
โข
(0gโ๐ถ) = (0gโ(๐ Mat ๐)) |
103 | 25, 2, 101, 102 | 0mat2pmat 22101 |
. . . . . . . . . . . . . . 15
โข ((๐
โ Ring โง ๐ โ Fin) โ (๐โ(0gโ๐ด)) = (0gโ๐ถ)) |
104 | 103 | ancoms 460 |
. . . . . . . . . . . . . 14
โข ((๐ โ Fin โง ๐
โ Ring) โ (๐โ(0gโ๐ด)) = (0gโ๐ถ)) |
105 | 104 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ (๐โ(0gโ๐ด)) = (0gโ๐ถ)) |
106 | 100, 105 | eqtrd 2773 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ (๐โ(๐ปโ๐)) = (0gโ๐ถ)) |
107 | 106 | oveq2d 7374 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ ((๐ โ ๐) โ (๐โ(๐ปโ๐))) = ((๐ โ ๐) โ
(0gโ๐ถ))) |
108 | 2, 3 | pmatlmod 22058 |
. . . . . . . . . . . . 13
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ถ โ LMod) |
109 | 108 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ ๐ถ โ LMod) |
110 | | simpllr 775 |
. . . . . . . . . . . . . 14
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ ๐
โ Ring) |
111 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
โข (๐ = 1 โ (๐ โ โ0 โ 1 โ
โ0)) |
112 | 90, 111 | mpbird 257 |
. . . . . . . . . . . . . . . 16
โข (๐ = 1 โ ๐ โ โ0) |
113 | 76, 112 | sylbi 216 |
. . . . . . . . . . . . . . 15
โข (๐ = (0 + 1) โ ๐ โ
โ0) |
114 | 113 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ ๐ โ
โ0) |
115 | | eqid 2733 |
. . . . . . . . . . . . . . 15
โข
(mulGrpโ๐) =
(mulGrpโ๐) |
116 | | eqid 2733 |
. . . . . . . . . . . . . . 15
โข
(Baseโ๐) =
(Baseโ๐) |
117 | 2, 28, 115, 27, 116 | ply1moncl 21658 |
. . . . . . . . . . . . . 14
โข ((๐
โ Ring โง ๐ โ โ0)
โ (๐ โ ๐) โ (Baseโ๐)) |
118 | 110, 114,
117 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ (๐ โ ๐) โ (Baseโ๐)) |
119 | 2 | ply1ring 21635 |
. . . . . . . . . . . . . . . . . 18
โข (๐
โ Ring โ ๐ โ Ring) |
120 | 3 | matsca2 21785 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ Fin โง ๐ โ Ring) โ ๐ = (Scalarโ๐ถ)) |
121 | 119, 120 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ = (Scalarโ๐ถ)) |
122 | 121 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ Fin โง ๐
โ Ring) โ
(Scalarโ๐ถ) = ๐) |
123 | 122 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
โข ((๐ โ Fin โง ๐
โ Ring) โ
(Baseโ(Scalarโ๐ถ)) = (Baseโ๐)) |
124 | 123 | eleq2d 2820 |
. . . . . . . . . . . . . 14
โข ((๐ โ Fin โง ๐
โ Ring) โ ((๐ โ ๐) โ (Baseโ(Scalarโ๐ถ)) โ (๐ โ ๐) โ (Baseโ๐))) |
125 | 124 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ ((๐ โ ๐) โ (Baseโ(Scalarโ๐ถ)) โ (๐ โ ๐) โ (Baseโ๐))) |
126 | 118, 125 | mpbird 257 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ (๐ โ ๐) โ (Baseโ(Scalarโ๐ถ))) |
127 | | eqid 2733 |
. . . . . . . . . . . . 13
โข
(Scalarโ๐ถ) =
(Scalarโ๐ถ) |
128 | | eqid 2733 |
. . . . . . . . . . . . 13
โข
(Baseโ(Scalarโ๐ถ)) = (Baseโ(Scalarโ๐ถ)) |
129 | 127, 26, 128, 34 | lmodvs0 20371 |
. . . . . . . . . . . 12
โข ((๐ถ โ LMod โง (๐ โ ๐) โ (Baseโ(Scalarโ๐ถ))) โ ((๐ โ ๐) โ
(0gโ๐ถ)) =
(0gโ๐ถ)) |
130 | 109, 126,
129 | syl2anc 585 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ ((๐ โ ๐) โ
(0gโ๐ถ)) =
(0gโ๐ถ)) |
131 | 107, 130 | eqtrd 2773 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (0 + 1)) โ ((๐ โ ๐) โ (๐โ(๐ปโ๐))) = (0gโ๐ถ)) |
132 | 8, 7, 71, 74, 131 | gsumsnd 19734 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ (๐ถ ฮฃg
(๐ โ {(0 + 1)} โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐))))) = (0gโ๐ถ)) |
133 | 132 | eqcomd 2739 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ
(0gโ๐ถ) =
(๐ถ
ฮฃg (๐ โ {(0 + 1)} โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))))) |
134 | 70, 133 | oveq12d 7376 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ ((๐ถ ฮฃg
(๐ โ {0} โฆ
((๐ โ ๐) โ (๐โ(๐บโ๐)))))(+gโ๐ถ)(0gโ๐ถ)) = ((๐ถ ฮฃg (๐ โ (0...0) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))))(+gโ๐ถ)(๐ถ ฮฃg (๐ โ {(0 + 1)} โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐))))))) |
135 | 36, 134 | eqtr3d 2775 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ (๐ถ ฮฃg
(๐ โ {0} โฆ
((๐ โ ๐) โ (๐โ(๐บโ๐))))) = ((๐ถ ฮฃg (๐ โ (0...0) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))))(+gโ๐ถ)(๐ถ ฮฃg (๐ โ {(0 + 1)} โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐))))))) |
136 | 135 | adantr 482 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))) โ (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐))))) = ((๐ถ ฮฃg (๐ โ (0...0) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))))(+gโ๐ถ)(๐ถ ฮฃg (๐ โ {(0 + 1)} โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐))))))) |
137 | 1, 136 | eqtrd 2773 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))) โ ๐ = ((๐ถ ฮฃg (๐ โ (0...0) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))))(+gโ๐ถ)(๐ถ ฮฃg (๐ โ {(0 + 1)} โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐))))))) |
138 | 137 | 3impa 1111 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0}) โง ๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))) โ ๐ = ((๐ถ ฮฃg (๐ โ (0...0) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))))(+gโ๐ถ)(๐ถ ฮฃg (๐ โ {(0 + 1)} โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐))))))) |
139 | 20 | a1i 11 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ 0 โ
โ0) |
140 | | simplll 774 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ (0...(0 + 1))) โ
๐ โ
Fin) |
141 | | simpllr 775 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ (0...(0 + 1))) โ
๐
โ
Ring) |
142 | | id 22 |
. . . . . . . . . . . . 13
โข (๐บ:{0}โถ๐ท โ ๐บ:{0}โถ๐ท) |
143 | | c0ex 11154 |
. . . . . . . . . . . . . . 15
โข 0 โ
V |
144 | 143 | snid 4623 |
. . . . . . . . . . . . . 14
โข 0 โ
{0} |
145 | 144 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐บ:{0}โถ๐ท โ 0 โ {0}) |
146 | 142, 145 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
โข (๐บ:{0}โถ๐ท โ (๐บโ0) โ ๐ท) |
147 | 16, 146 | syl 17 |
. . . . . . . . . . 11
โข (๐บ โ (๐ท โm {0}) โ (๐บโ0) โ ๐ท) |
148 | 147 | ad2antlr 726 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ (0...1)) โ (๐บโ0) โ ๐ท) |
149 | 23 | matring 21808 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
150 | 24, 88 | ring0cl 19995 |
. . . . . . . . . . . 12
โข (๐ด โ Ring โ 0 โ ๐ท) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring) โ 0 โ ๐ท) |
152 | 151 | ad2antrr 725 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ (0...1)) โ 0 โ ๐ท) |
153 | 148, 152 | ifcld 4533 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ (0...1)) โ if(๐ = 0, (๐บโ0), 0 ) โ ๐ท) |
154 | 153, 40 | fmptd 7063 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ ๐ป:(0...1)โถ๐ท) |
155 | 75 | oveq2i 7369 |
. . . . . . . . 9
โข (0...(0 +
1)) = (0...1) |
156 | 155 | feq2i 6661 |
. . . . . . . 8
โข (๐ป:(0...(0 + 1))โถ๐ท โ ๐ป:(0...1)โถ๐ท) |
157 | 154, 156 | sylibr 233 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ ๐ป:(0...(0 + 1))โถ๐ท) |
158 | 157 | ffvelcdmda 7036 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ (0...(0 + 1))) โ
(๐ปโ๐) โ ๐ท) |
159 | | elfznn0 13540 |
. . . . . . 7
โข (๐ โ (0...(0 + 1)) โ
๐ โ
โ0) |
160 | 159 | adantl 483 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ (0...(0 + 1))) โ
๐ โ
โ0) |
161 | 23, 24, 25, 2, 3, 8,
26, 27, 28 | mat2pmatscmxcl 22105 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง ((๐ปโ๐) โ ๐ท โง ๐ โ โ0)) โ ((๐ โ ๐) โ (๐โ(๐ปโ๐))) โ ๐ต) |
162 | 140, 141,
158, 160, 161 | syl22anc 838 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โง ๐ โ (0...(0 + 1))) โ
((๐ โ ๐) โ (๐โ(๐ปโ๐))) โ ๐ต) |
163 | 8, 33, 11, 139, 162 | gsummptfzsplit 19714 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0})) โ (๐ถ ฮฃg
(๐ โ (0...(0 + 1))
โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐))))) = ((๐ถ ฮฃg (๐ โ (0...0) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))))(+gโ๐ถ)(๐ถ ฮฃg (๐ โ {(0 + 1)} โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐))))))) |
164 | 163 | 3adant3 1133 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0}) โง ๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))) โ (๐ถ ฮฃg (๐ โ (0...(0 + 1)) โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐))))) = ((๐ถ ฮฃg (๐ โ (0...0) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))))(+gโ๐ถ)(๐ถ ฮฃg (๐ โ {(0 + 1)} โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐))))))) |
165 | 138, 164 | eqtr4d 2776 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0}) โง ๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))) โ ๐ = (๐ถ ฮฃg (๐ โ (0...(0 + 1)) โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐)))))) |
166 | 155 | mpteq1i 5202 |
. . 3
โข (๐ โ (0...(0 + 1)) โฆ
((๐ โ ๐) โ (๐โ(๐ปโ๐)))) = (๐ โ (0...1) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))) |
167 | 166 | oveq2i 7369 |
. 2
โข (๐ถ ฮฃg
(๐ โ (0...(0 + 1))
โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐))))) = (๐ถ ฮฃg (๐ โ (0...1) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐))))) |
168 | 165, 167 | eqtrdi 2789 |
1
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐บ โ (๐ท โm {0}) โง ๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐บโ๐)))))) โ ๐ = (๐ถ ฮฃg (๐ โ (0...1) โฆ ((๐ โ ๐) โ (๐โ(๐ปโ๐)))))) |