Step | Hyp | Ref
| Expression |
1 | | pmatcollpw.p |
. . 3
โข ๐ = (Poly1โ๐
) |
2 | | pmatcollpw.c |
. . 3
โข ๐ถ = (๐ Mat ๐) |
3 | | pmatcollpw.b |
. . 3
โข ๐ต = (Baseโ๐ถ) |
4 | | pmatcollpw.m |
. . 3
โข โ = (
ยท๐ โ๐ถ) |
5 | | pmatcollpw.e |
. . 3
โข โ =
(.gโ(mulGrpโ๐)) |
6 | | pmatcollpw.x |
. . 3
โข ๐ = (var1โ๐
) |
7 | | pmatcollpw.t |
. . 3
โข ๐ = (๐ matToPolyMat ๐
) |
8 | | pmatcollpw3.a |
. . 3
โข ๐ด = (๐ Mat ๐
) |
9 | | pmatcollpw3.d |
. . 3
โข ๐ท = (Baseโ๐ด) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | pmatcollpw3fi 21975 |
. 2
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ0 โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐)))))) |
11 | | df-n0 12276 |
. . . . 5
โข
โ0 = (โ โช {0}) |
12 | 11 | rexeqi 3359 |
. . . 4
โข
(โ๐ โ
โ0 โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โ โ๐ โ (โ โช {0})โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐)))))) |
13 | | rexun 4130 |
. . . 4
โข
(โ๐ โ
(โ โช {0})โ๐
โ (๐ท
โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โ (โ๐ โ โ โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โจ โ๐ โ {0}โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))))) |
14 | 12, 13 | bitri 276 |
. . 3
โข
(โ๐ โ
โ0 โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โ (โ๐ โ โ โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โจ โ๐ โ {0}โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))))) |
15 | | c0ex 11011 |
. . . . . 6
โข 0 โ
V |
16 | | oveq2 7311 |
. . . . . . . . 9
โข (๐ = 0 โ (0...๐ ) = (0...0)) |
17 | | 0z 12372 |
. . . . . . . . . 10
โข 0 โ
โค |
18 | | fzsn 13340 |
. . . . . . . . . 10
โข (0 โ
โค โ (0...0) = {0}) |
19 | 17, 18 | mp1i 13 |
. . . . . . . . 9
โข (๐ = 0 โ (0...0) =
{0}) |
20 | 16, 19 | eqtrd 2776 |
. . . . . . . 8
โข (๐ = 0 โ (0...๐ ) = {0}) |
21 | 20 | oveq2d 7319 |
. . . . . . 7
โข (๐ = 0 โ (๐ท โm (0...๐ )) = (๐ท โm {0})) |
22 | 20 | mpteq1d 5176 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐)))) = (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) |
23 | 22 | oveq2d 7319 |
. . . . . . . 8
โข (๐ = 0 โ (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐โ๐)))))) |
24 | 23 | eqeq2d 2747 |
. . . . . . 7
โข (๐ = 0 โ (๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โ ๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))))) |
25 | 21, 24 | rexeqbidv 3349 |
. . . . . 6
โข (๐ = 0 โ (โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โ โ๐ โ (๐ท โm {0})๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))))) |
26 | 15, 25 | rexsn 4622 |
. . . . 5
โข
(โ๐ โ
{0}โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โ โ๐ โ (๐ท โm {0})๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐โ๐)))))) |
27 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | pmatcollpw3fi1lem2 21977 |
. . . . . 6
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (โ๐ โ (๐ท โm {0})๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โ โ๐ โ โ โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))))) |
28 | 27 | com12 32 |
. . . . 5
โข
(โ๐ โ
(๐ท โm
{0})๐ = (๐ถ ฮฃg (๐ โ {0} โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โ ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))))) |
29 | 26, 28 | sylbi 216 |
. . . 4
โข
(โ๐ โ
{0}โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โ ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))))) |
30 | 29 | jao1i 856 |
. . 3
โข
((โ๐ โ
โ โ๐ โ
(๐ท โm
(0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โจ โ๐ โ {0}โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐)))))) โ ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))))) |
31 | 14, 30 | sylbi 216 |
. 2
โข
(โ๐ โ
โ0 โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))) โ ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐))))))) |
32 | 10, 31 | mpcom 38 |
1
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ท โm (0...๐ ))๐ = (๐ถ ฮฃg (๐ โ (0...๐ ) โฆ ((๐ โ ๐) โ (๐โ(๐โ๐)))))) |