Step |
Hyp |
Ref |
Expression |
1 |
|
cpm2mf.a |
|- A = ( N Mat R ) |
2 |
|
cpm2mf.k |
|- K = ( Base ` A ) |
3 |
|
cpm2mf.s |
|- S = ( N ConstPolyMat R ) |
4 |
|
cpm2mf.i |
|- I = ( N cPolyMatToMat R ) |
5 |
4 3
|
cpm2mfval |
|- ( ( N e. Fin /\ R e. Ring ) -> I = ( m e. S |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ) |
6 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
7 |
|
simpll |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) -> N e. Fin ) |
8 |
|
simplr |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) -> R e. Ring ) |
9 |
|
eqid |
|- ( N Mat ( Poly1 ` R ) ) = ( N Mat ( Poly1 ` R ) ) |
10 |
|
eqid |
|- ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) ) |
11 |
|
eqid |
|- ( Base ` ( N Mat ( Poly1 ` R ) ) ) = ( Base ` ( N Mat ( Poly1 ` R ) ) ) |
12 |
|
simp2 |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) /\ x e. N /\ y e. N ) -> x e. N ) |
13 |
|
simp3 |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) /\ x e. N /\ y e. N ) -> y e. N ) |
14 |
|
eqid |
|- ( Poly1 ` R ) = ( Poly1 ` R ) |
15 |
3 14 9 11
|
cpmatpmat |
|- ( ( N e. Fin /\ R e. Ring /\ m e. S ) -> m e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) ) |
16 |
15
|
3expa |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) -> m e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) ) |
17 |
16
|
3ad2ant1 |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) /\ x e. N /\ y e. N ) -> m e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) ) |
18 |
9 10 11 12 13 17
|
matecld |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) /\ x e. N /\ y e. N ) -> ( x m y ) e. ( Base ` ( Poly1 ` R ) ) ) |
19 |
|
0nn0 |
|- 0 e. NN0 |
20 |
|
eqid |
|- ( coe1 ` ( x m y ) ) = ( coe1 ` ( x m y ) ) |
21 |
20 10 14 6
|
coe1fvalcl |
|- ( ( ( x m y ) e. ( Base ` ( Poly1 ` R ) ) /\ 0 e. NN0 ) -> ( ( coe1 ` ( x m y ) ) ` 0 ) e. ( Base ` R ) ) |
22 |
18 19 21
|
sylancl |
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) /\ x e. N /\ y e. N ) -> ( ( coe1 ` ( x m y ) ) ` 0 ) e. ( Base ` R ) ) |
23 |
1 6 2 7 8 22
|
matbas2d |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ m e. S ) -> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) e. K ) |
24 |
5 23
|
fmpt3d |
|- ( ( N e. Fin /\ R e. Ring ) -> I : S --> K ) |