cpmadugsum

Description: The product of the characteristic matrix of a given matrix and its adjunct represented as an infinite 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 ) ) ) ) ) ) ) )
Assertion	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 ) ) ) ) )

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	1 2 3 4 5 6 7 8 9 10 11 12 13 14	cpmadugsumfi	\|- ( ( 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. ( 1 ... s ) \|-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
18		simpr	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( I .X. ( J ` I ) ) = ( ( Y gsum ( i e. ( 1 ... s ) \|-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) ) -> ( I .X. ( J ` I ) ) = ( ( Y gsum ( i e. ( 1 ... s ) \|-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
19	1 2 3 4 9 12 15 5 16 6 8 7 11	chfacfscmulgsum	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) \|-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
20	19	eqcomd	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 1 ... s ) \|-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )
21	20	adantr	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( I .X. ( J ` I ) ) = ( ( Y gsum ( i e. ( 1 ... s ) \|-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) ) -> ( ( Y gsum ( i e. ( 1 ... s ) \|-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )
22	18 21	eqtrd	\|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( I .X. ( J ` I ) ) = ( ( Y gsum ( i e. ( 1 ... s ) \|-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) ) -> ( I .X. ( J ` I ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) )
23	22	ex	\|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( I .X. ( J ` I ) ) = ( ( Y gsum ( i e. ( 1 ... s ) \|-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) -> ( I .X. ( J ` I ) ) = ( Y gsum ( i e. NN0 \|-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) ) )
24	23	reximdvva	\|- ( ( 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. ( 1 ... s ) \|-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) -> 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 ) ) ) ) ) )
25	17 24	mpd	\|- ( ( 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 ) ) ) ) )

Metamath Proof Explorer

Theorem cpmadugsum

Proof