Step |
Hyp |
Ref |
Expression |
1 |
|
m2cpminvid.i |
|- I = ( N cPolyMatToMat R ) |
2 |
|
m2cpminvid.a |
|- A = ( N Mat R ) |
3 |
|
m2cpminvid.k |
|- K = ( Base ` A ) |
4 |
|
m2cpminvid.t |
|- T = ( N matToPolyMat R ) |
5 |
|
eqid |
|- ( N ConstPolyMat R ) = ( N ConstPolyMat R ) |
6 |
5 4 2 3
|
m2cpm |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( T ` M ) e. ( N ConstPolyMat R ) ) |
7 |
1 5
|
cpm2mval |
|- ( ( N e. Fin /\ R e. Ring /\ ( T ` M ) e. ( N ConstPolyMat R ) ) -> ( I ` ( T ` M ) ) = ( x e. N , y e. N |-> ( ( coe1 ` ( x ( T ` M ) y ) ) ` 0 ) ) ) |
8 |
6 7
|
syld3an3 |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( I ` ( T ` M ) ) = ( x e. N , y e. N |-> ( ( coe1 ` ( x ( T ` M ) y ) ) ` 0 ) ) ) |
9 |
|
eqid |
|- ( Poly1 ` R ) = ( Poly1 ` R ) |
10 |
|
eqid |
|- ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) ) |
11 |
4 2 3 9 10
|
mat2pmatvalel |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( x e. N /\ y e. N ) ) -> ( x ( T ` M ) y ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) ) |
12 |
11
|
3impb |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( x ( T ` M ) y ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) ) |
13 |
12
|
fveq2d |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( coe1 ` ( x ( T ` M ) y ) ) = ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) ) ) |
14 |
13
|
fveq1d |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( ( coe1 ` ( x ( T ` M ) y ) ) ` 0 ) = ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) ) ` 0 ) ) |
15 |
|
simp12 |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> R e. Ring ) |
16 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
17 |
|
simp2 |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> x e. N ) |
18 |
|
simp3 |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> y e. N ) |
19 |
|
simp13 |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> M e. K ) |
20 |
2 16 3 17 18 19
|
matecld |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( x M y ) e. ( Base ` R ) ) |
21 |
9 10 16
|
ply1sclid |
|- ( ( R e. Ring /\ ( x M y ) e. ( Base ` R ) ) -> ( x M y ) = ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) ) ` 0 ) ) |
22 |
15 20 21
|
syl2anc |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( x M y ) = ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) ) ` 0 ) ) |
23 |
14 22
|
eqtr4d |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( ( coe1 ` ( x ( T ` M ) y ) ) ` 0 ) = ( x M y ) ) |
24 |
23
|
mpoeq3dva |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( x e. N , y e. N |-> ( ( coe1 ` ( x ( T ` M ) y ) ) ` 0 ) ) = ( x e. N , y e. N |-> ( x M y ) ) ) |
25 |
|
eqidd |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> ( x e. N , y e. N |-> ( x M y ) ) = ( x e. N , y e. N |-> ( x M y ) ) ) |
26 |
|
oveq12 |
|- ( ( x = i /\ y = j ) -> ( x M y ) = ( i M j ) ) |
27 |
26
|
adantl |
|- ( ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) /\ ( x = i /\ y = j ) ) -> ( x M y ) = ( i M j ) ) |
28 |
|
simprl |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> i e. N ) |
29 |
|
simprr |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> j e. N ) |
30 |
|
ovexd |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> ( i M j ) e. _V ) |
31 |
25 27 28 29 30
|
ovmpod |
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> ( i ( x e. N , y e. N |-> ( x M y ) ) j ) = ( i M j ) ) |
32 |
31
|
ralrimivva |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> A. i e. N A. j e. N ( i ( x e. N , y e. N |-> ( x M y ) ) j ) = ( i M j ) ) |
33 |
|
simp1 |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> N e. Fin ) |
34 |
|
simp2 |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> R e. Ring ) |
35 |
2 16 3 33 34 20
|
matbas2d |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( x e. N , y e. N |-> ( x M y ) ) e. K ) |
36 |
|
simp3 |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> M e. K ) |
37 |
2 3
|
eqmat |
|- ( ( ( x e. N , y e. N |-> ( x M y ) ) e. K /\ M e. K ) -> ( ( x e. N , y e. N |-> ( x M y ) ) = M <-> A. i e. N A. j e. N ( i ( x e. N , y e. N |-> ( x M y ) ) j ) = ( i M j ) ) ) |
38 |
35 36 37
|
syl2anc |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( ( x e. N , y e. N |-> ( x M y ) ) = M <-> A. i e. N A. j e. N ( i ( x e. N , y e. N |-> ( x M y ) ) j ) = ( i M j ) ) ) |
39 |
32 38
|
mpbird |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( x e. N , y e. N |-> ( x M y ) ) = M ) |
40 |
8 24 39
|
3eqtrd |
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( I ` ( T ` M ) ) = M ) |