Step | Hyp | Ref
| Expression |
1 | | cpmadumatpoly.a |
. . 3
โข ๐ด = (๐ Mat ๐
) |
2 | | cpmadumatpoly.b |
. . 3
โข ๐ต = (Baseโ๐ด) |
3 | | cpmadumatpoly.p |
. . 3
โข ๐ = (Poly1โ๐
) |
4 | | cpmadumatpoly.y |
. . 3
โข ๐ = (๐ Mat ๐) |
5 | | cpmadumatpoly.t |
. . 3
โข ๐ = (๐ matToPolyMat ๐
) |
6 | | cpmadumatpoly.z |
. . 3
โข ๐ = (var1โ๐
) |
7 | | eqid 2732 |
. . 3
โข
(.gโ(mulGrpโ๐)) =
(.gโ(mulGrpโ๐)) |
8 | | cpmadumatpoly.m1 |
. . 3
โข ยท = (
ยท๐ โ๐) |
9 | | cpmadumatpoly.r |
. . 3
โข ร =
(.rโ๐) |
10 | | cpmadumatpoly.1 |
. . 3
โข 1 =
(1rโ๐) |
11 | | eqid 2732 |
. . 3
โข
(+gโ๐) = (+gโ๐) |
12 | | cpmadumatpoly.m0 |
. . 3
โข โ =
(-gโ๐) |
13 | | cpmadumatpoly.d |
. . 3
โข ๐ท = ((๐ ยท 1 ) โ (๐โ๐)) |
14 | | cpmadumatpoly.j |
. . 3
โข ๐ฝ = (๐ maAdju ๐) |
15 | | cpmadumatpoly.0 |
. . 3
โข 0 =
(0gโ๐) |
16 | | cpmadumatpoly.g |
. . . 4
โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) |
17 | | eqeq1 2736 |
. . . . . 6
โข (๐ = ๐ง โ (๐ = 0 โ ๐ง = 0)) |
18 | | eqeq1 2736 |
. . . . . . 7
โข (๐ = ๐ง โ (๐ = (๐ + 1) โ ๐ง = (๐ + 1))) |
19 | | breq2 5152 |
. . . . . . . 8
โข (๐ = ๐ง โ ((๐ + 1) < ๐ โ (๐ + 1) < ๐ง)) |
20 | | fvoveq1 7431 |
. . . . . . . . . 10
โข (๐ = ๐ง โ (๐โ(๐ โ 1)) = (๐โ(๐ง โ 1))) |
21 | 20 | fveq2d 6895 |
. . . . . . . . 9
โข (๐ = ๐ง โ (๐โ(๐โ(๐ โ 1))) = (๐โ(๐โ(๐ง โ 1)))) |
22 | | 2fveq3 6896 |
. . . . . . . . . 10
โข (๐ = ๐ง โ (๐โ(๐โ๐)) = (๐โ(๐โ๐ง))) |
23 | 22 | oveq2d 7424 |
. . . . . . . . 9
โข (๐ = ๐ง โ ((๐โ๐) ร (๐โ(๐โ๐))) = ((๐โ๐) ร (๐โ(๐โ๐ง)))) |
24 | 21, 23 | oveq12d 7426 |
. . . . . . . 8
โข (๐ = ๐ง โ ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))) = ((๐โ(๐โ(๐ง โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐ง))))) |
25 | 19, 24 | ifbieq2d 4554 |
. . . . . . 7
โข (๐ = ๐ง โ if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐))))) = if((๐ + 1) < ๐ง, 0 , ((๐โ(๐โ(๐ง โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐ง)))))) |
26 | 18, 25 | ifbieq2d 4554 |
. . . . . 6
โข (๐ = ๐ง โ if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))) = if(๐ง = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐ง, 0 , ((๐โ(๐โ(๐ง โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐ง))))))) |
27 | 17, 26 | ifbieq2d 4554 |
. . . . 5
โข (๐ = ๐ง โ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐))))))) = if(๐ง = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ง = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐ง, 0 , ((๐โ(๐โ(๐ง โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐ง)))))))) |
28 | 27 | cbvmptv 5261 |
. . . 4
โข (๐ โ โ0
โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) = (๐ง โ โ0 โฆ if(๐ง = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ง = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐ง, 0 , ((๐โ(๐โ(๐ง โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐ง)))))))) |
29 | 16, 28 | eqtri 2760 |
. . 3
โข ๐บ = (๐ง โ โ0 โฆ if(๐ง = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ง = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐ง, 0 , ((๐โ(๐โ(๐ง โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐ง)))))))) |
30 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 29 | cpmadugsum 22379 |
. 2
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ท ร (๐ฝโ๐ท)) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐บโ๐))))) |
31 | | simp1 1136 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ ๐ โ Fin) |
32 | 31 | ad3antrrr 728 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ โ0) โ ๐ โ Fin) |
33 | | crngring 20067 |
. . . . . . . . . . . . 13
โข (๐
โ CRing โ ๐
โ Ring) |
34 | 33 | 3ad2ant2 1134 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ ๐
โ Ring) |
35 | 34 | ad3antrrr 728 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ โ0) โ ๐
โ Ring) |
36 | | cpmadumatpoly.s |
. . . . . . . . . . . . . . 15
โข ๐ = (๐ ConstPolyMat ๐
) |
37 | 1, 2, 3, 4, 9, 12,
15, 5, 16, 36 | chfacfisfcpmat 22356 |
. . . . . . . . . . . . . 14
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ๐บ:โ0โถ๐) |
38 | 33, 37 | syl3anl2 1413 |
. . . . . . . . . . . . 13
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ ๐บ:โ0โถ๐) |
39 | 38 | anassrs 468 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ ๐บ:โ0โถ๐) |
40 | 39 | ffvelcdmda 7086 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ โ0) โ (๐บโ๐) โ ๐) |
41 | | cpmadumatpoly.u |
. . . . . . . . . . . 12
โข ๐ = (๐ cPolyMatToMat ๐
) |
42 | 36, 41, 5 | m2cpminvid2 22256 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring โง (๐บโ๐) โ ๐) โ (๐โ(๐โ(๐บโ๐))) = (๐บโ๐)) |
43 | 32, 35, 40, 42 | syl3anc 1371 |
. . . . . . . . . 10
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ โ0) โ (๐โ(๐โ(๐บโ๐))) = (๐บโ๐)) |
44 | 43 | eqcomd 2738 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ โ0) โ (๐บโ๐) = (๐โ(๐โ(๐บโ๐)))) |
45 | 44 | oveq2d 7424 |
. . . . . . . 8
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ โ0) โ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐บโ๐)) = ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐))))) |
46 | 45 | mpteq2dva 5248 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ โ โ0 โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐บโ๐))) = (๐ โ โ0 โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐)))))) |
47 | 46 | oveq2d 7424 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐บโ๐)))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐))))))) |
48 | 47 | eqeq2d 2743 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ ((๐ท ร (๐ฝโ๐ท)) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐บโ๐)))) โ (๐ท ร (๐ฝโ๐ท)) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐)))))))) |
49 | | fveq2 6891 |
. . . . . . 7
โข ((๐ท ร (๐ฝโ๐ท)) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐)))))) โ (๐ผโ(๐ท ร (๐ฝโ๐ท))) = (๐ผโ(๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐)))))))) |
50 | | 3simpa 1148 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (๐ โ Fin โง ๐
โ CRing)) |
51 | 50 | ad2antrr 724 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ โ Fin โง ๐
โ CRing)) |
52 | | cpmadumatpoly.w |
. . . . . . . . . 10
โข ๐ = (Baseโ๐) |
53 | | cpmadumatpoly.q |
. . . . . . . . . 10
โข ๐ = (Poly1โ๐ด) |
54 | | cpmadumatpoly.x |
. . . . . . . . . 10
โข ๐ = (var1โ๐ด) |
55 | | cpmadumatpoly.m2 |
. . . . . . . . . 10
โข โ = (
ยท๐ โ๐) |
56 | | cpmadumatpoly.e |
. . . . . . . . . 10
โข โ =
(.gโ(mulGrpโ๐)) |
57 | 1, 2, 3, 4, 5, 9, 12, 15, 16, 36, 8, 10, 6, 13, 14, 52, 53, 54, 55, 56, 41 | cpmadumatpolylem1 22382 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ โ ๐บ) โ (๐ต โm
โ0)) |
58 | 1, 2, 3, 4, 5, 9, 12, 15, 16, 36, 8, 10, 6, 13, 14, 52, 53, 54, 55, 56, 41 | cpmadumatpolylem2 22383 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ โ ๐บ) finSupp (0gโ๐ด)) |
59 | | cpmadumatpoly.i |
. . . . . . . . . 10
โข ๐ผ = (๐ pMatToMatPoly ๐
) |
60 | 3, 4, 52, 55, 56, 54, 1, 2, 53, 59, 7, 6, 8, 5 | pm2mp 22326 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ CRing) โง ((๐ โ ๐บ) โ (๐ต โm โ0)
โง (๐ โ ๐บ) finSupp
(0gโ๐ด)))
โ (๐ผโ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ((๐ โ ๐บ)โ๐)))))) = (๐ ฮฃg (๐ โ โ0
โฆ (((๐ โ ๐บ)โ๐) โ (๐ โ ๐))))) |
61 | 51, 57, 58, 60 | syl12anc 835 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ผโ(๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ((๐ โ ๐บ)โ๐)))))) = (๐ ฮฃg (๐ โ โ0
โฆ (((๐ โ ๐บ)โ๐) โ (๐ โ ๐))))) |
62 | | fvco3 6990 |
. . . . . . . . . . . . . . 15
โข ((๐บ:โ0โถ๐ โง ๐ โ โ0) โ ((๐ โ ๐บ)โ๐) = (๐โ(๐บโ๐))) |
63 | 62 | eqcomd 2738 |
. . . . . . . . . . . . . 14
โข ((๐บ:โ0โถ๐ โง ๐ โ โ0) โ (๐โ(๐บโ๐)) = ((๐ โ ๐บ)โ๐)) |
64 | 39, 63 | sylan 580 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ โ0) โ (๐โ(๐บโ๐)) = ((๐ โ ๐บ)โ๐)) |
65 | 64 | fveq2d 6895 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ โ0) โ (๐โ(๐โ(๐บโ๐))) = (๐โ((๐ โ ๐บ)โ๐))) |
66 | 65 | oveq2d 7424 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ โ0) โ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐)))) = ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ((๐ โ ๐บ)โ๐)))) |
67 | 66 | mpteq2dva 5248 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ โ โ0 โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐))))) = (๐ โ โ0 โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ((๐ โ ๐บ)โ๐))))) |
68 | 67 | oveq2d 7424 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐)))))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ((๐ โ ๐บ)โ๐)))))) |
69 | 68 | fveq2d 6895 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ผโ(๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐))))))) = (๐ผโ(๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ((๐ โ ๐บ)โ๐))))))) |
70 | 64 | oveq1d 7423 |
. . . . . . . . . 10
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ โ0) โ ((๐โ(๐บโ๐)) โ (๐ โ ๐)) = (((๐ โ ๐บ)โ๐) โ (๐ โ ๐))) |
71 | 70 | mpteq2dva 5248 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ โ โ0 โฆ ((๐โ(๐บโ๐)) โ (๐ โ ๐))) = (๐ โ โ0 โฆ (((๐ โ ๐บ)โ๐) โ (๐ โ ๐)))) |
72 | 71 | oveq2d 7424 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐โ(๐บโ๐)) โ (๐ โ ๐)))) = (๐ ฮฃg (๐ โ โ0
โฆ (((๐ โ ๐บ)โ๐) โ (๐ โ ๐))))) |
73 | 61, 69, 72 | 3eqtr4d 2782 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ (๐ผโ(๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐))))))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐โ(๐บโ๐)) โ (๐ โ ๐))))) |
74 | 49, 73 | sylan9eqr 2794 |
. . . . . 6
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โง (๐ท ร (๐ฝโ๐ท)) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐))))))) โ (๐ผโ(๐ท ร (๐ฝโ๐ท))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐โ(๐บโ๐)) โ (๐ โ ๐))))) |
75 | 74 | ex 413 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ ((๐ท ร (๐ฝโ๐ท)) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐โ(๐โ(๐บโ๐)))))) โ (๐ผโ(๐ท ร (๐ฝโ๐ท))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐โ(๐บโ๐)) โ (๐ โ ๐)))))) |
76 | 48, 75 | sylbid 239 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โง ๐ โ (๐ต โm (0...๐ ))) โ ((๐ท ร (๐ฝโ๐ท)) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐บโ๐)))) โ (๐ผโ(๐ท ร (๐ฝโ๐ท))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐โ(๐บโ๐)) โ (๐ โ ๐)))))) |
77 | 76 | reximdva 3168 |
. . 3
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง ๐ โ โ) โ (โ๐ โ (๐ต โm (0...๐ ))(๐ท ร (๐ฝโ๐ท)) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐บโ๐)))) โ โ๐ โ (๐ต โm (0...๐ ))(๐ผโ(๐ท ร (๐ฝโ๐ท))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐โ(๐บโ๐)) โ (๐ โ ๐)))))) |
78 | 77 | reximdva 3168 |
. 2
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ (โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ท ร (๐ฝโ๐ท)) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(.gโ(mulGrpโ๐))๐) ยท (๐บโ๐)))) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ผโ(๐ท ร (๐ฝโ๐ท))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐โ(๐บโ๐)) โ (๐ โ ๐)))))) |
79 | 30, 78 | mpd 15 |
1
โข ((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โ โ๐ โ โ โ๐ โ (๐ต โm (0...๐ ))(๐ผโ(๐ท ร (๐ฝโ๐ท))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐โ(๐บโ๐)) โ (๐ โ ๐))))) |