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={\mathrm{Poly}}_1\left(R\right)$$
	pmat0opsc.c	$$⊢C=N\mathrm{Mat}P$$
	pmat0opsc.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	pmat0opsc.z	$$⊢\underset{\dot{}}{0}=0_R$$
	pmat1opsc.o	$$⊢\underset{\dot{}}{1}=1_R$$
	pmat1ovscd.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	pmat1ovscd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	pmat1ovscd.i	$$⊢\phi \to I\in N$$
	pmat1ovscd.j	$$⊢\phi \to J\in N$$
	pmat1ovscd.u	$$⊢U=1_C$$
Assertion	pmat1ovscd	$$⊢\phi \to IUJ=if\left(I=J,A\left(\underset{\dot{}}{1}\right),A\left(\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pmat0opsc.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		pmat0opsc.c	$$⊢C=N\mathrm{Mat}P$$
3		pmat0opsc.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
4		pmat0opsc.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		pmat1opsc.o	$$⊢\underset{\dot{}}{1}=1_R$$
6		pmat1ovscd.n	$$⊢\phi \to N\in \mathrm{Fin}$$
7		pmat1ovscd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
8		pmat1ovscd.i	$$⊢\phi \to I\in N$$
9		pmat1ovscd.j	$$⊢\phi \to J\in N$$
10		pmat1ovscd.u	$$⊢U=1_C$$
11		eqid	$$⊢0_P=0_P$$
12		eqid	$$⊢1_P=1_P$$
13	1 2 11 12 6 7 8 9 10	pmat1ovd	$$⊢\phi \to IUJ=if\left(I=J,1_P,0_P\right)$$
14	1 3 5 12	ply1scl1	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{1}\right)=1_P$$
15	7 14	syl	$$⊢\phi \to A\left(\underset{\dot{}}{1}\right)=1_P$$
16	15	eqcomd	$$⊢\phi \to 1_P=A\left(\underset{\dot{}}{1}\right)$$
17	1 3 4 11	ply1scl0	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{0}\right)=0_P$$
18	7 17	syl	$$⊢\phi \to A\left(\underset{\dot{}}{0}\right)=0_P$$
19	18	eqcomd	$$⊢\phi \to 0_P=A\left(\underset{\dot{}}{0}\right)$$
20	16 19	ifeq12d	$$⊢\phi \to if\left(I=J,1_P,0_P\right)=if\left(I=J,A\left(\underset{\dot{}}{1}\right),A\left(\underset{\dot{}}{0}\right)\right)$$
21	13 20	eqtrd	$$⊢\phi \to IUJ=if\left(I=J,A\left(\underset{\dot{}}{1}\right),A\left(\underset{\dot{}}{0}\right)\right)$$