Theorem cpmidpmatlem1

Description: Lemma 1 for cpmidpmat . (Contributed by AV, 13-Nov-2019)

	Ref	Expression
Hypotheses	cpmidgsum.a	$$⊢A=N\mathrm{Mat}R$$
	cpmidgsum.b	$$⊢B={\mathrm{Base}}_A$$
	cpmidgsum.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	cpmidgsum.y	$$⊢Y=N\mathrm{Mat}P$$
	cpmidgsum.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	cpmidgsum.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	cpmidgsum.m	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	cpmidgsum.1	$$⊢\underset{\dot{}}{1}=1_Y$$
	cpmidgsum.u	$$⊢U=\mathrm{algSc}\left(P\right)$$
	cpmidgsum.c	$$⊢C=N\mathrm{CharPlyMat}R$$
	cpmidgsum.k	$$⊢K=C\left(M\right)$$
	cpmidgsum.h	$$⊢H=K\underset{\dot{}}{·}\underset{\dot{}}{1}$$
	cpmidgsumm2pm.o	$$⊢O=1_A$$
	cpmidgsumm2pm.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
	cpmidgsumm2pm.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	cpmidpmat.g	$$⊢G=\left(k\in {\mathbb{N}}_0⟼{\mathrm{coe}}_1\left(K\right)\left(k\right)\underset{\dot{}}{\ast }O\right)$$
Assertion	cpmidpmatlem1	$$⊢L\in {\mathbb{N}}_0\to G\left(L\right)={\mathrm{coe}}_1\left(K\right)\left(L\right)\underset{\dot{}}{\ast }O$$

Proof

Step	Hyp	Ref	Expression
1		cpmidgsum.a	$$⊢A=N\mathrm{Mat}R$$
2		cpmidgsum.b	$$⊢B={\mathrm{Base}}_A$$
3		cpmidgsum.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		cpmidgsum.y	$$⊢Y=N\mathrm{Mat}P$$
5		cpmidgsum.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
6		cpmidgsum.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
7		cpmidgsum.m	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
8		cpmidgsum.1	$$⊢\underset{\dot{}}{1}=1_Y$$
9		cpmidgsum.u	$$⊢U=\mathrm{algSc}\left(P\right)$$
10		cpmidgsum.c	$$⊢C=N\mathrm{CharPlyMat}R$$
11		cpmidgsum.k	$$⊢K=C\left(M\right)$$
12		cpmidgsum.h	$$⊢H=K\underset{\dot{}}{·}\underset{\dot{}}{1}$$
13		cpmidgsumm2pm.o	$$⊢O=1_A$$
14		cpmidgsumm2pm.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
15		cpmidgsumm2pm.t	$$⊢T=N\mathrm{matToPolyMat}R$$
16		cpmidpmat.g	$$⊢G=\left(k\in {\mathbb{N}}_0⟼{\mathrm{coe}}_1\left(K\right)\left(k\right)\underset{\dot{}}{\ast }O\right)$$
17		fveq2	$$⊢k=L\to {\mathrm{coe}}_1\left(K\right)\left(k\right)={\mathrm{coe}}_1\left(K\right)\left(L\right)$$
18	17	oveq1d	$$⊢k=L\to {\mathrm{coe}}_1\left(K\right)\left(k\right)\underset{\dot{}}{\ast }O={\mathrm{coe}}_1\left(K\right)\left(L\right)\underset{\dot{}}{\ast }O$$
19		ovex	$$⊢{\mathrm{coe}}_1\left(K\right)\left(L\right)\underset{\dot{}}{\ast }O\in \mathrm{V}$$
20	18 16 19	fvmpt	$$⊢L\in {\mathbb{N}}_0\to G\left(L\right)={\mathrm{coe}}_1\left(K\right)\left(L\right)\underset{\dot{}}{\ast }O$$