Theorem cpmadugsumfi

Description: The product of the characteristic matrix of a given matrix and its adjunct represented as finite sum. (Contributed by AV, 7-Nov-2019) (Proof shortened by AV, 29-Nov-2019)

	Ref	Expression
Hypotheses	cpmadugsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cpmadugsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cpmadugsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmadugsum.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	cpmadugsum.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	cpmadugsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	cpmadugsum.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	cpmadugsum.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
	cpmadugsum.r	⊢ × = ( .r ‘ 𝑌 )
	cpmadugsum.1	⊢ 1 = ( 1r ‘ 𝑌 )
	cpmadugsum.g	⊢ + = ( +g ‘ 𝑌 )
	cpmadugsum.s	⊢ − = ( -g ‘ 𝑌 )
	cpmadugsum.i	⊢ 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
	cpmadugsum.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
Assertion	cpmadugsumfi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cpmadugsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cpmadugsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cpmadugsum.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		cpmadugsum.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		cpmadugsum.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
6		cpmadugsum.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
7		cpmadugsum.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
8		cpmadugsum.m	⊢ · = ( ·𝑠 ‘ 𝑌 )
9		cpmadugsum.r	⊢ × = ( .r ‘ 𝑌 )
10		cpmadugsum.1	⊢ 1 = ( 1r ‘ 𝑌 )
11		cpmadugsum.g	⊢ + = ( +g ‘ 𝑌 )
12		cpmadugsum.s	⊢ − = ( -g ‘ 𝑌 )
13		cpmadugsum.i	⊢ 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) )
14		cpmadugsum.j	⊢ 𝐽 = ( 𝑁 maAdju 𝑃 )
15		oveq2	⊢ ( ( 𝐽 ‘ 𝐼 ) = ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( 𝐼 × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) )
16	13	a1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝐼 = ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) )
17	16	oveq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝐼 × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) )
18		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
19		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
20	19	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
21	20	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
22	21	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
23	3 4	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
24	22 23	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑌 ∈ Ring )
25	3 4	pmatlmod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ LMod )
26	19 25	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ LMod )
27	19	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
28		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
29	6 3 28	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
30	27 29	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
31	3	ply1crng	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
32	4	matsca2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
33	31 32	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
34	33	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
35	30 34	eleqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
36	19 23	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Ring )
37	18 10	ringidcl	⊢ ( 𝑌 ∈ Ring → 1 ∈ ( Base ‘ 𝑌 ) )
38	36 37	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 1 ∈ ( Base ‘ 𝑌 ) )
39		eqid	⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
40		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
41	18 39 8 40	lmodvscl	⊢ ( ( 𝑌 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ 1 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
42	26 35 38 41	syl3anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
43	42	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
44	43	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑋 · 1 ) ∈ ( Base ‘ 𝑌 ) )
45	5 1 2 3 4	mat2pmatbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
46	19 45	syl3an2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
47	46	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑇 ‘ 𝑀 ) ∈ ( Base ‘ 𝑌 ) )
48		ringcmn	⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ CMnd )
49	36 48	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ CMnd )
50	49	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑌 ∈ CMnd )
51	50	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝑌 ∈ CMnd )
52		fzfid	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 0 ... 𝑠 ) ∈ Fin )
53	21	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ( 0 ... 𝑠 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
54		elmapi	⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) → 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 )
55		ffvelcdm	⊢ ( ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 ∧ 𝑛 ∈ ( 0 ... 𝑠 ) ) → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 )
56	55	ex	⊢ ( 𝑏 : ( 0 ... 𝑠 ) ⟶ 𝐵 → ( 𝑛 ∈ ( 0 ... 𝑠 ) → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) )
57	54 56	syl	⊢ ( 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) → ( 𝑛 ∈ ( 0 ... 𝑠 ) → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) )
58	57	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑛 ∈ ( 0 ... 𝑠 ) → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ) )
59	58	imp	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ( 0 ... 𝑠 ) ) → ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 )
60		elfznn0	⊢ ( 𝑛 ∈ ( 0 ... 𝑠 ) → 𝑛 ∈ ℕ0 )
61	60	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ( 0 ... 𝑠 ) ) → 𝑛 ∈ ℕ0 )
62	1 2 5 3 4 18 8 7 6	mat2pmatscmxcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑏 ‘ 𝑛 ) ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ∈ ( Base ‘ 𝑌 ) )
63	53 59 61 62	syl12anc	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ( 0 ... 𝑠 ) ) → ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ∈ ( Base ‘ 𝑌 ) )
64	63	ralrimiva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ∀ 𝑛 ∈ ( 0 ... 𝑠 ) ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ∈ ( Base ‘ 𝑌 ) )
65	18 51 52 64	gsummptcl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑌 ) )
66	18 9 12 24 44 47 65	ringsubdir	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( ( 𝑋 · 1 ) − ( 𝑇 ‘ 𝑀 ) ) × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = ( ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
67		oveq1	⊢ ( 𝑛 = 𝑖 → ( 𝑛 ↑ 𝑋 ) = ( 𝑖 ↑ 𝑋 ) )
68		2fveq3	⊢ ( 𝑛 = 𝑖 → ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) = ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) )
69	67 68	oveq12d	⊢ ( 𝑛 = 𝑖 → ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) = ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) )
70	69	cbvmptv	⊢ ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) )
71	70	oveq2i	⊢ ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) = ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) )
72	71	oveq2i	⊢ ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
73	71	oveq2i	⊢ ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
74	72 73	oveq12i	⊢ ( ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
75	1 2 3 4 5 6 7 8 9 10 11 12	cpmadugsumlemF	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
76	75	anassrs	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑖 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
77	74 76	eqtrid	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( ( 𝑋 · 1 ) × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
78	17 66 77	3eqtrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝐼 × ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
79	15 78	sylan9eqr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ ( 𝐽 ‘ 𝐼 ) = ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) → ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )
80	4 14 18	maduf	⊢ ( 𝑃 ∈ CRing → 𝐽 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑌 ) )
81	31 80	syl	⊢ ( 𝑅 ∈ CRing → 𝐽 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑌 ) )
82	81	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐽 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑌 ) )
83	1 2 3 4 6 5 12 8 10 13	chmatcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝐼 ∈ ( Base ‘ 𝑌 ) )
84	19 83	syl3an2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐼 ∈ ( Base ‘ 𝑌 ) )
85	82 84	ffvelcdmd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐽 ‘ 𝐼 ) ∈ ( Base ‘ 𝑌 ) )
86	3 4 18 8 7 6 5 1 2	pmatcollpw3fi1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ ( 𝐽 ‘ 𝐼 ) ∈ ( Base ‘ 𝑌 ) ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐽 ‘ 𝐼 ) = ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) )
87	85 86	syld3an3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐽 ‘ 𝐼 ) = ( 𝑌 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) )
88	79 87	reximddv2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐼 × ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝑌 Σg ( 𝑖 ∈ ( 1 ... 𝑠 ) ↦ ( ( 𝑖 ↑ 𝑋 ) · ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) + ( ( ( ( 𝑠 + 1 ) ↑ 𝑋 ) · ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) ) )