Theorem pmat0op

Description: The zero 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$$
Assertion	pmat0op	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 0_C=\left(i\in N,j\in N⟼\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	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
5	2 3	mat0op	$$⊢\left(N\in \mathrm{Fin}\wedge P\in \mathrm{Ring}\right)\to 0_C=\left(i\in N,j\in N⟼\underset{\dot{}}{0}\right)$$
6	4 5	sylan2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 0_C=\left(i\in N,j\in N⟼\underset{\dot{}}{0}\right)$$