Theorem pmat1ovd

Description: Entries of the identity polynomial matrix over a ring, deduction form. (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 )
	pmat1ovd.n	|- ( ph -> N e. Fin )
	pmat1ovd.r	|- ( ph -> R e. Ring )
	pmat1ovd.i	|- ( ph -> I e. N )
	pmat1ovd.j	|- ( ph -> J e. N )
	pmat1ovd.u	|- U = ( 1r ` C )
Assertion	pmat1ovd	|- ( ph -> ( I U J ) = 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		pmat1ovd.n	|- ( ph -> N e. Fin )
6		pmat1ovd.r	|- ( ph -> R e. Ring )
7		pmat1ovd.i	|- ( ph -> I e. N )
8		pmat1ovd.j	|- ( ph -> J e. N )
9		pmat1ovd.u	|- U = ( 1r ` C )
10	1	ply1ring	|- ( R e. Ring -> P e. Ring )
11	6 10	syl	|- ( ph -> P e. Ring )
12	2 4 3 5 11 7 8 9	mat1ov	|- ( ph -> ( I U J ) = if ( I = J , .1. , .0. ) )