Theorem chpscmatgsummon

Description: The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of scaled monomials. (Contributed by AV, 2-Sep-2019)

	Ref	Expression
Hypotheses	chp0mat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	chp0mat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	chp0mat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chp0mat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	chp0mat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
	chp0mat.m	⊢ ↑ = ( .g ‘ 𝐺 )
	chpscmat.d	⊢ 𝐷 = { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑅 ) ) }
	chpscmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
	chpscmat.m	⊢ − = ( -g ‘ 𝑃 )
	chpscmatgsum.f	⊢ 𝐹 = ( .g ‘ 𝑃 )
	chpscmatgsum.h	⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
	chpscmatgsum.e	⊢ 𝐸 = ( .g ‘ 𝐻 )
	chpscmatgsum.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
	chpscmatgsum.s	⊢ · = ( ·𝑠 ‘ 𝑃 )
	chpscmatgsum.z	⊢ 𝑍 = ( .g ‘ 𝑅 )
Assertion	chpscmatgsummon	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		chp0mat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2		chp0mat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		chp0mat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		chp0mat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
5		chp0mat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
6		chp0mat.m	⊢ ↑ = ( .g ‘ 𝐺 )
7		chpscmat.d	⊢ 𝐷 = { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑅 ) ) }
8		chpscmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
9		chpscmat.m	⊢ − = ( -g ‘ 𝑃 )
10		chpscmatgsum.f	⊢ 𝐹 = ( .g ‘ 𝑃 )
11		chpscmatgsum.h	⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
12		chpscmatgsum.e	⊢ 𝐸 = ( .g ‘ 𝐻 )
13		chpscmatgsum.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
14		chpscmatgsum.s	⊢ · = ( ·𝑠 ‘ 𝑃 )
15		chpscmatgsum.z	⊢ 𝑍 = ( .g ‘ 𝑅 )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14	chpscmatgsumbin	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) ) )
17		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
18	17	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
19	2	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
20	18 19	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ LMod )
21	20	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝑃 ∈ LMod )
22	11	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝐻 ∈ Mnd )
23	18 22	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐻 ∈ Mnd )
24	23	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝐻 ∈ Mnd )
25		fznn0sub	⊢ ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) → ( ( ♯ ‘ 𝑁 ) − 𝑙 ) ∈ ℕ0 )
26	25	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ♯ ‘ 𝑁 ) − 𝑙 ) ∈ ℕ0 )
27		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
28	17 27	syl	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Grp )
29	28	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Grp )
30		simp2	⊢ ( ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) → 𝐽 ∈ 𝑁 )
31		elrabi	⊢ ( 𝑀 ∈ { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑅 ) ) } → 𝑀 ∈ ( Base ‘ 𝐴 ) )
32	31 7	eleq2s	⊢ ( 𝑀 ∈ 𝐷 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
33	32	3ad2ant1	⊢ ( ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
34	30 30 33	3jca	⊢ ( ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) → ( 𝐽 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) )
35	34	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐽 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) )
36		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
37	3 36	matecl	⊢ ( ( 𝐽 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
38	35 37	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
39	36 13	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑅 ) )
40	29 38 39	syl2an2r	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑅 ) )
41	40	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑅 ) )
42	11 36	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐻 )
43	42 12	mulgnn0cl	⊢ ( ( 𝐻 ∈ Mnd ∧ ( ( ♯ ‘ 𝑁 ) − 𝑙 ) ∈ ℕ0 ∧ ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ∈ ( Base ‘ 𝑅 ) )
44	24 26 41 43	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ∈ ( Base ‘ 𝑅 ) )
45	2	ply1sca	⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
46	45	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
47	46	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
48	47	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
49	48	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
50	44 49	eleqtrrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
51		hashcl	⊢ ( 𝑁 ∈ Fin → ( ♯ ‘ 𝑁 ) ∈ ℕ0 )
52	51	ad2antrr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( ♯ ‘ 𝑁 ) ∈ ℕ0 )
53		elfzelz	⊢ ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) → 𝑙 ∈ ℤ )
54		bccl	⊢ ( ( ( ♯ ‘ 𝑁 ) ∈ ℕ0 ∧ 𝑙 ∈ ℤ ) → ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ∈ ℕ0 )
55	52 53 54	syl2an	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ∈ ℕ0 )
56	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
57	5	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝐺 ∈ Mnd )
58	17 56 57	3syl	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Mnd )
59	58	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐺 ∈ Mnd )
60	59	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝐺 ∈ Mnd )
61		elfznn0	⊢ ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) → 𝑙 ∈ ℕ0 )
62	61	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝑙 ∈ ℕ0 )
63		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
64	4 2 63	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
65	18 64	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
66	65	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
67	5 63	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
68	67 6	mulgnn0cl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑙 ∈ ℕ0 ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑙 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
69	60 62 66 68	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( 𝑙 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
70		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
71		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
72		eqid	⊢ ( .g ‘ ( Scalar ‘ 𝑃 ) ) = ( .g ‘ ( Scalar ‘ 𝑃 ) )
73	63 70 14 71 10 72	lmodvsmmulgdi	⊢ ( ( 𝑃 ∈ LMod ∧ ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ∈ ℕ0 ∧ ( 𝑙 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) = ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) )
74	21 50 55 69 73	syl13anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) = ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) )
75	46	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( .g ‘ 𝑅 ) = ( .g ‘ ( Scalar ‘ 𝑃 ) ) )
76	15 75	eqtr2id	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( .g ‘ ( Scalar ‘ 𝑃 ) ) = 𝑍 )
77	76	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( .g ‘ ( Scalar ‘ 𝑃 ) ) = 𝑍 )
78	77	oveqd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) = ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) )
79	78	oveq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) = ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) )
80	74 79	eqtrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) = ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) )
81	80	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) = ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) )
82	81	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑃 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) ) = ( 𝑃 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) )
83	16 82	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) )