Theorem cpmidgsum

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum. (Contributed by AV, 7-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. )
Assertion	cpmidgsum	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> H = ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. .1. ) ) ) ) )

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		eqid	|- ( Base ` P ) = ( Base ` P )
14	10 1 2 3 13	chpmatply1	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) e. ( Base ` P ) )
15	11 14	eqeltrid	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> K e. ( Base ` P ) )
16		eqid	|- ( Base ` Y ) = ( Base ` Y )
17		eqid	|- ( N matToPolyMat R ) = ( N matToPolyMat R )
18		eqid	|- ( Base ` R ) = ( Base ` R )
19	3 4 16 7 6 5 17 1 2 9 18 13 9 8 12	pmatcollpwscmat	|- ( ( N e. Fin /\ R e. CRing /\ K e. ( Base ` P ) ) -> H = ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. .1. ) ) ) ) )
20	15 19	syld3an3	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> H = ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. .1. ) ) ) ) )