Metamath Proof Explorer

Theorem m2cpm

Description: The result of a matrix transformation is a constant polynomial matrix. (Contributed by AV, 18-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

Ref Expression
Hypotheses m2cpm.s 
|- S = ( N ConstPolyMat R )
m2cpm.t 
|- T = ( N matToPolyMat R )
m2cpm.a 
|- A = ( N Mat R )
m2cpm.b 
|- B = ( Base ` A )
Assertion m2cpm 
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. S )

Proof

Step Hyp Ref Expression
1 m2cpm.s 
 |-  S = ( N ConstPolyMat R )
2 m2cpm.t 
 |-  T = ( N matToPolyMat R )
3 m2cpm.a 
 |-  A = ( N Mat R )
4 m2cpm.b 
 |-  B = ( Base ` A )
5 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
6 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
7 2 3 4 5 6 mat2pmatvalel 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` M ) j ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( i M j ) ) )
8 7 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> ( i ( T ` M ) j ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( i M j ) ) )
9 8 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> ( coe1 ` ( i ( T ` M ) j ) ) = ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( i M j ) ) ) )
10 9 fveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> ( ( coe1 ` ( i ( T ` M ) j ) ) ` n ) = ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( i M j ) ) ) ` n ) )
11 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
14 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
15 simpl3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> M e. B )
16 3 12 4 13 14 15 matecld 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i M j ) e. ( Base ` R ) )
17 11 16 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> ( R e. Ring /\ ( i M j ) e. ( Base ` R ) ) )
18 17 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> ( R e. Ring /\ ( i M j ) e. ( Base ` R ) ) )
19 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
20 5 6 12 19 coe1scl 
 |-  ( ( R e. Ring /\ ( i M j ) e. ( Base ` R ) ) -> ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( i M j ) ) ) = ( k e. NN0 |-> if ( k = 0 , ( i M j ) , ( 0g ` R ) ) ) )
21 18 20 syl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( i M j ) ) ) = ( k e. NN0 |-> if ( k = 0 , ( i M j ) , ( 0g ` R ) ) ) )
22 eqeq1 
 |-  ( k = n -> ( k = 0 <-> n = 0 ) )
23 22 ifbid 
 |-  ( k = n -> if ( k = 0 , ( i M j ) , ( 0g ` R ) ) = if ( n = 0 , ( i M j ) , ( 0g ` R ) ) )
24 23 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) /\ k = n ) -> if ( k = 0 , ( i M j ) , ( 0g ` R ) ) = if ( n = 0 , ( i M j ) , ( 0g ` R ) ) )
25 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
26 25 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> n e. NN0 )
27 ovex 
 |-  ( i M j ) e. _V
28 fvex 
 |-  ( 0g ` R ) e. _V
29 27 28 ifex 
 |-  if ( n = 0 , ( i M j ) , ( 0g ` R ) ) e. _V
30 29 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> if ( n = 0 , ( i M j ) , ( 0g ` R ) ) e. _V )
31 21 24 26 30 fvmptd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( i M j ) ) ) ` n ) = if ( n = 0 , ( i M j ) , ( 0g ` R ) ) )
32 nnne0 
 |-  ( n e. NN -> n =/= 0 )
33 32 neneqd 
 |-  ( n e. NN -> -. n = 0 )
34 33 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> -. n = 0 )
35 34 iffalsed 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> if ( n = 0 , ( i M j ) , ( 0g ` R ) ) = ( 0g ` R ) )
36 10 31 35 3eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) /\ n e. NN ) -> ( ( coe1 ` ( i ( T ` M ) j ) ) ` n ) = ( 0g ` R ) )
37 36 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( i e. N /\ j e. N ) ) -> A. n e. NN ( ( coe1 ` ( i ( T ` M ) j ) ) ` n ) = ( 0g ` R ) )
38 37 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> A. i e. N A. j e. N A. n e. NN ( ( coe1 ` ( i ( T ` M ) j ) ) ` n ) = ( 0g ` R ) )
39 eqid 
 |-  ( N Mat ( Poly1 ` R ) ) = ( N Mat ( Poly1 ` R ) )
40 2 3 4 5 39 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
41 eqid 
 |-  ( Base ` ( N Mat ( Poly1 ` R ) ) ) = ( Base ` ( N Mat ( Poly1 ` R ) ) )
42 1 5 39 41 cpmatel 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( T ` M ) e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) ) -> ( ( T ` M ) e. S <-> A. i e. N A. j e. N A. n e. NN ( ( coe1 ` ( i ( T ` M ) j ) ) ` n ) = ( 0g ` R ) ) )
43 40 42 syld3an3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( T ` M ) e. S <-> A. i e. N A. j e. N A. n e. NN ( ( coe1 ` ( i ( T ` M ) j ) ) ` n ) = ( 0g ` R ) ) )
44 38 43 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. S )