Theorem idmatidpmat

Description: The transformed identity matrix is the identity polynomial matrix. (Contributed by AV, 1-Aug-2019) (Proof shortened by AV, 19-Nov-2019)

	Ref	Expression
Hypotheses	idmatidpmat.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	idmatidpmat.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	idmatidpmat.1	$$⊢\underset{\dot{}}{1}=1_{\left(N\mathrm{Mat}R\right)}$$
	idmatidpmat.i	$$⊢I=1_{\left(N\mathrm{Mat}P\right)}$$
Assertion	idmatidpmat	$$⊢\left(R\in \mathrm{Ring}\wedge N\in \mathrm{Fin}\right)\to T\left(\underset{\dot{}}{1}\right)=I$$

Proof

Step	Hyp	Ref	Expression
1		idmatidpmat.t	$$⊢T=N\mathrm{matToPolyMat}R$$
2		idmatidpmat.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		idmatidpmat.1	$$⊢\underset{\dot{}}{1}=1_{\left(N\mathrm{Mat}R\right)}$$
4		idmatidpmat.i	$$⊢I=1_{\left(N\mathrm{Mat}P\right)}$$
5		eqid	$$⊢N\mathrm{Mat}R=N\mathrm{Mat}R$$
6		eqid	$$⊢{\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
7		eqid	$$⊢N\mathrm{Mat}P=N\mathrm{Mat}P$$
8		eqid	$$⊢{\mathrm{Base}}_{\left(N\mathrm{Mat}P\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}P\right)}$$
9	1 5 6 2 7 8	mat2pmat1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\left(1_{\left(N\mathrm{Mat}R\right)}\right)=1_{\left(N\mathrm{Mat}P\right)}$$
10	3	fveq2i	$$⊢T\left(\underset{\dot{}}{1}\right)=T\left(1_{\left(N\mathrm{Mat}R\right)}\right)$$
11	9 10 4	3eqtr4g	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\left(\underset{\dot{}}{1}\right)=I$$
12	11	ancoms	$$⊢\left(R\in \mathrm{Ring}\wedge N\in \mathrm{Fin}\right)\to T\left(\underset{\dot{}}{1}\right)=I$$