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={\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$$
Assertion	pmat1opsc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 1_C=\left(i\in N,j\in N⟼if\left(i=j,A\left(\underset{\dot{}}{1}\right),A\left(\underset{\dot{}}{0}\right)\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		eqid	$$⊢0_P=0_P$$
7		eqid	$$⊢1_P=1_P$$
8	1 2 6 7	pmat1op	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 1_C=\left(i\in N,j\in N⟼if\left(i=j,1_P,0_P\right)\right)$$
9	1 3 5 7	ply1scl1	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{1}\right)=1_P$$
10	9	eqcomd	$$⊢R\in \mathrm{Ring}\to 1_P=A\left(\underset{\dot{}}{1}\right)$$
11	1 3 4 6	ply1scl0	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{0}\right)=0_P$$
12	11	eqcomd	$$⊢R\in \mathrm{Ring}\to 0_P=A\left(\underset{\dot{}}{0}\right)$$
13	10 12	ifeq12d	$$⊢R\in \mathrm{Ring}\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)$$
14	13	adantl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\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)$$
15	14	mpoeq3dv	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to \left(i\in N,j\in N⟼if\left(i=j,1_P,0_P\right)\right)=\left(i\in N,j\in N⟼if\left(i=j,A\left(\underset{\dot{}}{1}\right),A\left(\underset{\dot{}}{0}\right)\right)\right)$$
16	8 15	eqtrd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 1_C=\left(i\in N,j\in N⟼if\left(i=j,A\left(\underset{\dot{}}{1}\right),A\left(\underset{\dot{}}{0}\right)\right)\right)$$