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={\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$$
	pmat1ovd.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	pmat1ovd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	pmat1ovd.i	$$⊢\phi \to I\in N$$
	pmat1ovd.j	$$⊢\phi \to J\in N$$
	pmat1ovd.u	$$⊢U=1_C$$
Assertion	pmat1ovd	$$⊢\phi \to IUJ=if\left(I=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\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		pmat1ovd.n	$$⊢\phi \to N\in \mathrm{Fin}$$
6		pmat1ovd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		pmat1ovd.i	$$⊢\phi \to I\in N$$
8		pmat1ovd.j	$$⊢\phi \to J\in N$$
9		pmat1ovd.u	$$⊢U=1_C$$
10	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
11	6 10	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
12	2 4 3 5 11 7 8 9	mat1ov	$$⊢\phi \to IUJ=if\left(I=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$