Theorem pmat1op

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

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

Proof

Step	Hyp	Ref	Expression
1		pmatring.p	|- P = ( Poly1 ` R )
2		pmatring.c	|- C = ( N Mat P )
3		pmat0op.z	|- .0. = ( 0g ` P )
4		pmat1op.o	|- .1. = ( 1r ` P )
5	1	ply1ring	|- ( R e. Ring -> P e. Ring )
6	2 4 3	mat1	|- ( ( N e. Fin /\ P e. Ring ) -> ( 1r ` C ) = ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) )
7	5 6	sylan2	|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) = ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) )