Theorem pmat1ovscd

Description: Entries of the identity polynomial matrix over a ring represented with "lifted scalars", deduction form. (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 )
	pmat1ovscd.n	|- ( ph -> N e. Fin )
	pmat1ovscd.r	|- ( ph -> R e. Ring )
	pmat1ovscd.i	|- ( ph -> I e. N )
	pmat1ovscd.j	|- ( ph -> J e. N )
	pmat1ovscd.u	|- U = ( 1r ` C )
Assertion	pmat1ovscd	|- ( ph -> ( I U J ) = 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		pmat1ovscd.n	|- ( ph -> N e. Fin )
7		pmat1ovscd.r	|- ( ph -> R e. Ring )
8		pmat1ovscd.i	|- ( ph -> I e. N )
9		pmat1ovscd.j	|- ( ph -> J e. N )
10		pmat1ovscd.u	|- U = ( 1r ` C )
11		eqid	|- ( 0g ` P ) = ( 0g ` P )
12		eqid	|- ( 1r ` P ) = ( 1r ` P )
13	1 2 11 12 6 7 8 9 10	pmat1ovd	|- ( ph -> ( I U J ) = if ( I = J , ( 1r ` P ) , ( 0g ` P ) ) )
14	1 3 5 12	ply1scl1	|- ( R e. Ring -> ( A ` .1. ) = ( 1r ` P ) )
15	7 14	syl	|- ( ph -> ( A ` .1. ) = ( 1r ` P ) )
16	15	eqcomd	|- ( ph -> ( 1r ` P ) = ( A ` .1. ) )
17	1 3 4 11	ply1scl0	|- ( R e. Ring -> ( A ` .0. ) = ( 0g ` P ) )
18	7 17	syl	|- ( ph -> ( A ` .0. ) = ( 0g ` P ) )
19	18	eqcomd	|- ( ph -> ( 0g ` P ) = ( A ` .0. ) )
20	16 19	ifeq12d	|- ( ph -> if ( I = J , ( 1r ` P ) , ( 0g ` P ) ) = if ( I = J , ( A ` .1. ) , ( A ` .0. ) ) )
21	13 20	eqtrd	|- ( ph -> ( I U J ) = if ( I = J , ( A ` .1. ) , ( A ` .0. ) ) )