Theorem cpmidg2sum

Description: Equality of two sums representing the identity matrix multiplied with the characteristic polynomial of a matrix. (Contributed by AV, 11-Nov-2019)

	Ref	Expression
Hypotheses	cpmadugsum.a	|- A = ( N Mat R )
	cpmadugsum.b	|- B = ( Base ` A )
	cpmadugsum.p	|- P = ( Poly1 ` R )
	cpmadugsum.y	|- Y = ( N Mat P )
	cpmadugsum.t	|- T = ( N matToPolyMat R )
	cpmadugsum.x	|- X = ( var1 ` R )
	cpmadugsum.e	|- .^ = ( .g ` ( mulGrp ` P ) )
	cpmadugsum.m	|- .x. = ( .s ` Y )
	cpmadugsum.r	|- .X. = ( .r ` Y )
	cpmadugsum.1	|- .1. = ( 1r ` Y )
	cpmadugsum.g	|- .+ = ( +g ` Y )
	cpmadugsum.s	|- .- = ( -g ` Y )
	cpmadugsum.i	|- I = ( ( X .x. .1. ) .- ( T ` M ) )
	cpmadugsum.j	|- J = ( N maAdju P )
	cpmadugsum.0	|- .0. = ( 0g ` Y )
	cpmadugsum.g2	|- G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
	cpmidgsum2.c	|- C = ( N CharPlyMat R )
	cpmidgsum2.k	|- K = ( C ` M )
	cpmidg2sum.u	|- U = ( algSc ` P )
Assertion	cpmidg2sum	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` i ) ) .x. .1. ) ) ) ) = ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cpmadugsum.a	|- A = ( N Mat R )
2		cpmadugsum.b	|- B = ( Base ` A )
3		cpmadugsum.p	|- P = ( Poly1 ` R )
4		cpmadugsum.y	|- Y = ( N Mat P )
5		cpmadugsum.t	|- T = ( N matToPolyMat R )
6		cpmadugsum.x	|- X = ( var1 ` R )
7		cpmadugsum.e	|- .^ = ( .g ` ( mulGrp ` P ) )
8		cpmadugsum.m	|- .x. = ( .s ` Y )
9		cpmadugsum.r	|- .X. = ( .r ` Y )
10		cpmadugsum.1	|- .1. = ( 1r ` Y )
11		cpmadugsum.g	|- .+ = ( +g ` Y )
12		cpmadugsum.s	|- .- = ( -g ` Y )
13		cpmadugsum.i	|- I = ( ( X .x. .1. ) .- ( T ` M ) )
14		cpmadugsum.j	|- J = ( N maAdju P )
15		cpmadugsum.0	|- .0. = ( 0g ` Y )
16		cpmadugsum.g2	|- G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
17		cpmidgsum2.c	|- C = ( N CharPlyMat R )
18		cpmidgsum2.k	|- K = ( C ` M )
19		cpmidg2sum.u	|- U = ( algSc ` P )
20		eqid	|- ( K .x. .1. ) = ( K .x. .1. )
21	1 2 3 4 6 7 8 10 19 17 18 20	cpmidgsum	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( K .x. .1. ) = ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` i ) ) .x. .1. ) ) ) ) )
22	21	eqcomd	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` i ) ) .x. .1. ) ) ) ) = ( K .x. .1. ) )
23	22	ad3antrrr	|- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ ( K .x. .1. ) = ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) ) -> ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` i ) ) .x. .1. ) ) ) ) = ( K .x. .1. ) )
24		simpr	|- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ ( K .x. .1. ) = ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) ) -> ( K .x. .1. ) = ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )
25	23 24	eqtrd	|- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ ( K .x. .1. ) = ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) ) -> ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` i ) ) .x. .1. ) ) ) ) = ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 20	cpmidgsum2	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( K .x. .1. ) = ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )
27	25 26	reximddv2	|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` i ) ) .x. .1. ) ) ) ) = ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )