Metamath Proof Explorer

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 ) ) ) ) ) )