Theorem pmat0opsc

Description: The zero polynomial matrix over a ring represented as operation with "lifted scalars" (i.e. elements of the ring underlying the polynomial ring embedded into the polynomial ring by the scalar injection/algebraic scalars function algSc ). (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$$
Assertion	pmat0opsc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 0_C=\left(i\in N,j\in N⟼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		eqid	$$⊢0_P=0_P$$
6	1 2 5	pmat0op	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 0_C=\left(i\in N,j\in N⟼0_P\right)$$
7	1 3 4 5	ply1scl0	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{0}\right)=0_P$$
8	7	eqcomd	$$⊢R\in \mathrm{Ring}\to 0_P=A\left(\underset{\dot{}}{0}\right)$$
9	8	adantl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 0_P=A\left(\underset{\dot{}}{0}\right)$$
10	9	mpoeq3dv	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to \left(i\in N,j\in N⟼0_P\right)=\left(i\in N,j\in N⟼A\left(\underset{\dot{}}{0}\right)\right)$$
11	6 10	eqtrd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 0_C=\left(i\in N,j\in N⟼A\left(\underset{\dot{}}{0}\right)\right)$$