Metamath Proof Explorer

Theorem m2cpmfo

Description: The matrix transformation is a function from the matrices onto the constant polynomial matrices. (Contributed by AV, 19-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

Ref Expression
Hypotheses m2cpmfo.s 
|- S = ( N ConstPolyMat R )
m2cpmfo.t 
|- T = ( N matToPolyMat R )
m2cpmfo.a 
|- A = ( N Mat R )
m2cpmfo.k 
|- K = ( Base ` A )
Assertion m2cpmfo 
|- ( ( N e. Fin /\ R e. Ring ) -> T : K -onto-> S )

Proof

Step Hyp Ref Expression
1 m2cpmfo.s 
 |-  S = ( N ConstPolyMat R )
2 m2cpmfo.t 
 |-  T = ( N matToPolyMat R )
3 m2cpmfo.a 
 |-  A = ( N Mat R )
4 m2cpmfo.k 
 |-  K = ( Base ` A )
5 1 2 3 4 m2cpmf 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : K --> S )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 simplll 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) /\ m e. S ) -> N e. Fin )
8 simpllr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) /\ 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 ) /\ x e. S ) /\ m e. S ) /\ i e. N /\ j e. N ) -> i e. N )
13 simp3 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) /\ m e. S ) /\ i e. N /\ j e. N ) -> j e. N )
14 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
15 1 14 9 11 cpmatpmat 
 |-  ( ( N e. Fin /\ R e. Ring /\ m e. S ) -> m e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
16 15 ad4ant124 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) /\ m e. S ) -> m e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
17 16 3ad2ant1 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) /\ m e. S ) /\ i e. N /\ j e. N ) -> m e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
18 9 10 11 12 13 17 matecld 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) /\ m e. S ) /\ i e. N /\ j e. N ) -> ( i m j ) e. ( Base ` ( Poly1 ` R ) ) )
19 0nn0 
 |-  0 e. NN0
20 eqid 
 |-  ( coe1 ` ( i m j ) ) = ( coe1 ` ( i m j ) )
21 20 10 14 6 coe1fvalcl 
 |-  ( ( ( i m j ) e. ( Base ` ( Poly1 ` R ) ) /\ 0 e. NN0 ) -> ( ( coe1 ` ( i m j ) ) ` 0 ) e. ( Base ` R ) )
22 18 19 21 sylancl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) /\ m e. S ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i m j ) ) ` 0 ) e. ( Base ` R ) )
23 3 6 4 7 8 22 matbas2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) /\ m e. S ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) e. K )
24 23 fmpttd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) : S --> K )
25 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> x e. S )
26 24 25 ffvelrnd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) e. K )
27 fveq2 
 |-  ( c = ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) -> ( T ` c ) = ( T ` ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) ) )
28 27 eqeq2d 
 |-  ( c = ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) -> ( x = ( T ` c ) <-> x = ( T ` ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) ) ) )
29 28 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) /\ c = ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) ) -> ( x = ( T ` c ) <-> x = ( T ` ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) ) ) )
30 eqid 
 |-  ( N cPolyMatToMat R ) = ( N cPolyMatToMat R )
31 30 1 cpm2mfval 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( N cPolyMatToMat R ) = ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) )
32 31 fveq1d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( N cPolyMatToMat R ) ` x ) = ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) )
33 32 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. S ) -> ( ( N cPolyMatToMat R ) ` x ) = ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) )
34 33 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. S ) -> ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) = ( ( N cPolyMatToMat R ) ` x ) )
35 34 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. S ) -> ( T ` ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) ) = ( T ` ( ( N cPolyMatToMat R ) ` x ) ) )
36 1 30 2 m2cpminvid2 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. S ) -> ( T ` ( ( N cPolyMatToMat R ) ` x ) ) = x )
37 35 36 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. S ) -> ( T ` ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) ) = x )
38 37 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> ( T ` ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) ) = x )
39 38 eqcomd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> x = ( T ` ( ( m e. S |-> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` 0 ) ) ) ` x ) ) )
40 26 29 39 rspcedvd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> E. c e. K x = ( T ` c ) )
41 40 ralrimiva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S E. c e. K x = ( T ` c ) )
42 dffo3 
 |-  ( T : K -onto-> S <-> ( T : K --> S /\ A. x e. S E. c e. K x = ( T ` c ) ) )
43 5 41 42 sylanbrc 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : K -onto-> S )