Metamath Proof Explorer

Theorem pmat1opsc

Description: The identity polynomial matrix over a ring represented as operation with "lifted scalars". (Contributed by AV, 16-Nov-2019)

Ref Expression
Hypotheses pmat0opsc.p 
|- P = ( Poly1 ` R )
pmat0opsc.c 
|- C = ( N Mat P )
pmat0opsc.a 
|- A = ( algSc ` P )
pmat0opsc.z 
|- .0. = ( 0g ` R )
pmat1opsc.o 
|- .1. = ( 1r ` R )
Assertion pmat1opsc 
|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) = ( i e. N , j e. N |-> if ( i = j , ( A ` .1. ) , ( A ` .0. ) ) ) )

Proof

Step Hyp Ref Expression
1 pmat0opsc.p 
 |-  P = ( Poly1 ` R )
2 pmat0opsc.c 
 |-  C = ( N Mat P )
3 pmat0opsc.a 
 |-  A = ( algSc ` P )
4 pmat0opsc.z 
 |-  .0. = ( 0g ` R )
5 pmat1opsc.o 
 |-  .1. = ( 1r ` R )
6 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
7 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
8 1 2 6 7 pmat1op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) = ( i e. N , j e. N |-> if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) ) )
9 1 3 5 7 ply1scl1 
 |-  ( R e. Ring -> ( A ` .1. ) = ( 1r ` P ) )
10 9 eqcomd 
 |-  ( R e. Ring -> ( 1r ` P ) = ( A ` .1. ) )
11 1 3 4 6 ply1scl0 
 |-  ( R e. Ring -> ( A ` .0. ) = ( 0g ` P ) )
12 11 eqcomd 
 |-  ( R e. Ring -> ( 0g ` P ) = ( A ` .0. ) )
13 10 12 ifeq12d 
 |-  ( R e. Ring -> if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) = if ( i = j , ( A ` .1. ) , ( A ` .0. ) ) )
14 13 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) = if ( i = j , ( A ` .1. ) , ( A ` .0. ) ) )
15 14 mpoeq3dv 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( i e. N , j e. N |-> if ( i = j , ( 1r ` P ) , ( 0g ` P ) ) ) = ( i e. N , j e. N |-> if ( i = j , ( A ` .1. ) , ( A ` .0. ) ) ) )
16 8 15 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) = ( i e. N , j e. N |-> if ( i = j , ( A ` .1. ) , ( A ` .0. ) ) ) )