Theorem cpmidpmatlem1

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

	Ref	Expression
Hypotheses	cpmidgsum.a	|- A = ( N Mat R )
	cpmidgsum.b	|- B = ( Base ` A )
	cpmidgsum.p	|- P = ( Poly1 ` R )
	cpmidgsum.y	|- Y = ( N Mat P )
	cpmidgsum.x	|- X = ( var1 ` R )
	cpmidgsum.e	|- .^ = ( .g ` ( mulGrp ` P ) )
	cpmidgsum.m	|- .x. = ( .s ` Y )
	cpmidgsum.1	|- .1. = ( 1r ` Y )
	cpmidgsum.u	|- U = ( algSc ` P )
	cpmidgsum.c	|- C = ( N CharPlyMat R )
	cpmidgsum.k	|- K = ( C ` M )
	cpmidgsum.h	|- H = ( K .x. .1. )
	cpmidgsumm2pm.o	|- O = ( 1r ` A )
	cpmidgsumm2pm.m	|- .* = ( .s ` A )
	cpmidgsumm2pm.t	|- T = ( N matToPolyMat R )
	cpmidpmat.g	|- G = ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) )
Assertion	cpmidpmatlem1	|- ( L e. NN0 -> ( G ` L ) = ( ( ( coe1 ` K ) ` L ) .* O ) )

Proof

Step	Hyp	Ref	Expression
1		cpmidgsum.a	|- A = ( N Mat R )
2		cpmidgsum.b	|- B = ( Base ` A )
3		cpmidgsum.p	|- P = ( Poly1 ` R )
4		cpmidgsum.y	|- Y = ( N Mat P )
5		cpmidgsum.x	|- X = ( var1 ` R )
6		cpmidgsum.e	|- .^ = ( .g ` ( mulGrp ` P ) )
7		cpmidgsum.m	|- .x. = ( .s ` Y )
8		cpmidgsum.1	|- .1. = ( 1r ` Y )
9		cpmidgsum.u	|- U = ( algSc ` P )
10		cpmidgsum.c	|- C = ( N CharPlyMat R )
11		cpmidgsum.k	|- K = ( C ` M )
12		cpmidgsum.h	|- H = ( K .x. .1. )
13		cpmidgsumm2pm.o	|- O = ( 1r ` A )
14		cpmidgsumm2pm.m	|- .* = ( .s ` A )
15		cpmidgsumm2pm.t	|- T = ( N matToPolyMat R )
16		cpmidpmat.g	|- G = ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) )
17		fveq2	|- ( k = L -> ( ( coe1 ` K ) ` k ) = ( ( coe1 ` K ) ` L ) )
18	17	oveq1d	|- ( k = L -> ( ( ( coe1 ` K ) ` k ) .* O ) = ( ( ( coe1 ` K ) ` L ) .* O ) )
19		ovex	|- ( ( ( coe1 ` K ) ` L ) .* O ) e. _V
20	18 16 19	fvmpt	|- ( L e. NN0 -> ( G ` L ) = ( ( ( coe1 ` K ) ` L ) .* O ) )