Metamath Proof Explorer

Theorem mat2pmat1

Description: The transformation of the identity matrix results in the identity polynomial matrix. (Contributed by AV, 29-Oct-2019)

Ref Expression
Hypotheses mat2pmatbas.t 
|- T = ( N matToPolyMat R )
mat2pmatbas.a 
|- A = ( N Mat R )
mat2pmatbas.b 
|- B = ( Base ` A )
mat2pmatbas.p 
|- P = ( Poly1 ` R )
mat2pmatbas.c 
|- C = ( N Mat P )
mat2pmatbas0.h 
|- H = ( Base ` C )
Assertion mat2pmat1 
|- ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` A ) ) = ( 1r ` C ) )

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t 
 |-  T = ( N matToPolyMat R )
2 mat2pmatbas.a 
 |-  A = ( N Mat R )
3 mat2pmatbas.b 
 |-  B = ( Base ` A )
4 mat2pmatbas.p 
 |-  P = ( Poly1 ` R )
5 mat2pmatbas.c 
 |-  C = ( N Mat P )
6 mat2pmatbas0.h 
 |-  H = ( Base ` C )
7 simpl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )
8 simpr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
9 2 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
10 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
11 3 10 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
12 9 11 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. B )
13 7 8 12 3jca 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ R e. Ring /\ ( 1r ` A ) e. B ) )
14 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
15 1 2 3 4 14 mat2pmatvalel 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ ( 1r ` A ) e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` ( 1r ` A ) ) j ) = ( ( algSc ` P ) ` ( i ( 1r ` A ) j ) ) )
16 13 15 sylan 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` ( 1r ` A ) ) j ) = ( ( algSc ` P ) ` ( i ( 1r ` A ) j ) ) )
17 fvif 
 |-  ( ( algSc ` P ) ` if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) )
18 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
19 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
20 4 14 18 19 ply1scl1 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
21 20 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
22 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
23 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
24 4 14 22 23 ply1scl0 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 0g ` R ) ) = ( 0g ` P ) )
25 24 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( ( algSc ` P ) ` ( 0g ` R ) ) = ( 0g ` P ) )
26 21 25 ifeq12d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) = if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) )
27 17 26 syl5eq 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( ( algSc ` P ) ` if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) )
28 7 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> N e. Fin )
29 8 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
30 simpl 
 |-  ( ( i e. N /\ j e. N ) -> i e. N )
31 30 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
32 simpr 
 |-  ( ( i e. N /\ j e. N ) -> j e. N )
33 32 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
34 2 18 22 28 29 31 33 10 mat1ov 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( i ( 1r ` A ) j ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
35 34 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( ( algSc ` P ) ` ( i ( 1r ` A ) j ) ) = ( ( algSc ` P ) ` if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) )
36 4 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
37 36 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> P e. Ring )
38 eqid 
 |-  ( 1r ` C ) = ( 1r ` C )
39 5 19 23 28 37 31 33 38 mat1ov 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( i ( 1r ` C ) j ) = if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) )
40 27 35 39 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( ( algSc ` P ) ` ( i ( 1r ` A ) j ) ) = ( i ( 1r ` C ) j ) )
41 16 40 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` ( 1r ` A ) ) j ) = ( i ( 1r ` C ) j ) )
42 41 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. i e. N A. j e. N ( i ( T ` ( 1r ` A ) ) j ) = ( i ( 1r ` C ) j ) )
43 1 2 3 4 5 6 mat2pmatbas0 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( 1r ` A ) e. B ) -> ( T ` ( 1r ` A ) ) e. H )
44 13 43 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` A ) ) e. H )
45 4 5 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
46 6 38 ringidcl 
 |-  ( C e. Ring -> ( 1r ` C ) e. H )
47 45 46 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) e. H )
48 5 6 eqmat 
 |-  ( ( ( T ` ( 1r ` A ) ) e. H /\ ( 1r ` C ) e. H ) -> ( ( T ` ( 1r ` A ) ) = ( 1r ` C ) <-> A. i e. N A. j e. N ( i ( T ` ( 1r ` A ) ) j ) = ( i ( 1r ` C ) j ) ) )
49 44 47 48 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( T ` ( 1r ` A ) ) = ( 1r ` C ) <-> A. i e. N A. j e. N ( i ( T ` ( 1r ` A ) ) j ) = ( i ( 1r ` C ) j ) ) )
50 42 49 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` A ) ) = ( 1r ` C ) )