cpmidgsum2

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as another group sum. (Contributed by AV, 10-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 )
	cpmidgsum2.h	\|- H = ( K .x. .1. )
Assertion	cpmidgsum2	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) H = ( 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		cpmidgsum2.h	\|- H = ( K .x. .1. )
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	cpmadugsum	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( I .X. ( J ` I ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )
21		crngring	\|- ( R e. CRing -> R e. Ring )
22	21	anim2i	\|- ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
23	22	3adant3	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
24	3 4	pmatring	\|- ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
25		ringgrp	\|- ( Y e. Ring -> Y e. Grp )
26	23 24 25	3syl	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Grp )
27	3 4	pmatlmod	\|- ( ( N e. Fin /\ R e. Ring ) -> Y e. LMod )
28	21 27	sylan2	\|- ( ( N e. Fin /\ R e. CRing ) -> Y e. LMod )
29	21	adantl	\|- ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
30		eqid	\|- ( Base ` P ) = ( Base ` P )
31	6 3 30	vr1cl	\|- ( R e. Ring -> X e. ( Base ` P ) )
32	29 31	syl	\|- ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` P ) )
33	3	ply1crng	\|- ( R e. CRing -> P e. CRing )
34	4	matsca2	\|- ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` Y ) )
35	33 34	sylan2	\|- ( ( N e. Fin /\ R e. CRing ) -> P = ( Scalar ` Y ) )
36	35	fveq2d	\|- ( ( N e. Fin /\ R e. CRing ) -> ( Base ` P ) = ( Base ` ( Scalar ` Y ) ) )
37	32 36	eleqtrd	\|- ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` ( Scalar ` Y ) ) )
38		eqid	\|- ( Base ` Y ) = ( Base ` Y )
39	38 10	ringidcl	\|- ( Y e. Ring -> .1. e. ( Base ` Y ) )
40	22 24 39	3syl	\|- ( ( N e. Fin /\ R e. CRing ) -> .1. e. ( Base ` Y ) )
41		eqid	\|- ( Scalar ` Y ) = ( Scalar ` Y )
42		eqid	\|- ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
43	38 41 8 42	lmodvscl	\|- ( ( Y e. LMod /\ X e. ( Base ` ( Scalar ` Y ) ) /\ .1. e. ( Base ` Y ) ) -> ( X .x. .1. ) e. ( Base ` Y ) )
44	28 37 40 43	syl3anc	\|- ( ( N e. Fin /\ R e. CRing ) -> ( X .x. .1. ) e. ( Base ` Y ) )
45	44	3adant3	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( X .x. .1. ) e. ( Base ` Y ) )
46	5 1 2 3 4	mat2pmatbas	\|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
47	21 46	syl3an2	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
48	38 12	grpsubcl	\|- ( ( Y e. Grp /\ ( X .x. .1. ) e. ( Base ` Y ) /\ ( T ` M ) e. ( Base ` Y ) ) -> ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` Y ) )
49	26 45 47 48	syl3anc	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` Y ) )
50	33	3ad2ant2	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. CRing )
51		eqid	\|- ( N maDet P ) = ( N maDet P )
52	4 38 14 51 10 9 8	madurid	\|- ( ( ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` Y ) /\ P e. CRing ) -> ( ( ( X .x. .1. ) .- ( T ` M ) ) .X. ( J ` ( ( X .x. .1. ) .- ( T ` M ) ) ) ) = ( ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) .x. .1. ) )
53	49 50 52	syl2anc	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( ( X .x. .1. ) .- ( T ` M ) ) .X. ( J ` ( ( X .x. .1. ) .- ( T ` M ) ) ) ) = ( ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) .x. .1. ) )
54		id	\|- ( I = ( ( X .x. .1. ) .- ( T ` M ) ) -> I = ( ( X .x. .1. ) .- ( T ` M ) ) )
55		fveq2	\|- ( I = ( ( X .x. .1. ) .- ( T ` M ) ) -> ( J ` I ) = ( J ` ( ( X .x. .1. ) .- ( T ` M ) ) ) )
56	54 55	oveq12d	\|- ( I = ( ( X .x. .1. ) .- ( T ` M ) ) -> ( I .X. ( J ` I ) ) = ( ( ( X .x. .1. ) .- ( T ` M ) ) .X. ( J ` ( ( X .x. .1. ) .- ( T ` M ) ) ) ) )
57	13 56	mp1i	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I .X. ( J ` I ) ) = ( ( ( X .x. .1. ) .- ( T ` M ) ) .X. ( J ` ( ( X .x. .1. ) .- ( T ` M ) ) ) ) )
58	17 1 2 3 4 51 12 6 8 5 10	chpmatval	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) = ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) )
59	18 58	syl5eq	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> K = ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) )
60	59	oveq1d	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( K .x. .1. ) = ( ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) .x. .1. ) )
61	19 60	syl5eq	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> H = ( ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) .x. .1. ) )
62	53 57 61	3eqtr4rd	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> H = ( I .X. ( J ` I ) ) )
63	62	adantr	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I .X. ( J ` I ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) ) -> H = ( I .X. ( J ` I ) ) )
64		simpr	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I .X. ( J ` I ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) ) -> ( I .X. ( J ` I ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )
65	63 64	eqtrd	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I .X. ( J ` I ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) ) -> H = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )
66	65	ex	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( I .X. ( J ` I ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) -> H = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) ) )
67	66	reximdv	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. b e. ( B ^m ( 0 ... s ) ) ( I .X. ( J ` I ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) -> E. b e. ( B ^m ( 0 ... s ) ) H = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) ) )
68	67	reximdv	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( I .X. ( J ` I ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) H = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) ) )
69	20 68	mpd	\|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) H = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )

Metamath Proof Explorer

Theorem cpmidgsum2

Proof