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		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23	11 22	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐻 )
24	11	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝐻 ∈ Mnd )
25	18 24	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐻 ∈ Mnd )
26	25	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝐻 ∈ Mnd )
27		fznn0sub	⊢ ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) → ( ( ♯ ‘ 𝑁 ) − 𝑙 ) ∈ ℕ0 )
28	27	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ♯ ‘ 𝑁 ) − 𝑙 ) ∈ ℕ0 )
29		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
30	17 29	syl	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Grp )
31	30	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Grp )
32		simp2	⊢ ( ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) → 𝐽 ∈ 𝑁 )
33		elrabi	⊢ ( 𝑀 ∈ { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑅 ) ) } → 𝑀 ∈ ( Base ‘ 𝐴 ) )
34	33 7	eleq2s	⊢ ( 𝑀 ∈ 𝐷 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
35	34	3ad2ant1	⊢ ( ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
36	32 32 35	3jca	⊢ ( ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) → ( 𝐽 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) )
37	36	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐽 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) )
38	3 22	matecl	⊢ ( ( 𝐽 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
39	37 38	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
40	22 13	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑅 ) )
41	31 39 40	syl2an2r	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑅 ) )
42	41	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑅 ) )
43	23 12 26 28 42	mulgnn0cld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ∈ ( Base ‘ 𝑅 ) )
44	2	ply1sca	⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
45	44	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
46	45	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
47	46	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
48	47	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
49	43 48	eleqtrrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
50		hashcl	⊢ ( 𝑁 ∈ Fin → ( ♯ ‘ 𝑁 ) ∈ ℕ0 )
51	50	ad2antrr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( ♯ ‘ 𝑁 ) ∈ ℕ0 )
52		elfzelz	⊢ ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) → 𝑙 ∈ ℤ )
53		bccl	⊢ ( ( ( ♯ ‘ 𝑁 ) ∈ ℕ0 ∧ 𝑙 ∈ ℤ ) → ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ∈ ℕ0 )
54	51 52 53	syl2an	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ∈ ℕ0 )
55		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
56	5 55	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
57	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
58	5	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝐺 ∈ Mnd )
59	17 57 58	3syl	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Mnd )
60	59	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐺 ∈ Mnd )
61	60	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝐺 ∈ Mnd )
62		elfznn0	⊢ ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) → 𝑙 ∈ ℕ0 )
63	62	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝑙 ∈ ℕ0 )
64	4 2 55	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
65	18 64	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
66	65	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
67	56 6 61 63 66	mulgnn0cld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( 𝑙 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
68		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
69		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
70		eqid	⊢ ( .g ‘ ( Scalar ‘ 𝑃 ) ) = ( .g ‘ ( Scalar ‘ 𝑃 ) )
71	55 68 14 69 10 70	lmodvsmmulgdi	⊢ ( ( 𝑃 ∈ LMod ∧ ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ∈ ℕ0 ∧ ( 𝑙 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) = ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) )
72	21 49 54 67 71	syl13anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) = ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) )
73	45	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( .g ‘ 𝑅 ) = ( .g ‘ ( Scalar ‘ 𝑃 ) ) )
74	15 73	eqtr2id	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( .g ‘ ( Scalar ‘ 𝑃 ) ) = 𝑍 )
75	74	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( .g ‘ ( Scalar ‘ 𝑃 ) ) = 𝑍 )
76	75	oveqd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) = ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) )
77	76	oveq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) ( .g ‘ ( Scalar ‘ 𝑃 ) ) ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) = ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) )
78	72 77	eqtrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) = ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) )
79	78	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) = ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) )
80	79	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑃 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) ) = ( 𝑃 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) )
81	16 80	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σg ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝑍 ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) )