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={\mathrm{Poly}}_1\left(R\right)$$
	pmatring.c	$$⊢C=N\mathrm{Mat}P$$
	pmat0op.z	$$⊢\underset{\dot{}}{0}=0_P$$
	pmat1op.o	$$⊢\underset{\dot{}}{1}=1_P$$
Assertion	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,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pmatring.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		pmatring.c	$$⊢C=N\mathrm{Mat}P$$
3		pmat0op.z	$$⊢\underset{\dot{}}{0}=0_P$$
4		pmat1op.o	$$⊢\underset{\dot{}}{1}=1_P$$
5	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
6	2 4 3	mat1	$$⊢\left(N\in \mathrm{Fin}\wedge P\in \mathrm{Ring}\right)\to 1_C=\left(i\in N,j\in N⟼if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
7	5 6	sylan2	$$⊢\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,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$