chpscmatgsumbin

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

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

Proof

Step	Hyp	Ref	Expression
1		chp0mat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2		chp0mat.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
3		chp0mat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		chp0mat.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
5		chp0mat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
6		chp0mat.m	⊢ ↑ = ( ._g ‘ 𝐺 )
7		chpscmat.d	⊢ 𝐷 = { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0_g ‘ 𝑅 ) ) }
8		chpscmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
9		chpscmat.m	⊢ − = ( -_g ‘ 𝑃 )
10		chpscmatgsum.f	⊢ 𝐹 = ( ._g ‘ 𝑃 )
11		chpscmatgsum.h	⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
12		chpscmatgsum.e	⊢ 𝐸 = ( ._g ‘ 𝐻 )
13		chpscmatgsum.i	⊢ 𝐼 = ( inv_g ‘ 𝑅 )
14		chpscmatgsum.s	⊢ · = ( ·_𝑠 ‘ 𝑃 )
15	1 2 3 4 5 6 7 8 9	chpscmat0	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐶 ‘ 𝑀 ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) )
16		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
17	16	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
18		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
19	4 2 18	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
20	17 19	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
21	20	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
22	16	ad2antlr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → 𝑅 ∈ Ring )
23		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
24	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
25	2	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
26		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
27	8 23 24 25 26 18	asclf	⊢ ( 𝑅 ∈ Ring → 𝑆 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ ( Base ‘ 𝑃 ) )
28	22 27	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → 𝑆 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ ( Base ‘ 𝑃 ) )
29		simpr2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → 𝐽 ∈ 𝑁 )
30		elrabi	⊢ ( 𝑀 ∈ { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0_g ‘ 𝑅 ) ) } → 𝑀 ∈ ( Base ‘ 𝐴 ) )
31	30	a1d	⊢ ( 𝑀 ∈ { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0_g ‘ 𝑅 ) ) } → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑀 ∈ ( Base ‘ 𝐴 ) ) )
32	31 7	eleq2s	⊢ ( 𝑀 ∈ 𝐷 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑀 ∈ ( Base ‘ 𝐴 ) ) )
33	32	3ad2ant1	⊢ ( ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑀 ∈ ( Base ‘ 𝐴 ) ) )
34	33	impcom	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
35		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
36	3 35	matecl	⊢ ( ( 𝐽 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
37	29 29 34 36	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
38	2	ply1sca	⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
39	38	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
40	39	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
41	40	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
42	41	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
43	37 42	eleqtrrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
44	28 43	ffvelcdmd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑃 ) )
45		eqid	⊢ ( +_g ‘ 𝑃 ) = ( +_g ‘ 𝑃 )
46		eqid	⊢ ( inv_g ‘ 𝑃 ) = ( inv_g ‘ 𝑃 )
47	18 45 46 9	grpsubval	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 − ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) = ( 𝑋 ( +_g ‘ 𝑃 ) ( ( inv_g ‘ 𝑃 ) ‘ ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) )
48	21 44 47	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑋 − ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) = ( 𝑋 ( +_g ‘ 𝑃 ) ( ( inv_g ‘ 𝑃 ) ‘ ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) )
49	17 25	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ LMod )
50	49	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → 𝑃 ∈ LMod )
51	17 24	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ Ring )
52	51	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → 𝑃 ∈ Ring )
53		eqid	⊢ ( inv_g ‘ ( Scalar ‘ 𝑃 ) ) = ( inv_g ‘ ( Scalar ‘ 𝑃 ) )
54	8 23 26 53 46	asclinvg	⊢ ( ( 𝑃 ∈ LMod ∧ 𝑃 ∈ Ring ∧ ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → ( ( inv_g ‘ 𝑃 ) ‘ ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) = ( 𝑆 ‘ ( ( inv_g ‘ ( Scalar ‘ 𝑃 ) ) ‘ ( 𝐽 𝑀 𝐽 ) ) ) )
55	50 52 43 54	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( ( inv_g ‘ 𝑃 ) ‘ ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) = ( 𝑆 ‘ ( ( inv_g ‘ ( Scalar ‘ 𝑃 ) ) ‘ ( 𝐽 𝑀 𝐽 ) ) ) )
56	39	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( inv_g ‘ 𝑅 ) = ( inv_g ‘ ( Scalar ‘ 𝑃 ) ) )
57	56	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( inv_g ‘ 𝑅 ) = ( inv_g ‘ ( Scalar ‘ 𝑃 ) ) )
58	13 57	eqtr2id	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( inv_g ‘ ( Scalar ‘ 𝑃 ) ) = 𝐼 )
59	58	fveq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( ( inv_g ‘ ( Scalar ‘ 𝑃 ) ) ‘ ( 𝐽 𝑀 𝐽 ) ) = ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) )
60	59	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑆 ‘ ( ( inv_g ‘ ( Scalar ‘ 𝑃 ) ) ‘ ( 𝐽 𝑀 𝐽 ) ) ) = ( 𝑆 ‘ ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) )
61	55 60	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( ( inv_g ‘ 𝑃 ) ‘ ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) = ( 𝑆 ‘ ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) )
62	61	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑋 ( +_g ‘ 𝑃 ) ( ( inv_g ‘ 𝑃 ) ‘ ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) = ( 𝑋 ( +_g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) )
63	48 62	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑋 − ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) = ( 𝑋 ( +_g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) )
64	63	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 ( +_g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ) )
65		simplr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → 𝑅 ∈ CRing )
66		hashcl	⊢ ( 𝑁 ∈ Fin → ( ♯ ‘ 𝑁 ) ∈ ℕ₀ )
67	66	ad2antrr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( ♯ ‘ 𝑁 ) ∈ ℕ₀ )
68		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
69	16 68	syl	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Grp )
70	69	ad2antlr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → 𝑅 ∈ Grp )
71	35 13	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐽 𝑀 𝐽 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑅 ) )
72	70 37 71	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑅 ) )
73		eqid	⊢ ( ._r ‘ 𝑃 ) = ( ._r ‘ 𝑃 )
74	2 4 45 73 10 5 6 35 8 11 12	lply1binomsc	⊢ ( ( 𝑅 ∈ CRing ∧ ( ♯ ‘ 𝑁 ) ∈ ℕ₀ ∧ ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 ( +_g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ) = ( 𝑃 Σ_g ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( 𝑆 ‘ ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ( ._r ‘ 𝑃 ) ( 𝑙 ↑ 𝑋 ) ) ) ) ) )
75	65 67 72 74	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 ( +_g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ) = ( 𝑃 Σ_g ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( 𝑆 ‘ ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ( ._r ‘ 𝑃 ) ( 𝑙 ↑ 𝑋 ) ) ) ) ) )
76	2	ply1assa	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )
77	76	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ AssAlg )
78	77	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝑃 ∈ AssAlg )
79		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
80	11	ringmgp	⊢ ( 𝑅 ∈ Ring → 𝐻 ∈ Mnd )
81	17 80	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐻 ∈ Mnd )
82	81	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝐻 ∈ Mnd )
83		fznn0sub	⊢ ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) → ( ( ♯ ‘ 𝑁 ) − 𝑙 ) ∈ ℕ₀ )
84	83	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ♯ ‘ 𝑁 ) − 𝑙 ) ∈ ℕ₀ )
85	11 35	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐻 )
86	72 85	eleqtrdi	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝐻 ) )
87	86	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ∈ ( Base ‘ 𝐻 ) )
88	79 12 82 84 87	mulgnn0cld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ∈ ( Base ‘ 𝐻 ) )
89	40	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
90	89 85	eqtrdi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝐻 ) )
91	90	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝐻 ) )
92	88 91	eleqtrrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
93	5 18	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
94	5	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝐺 ∈ Mnd )
95	16 24 94	3syl	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ Mnd )
96	95	ad2antlr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝐺 ∈ Mnd )
97		elfznn0	⊢ ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) → 𝑙 ∈ ℕ₀ )
98	97	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝑙 ∈ ℕ₀ )
99	20	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
100	93 6 96 98 99	mulgnn0cld	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( 𝑙 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
101	100	adantlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( 𝑙 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
102	8 23 26 18 73 14	asclmul1	⊢ ( ( 𝑃 ∈ AssAlg ∧ ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑙 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑆 ‘ ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ( ._r ‘ 𝑃 ) ( 𝑙 ↑ 𝑋 ) ) = ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) )
103	78 92 101 102	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( 𝑆 ‘ ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ( ._r ‘ 𝑃 ) ( 𝑙 ↑ 𝑋 ) ) = ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) )
104	103	oveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) ∧ 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ) → ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( 𝑆 ‘ ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ( ._r ‘ 𝑃 ) ( 𝑙 ↑ 𝑋 ) ) ) = ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) )
105	104	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( 𝑆 ‘ ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ( ._r ‘ 𝑃 ) ( 𝑙 ↑ 𝑋 ) ) ) ) = ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) )
106	105	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝑃 Σ_g ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( 𝑆 ‘ ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ( ._r ‘ 𝑃 ) ( 𝑙 ↑ 𝑋 ) ) ) ) ) = ( 𝑃 Σ_g ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) ) )
107	75 106	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 ( +_g ‘ 𝑃 ) ( 𝑆 ‘ ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) ) ) = ( 𝑃 Σ_g ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) ) )
108	15 64 107	3eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐽 𝑀 𝐽 ) ) ) → ( 𝐶 ‘ 𝑀 ) = ( 𝑃 Σ_g ( 𝑙 ∈ ( 0 ... ( ♯ ‘ 𝑁 ) ) ↦ ( ( ( ♯ ‘ 𝑁 ) C 𝑙 ) 𝐹 ( ( ( ( ♯ ‘ 𝑁 ) − 𝑙 ) 𝐸 ( 𝐼 ‘ ( 𝐽 𝑀 𝐽 ) ) ) · ( 𝑙 ↑ 𝑋 ) ) ) ) ) )

Metamath Proof Explorer

Theorem chpscmatgsumbin

Proof