Step | Hyp | Ref
| Expression |
1 | | pm2mpfo.p |
. . 3
โข ๐ = (Poly1โ๐
) |
2 | | pm2mpfo.c |
. . 3
โข ๐ถ = (๐ Mat ๐) |
3 | | pm2mpfo.b |
. . 3
โข ๐ต = (Baseโ๐ถ) |
4 | | pm2mpfo.m |
. . 3
โข โ = (
ยท๐ โ๐) |
5 | | pm2mpfo.e |
. . 3
โข โ =
(.gโ(mulGrpโ๐)) |
6 | | pm2mpfo.x |
. . 3
โข ๐ = (var1โ๐ด) |
7 | | pm2mpfo.a |
. . 3
โข ๐ด = (๐ Mat ๐
) |
8 | | pm2mpfo.q |
. . 3
โข ๐ = (Poly1โ๐ด) |
9 | | pm2mpfo.t |
. . 3
โข ๐ = (๐ pMatToMatPoly ๐
) |
10 | | pm2mpfo.l |
. . 3
โข ๐ฟ = (Baseโ๐) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pm2mpf 22163 |
. 2
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐:๐ตโถ๐ฟ) |
12 | | eqid 2733 |
. . . . . 6
โข (
ยท๐ โ๐) = ( ยท๐
โ๐) |
13 | | eqid 2733 |
. . . . . 6
โข
(.gโ(mulGrpโ๐)) =
(.gโ(mulGrpโ๐)) |
14 | | eqid 2733 |
. . . . . 6
โข
(var1โ๐
) = (var1โ๐
) |
15 | | eqid 2733 |
. . . . . 6
โข (๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) = (๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) |
16 | 7, 8, 10, 12, 13, 14, 15, 1, 9 | mp2pm2mp 22176 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ) โ (๐โ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐)) = ๐) |
17 | 16 | 3expa 1119 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ฟ) โ (๐โ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐)) = ๐) |
18 | 7, 8, 10, 1, 12, 13, 14, 15, 2, 3 | mply1topmatcl 22170 |
. . . . . . . 8
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ฟ) โ ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐) โ ๐ต) |
19 | 18 | 3expa 1119 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ฟ) โ ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐) โ ๐ต) |
20 | | simpr 486 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ฟ) โง ๐ = ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐)) โ ๐ = ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐)) |
21 | 20 | fveq2d 6847 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ฟ) โง ๐ = ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐)) โ (๐โ๐) = (๐โ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐))) |
22 | 21 | eqeq2d 2744 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ฟ) โง ๐ = ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐)) โ (๐ = (๐โ๐) โ ๐ = (๐โ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐)))) |
23 | 19, 22 | rspcedv 3573 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ฟ) โ (๐ = (๐โ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐)) โ โ๐ โ ๐ต ๐ = (๐โ๐))) |
24 | 23 | com12 32 |
. . . . 5
โข (๐ = (๐โ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐)) โ (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ฟ) โ โ๐ โ ๐ต ๐ = (๐โ๐))) |
25 | 24 | eqcoms 2741 |
. . . 4
โข ((๐โ((๐ โ ๐ฟ โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐((coe1โ๐)โ๐)๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))โ๐)) = ๐ โ (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ฟ) โ โ๐ โ ๐ต ๐ = (๐โ๐))) |
26 | 17, 25 | mpcom 38 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ฟ) โ โ๐ โ ๐ต ๐ = (๐โ๐)) |
27 | 26 | ralrimiva 3140 |
. 2
โข ((๐ โ Fin โง ๐
โ Ring) โ
โ๐ โ ๐ฟ โ๐ โ ๐ต ๐ = (๐โ๐)) |
28 | | dffo3 7053 |
. 2
โข (๐:๐ตโontoโ๐ฟ โ (๐:๐ตโถ๐ฟ โง โ๐ โ ๐ฟ โ๐ โ ๐ต ๐ = (๐โ๐))) |
29 | 11, 27, 28 | sylanbrc 584 |
1
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐:๐ตโontoโ๐ฟ) |