Metamath Proof Explorer

Theorem pmatcollpwfi

Description: Write a polynomial matrix (over a commutative ring) as a finite sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 4-Nov-2019) (Revised by AV, 4-Dec-2019) (Proof shortened by AV, 3-Jul-2022)

Ref Expression
Hypotheses pmatcollpw.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pmatcollpw.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
pmatcollpw.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
pmatcollpw.m ⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
pmatcollpw.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
pmatcollpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
pmatcollpw.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion pmatcollpwfi ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 pmatcollpw.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 pmatcollpw.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 pmatcollpw.m ⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
5 pmatcollpw.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6 pmatcollpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
7 pmatcollpw.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
8 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
9 8 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
10 simp3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
11 eqid ⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
12 eqid ⊢ ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) )
13 1 2 3 11 12 decpmataa0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) )
14 9 10 13 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) )
15 1 2 3 4 5 6 7 pmatcollpw ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
16 15 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
17 eqid ⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
18 simp1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
19 1 2 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
20 18 9 19 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐶 ∈ Ring )
21 ringcmn ⊢ ( 𝐶 ∈ Ring → 𝐶 ∈ CMnd )
22 20 21 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐶 ∈ CMnd )
23 22 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) ) → 𝐶 ∈ CMnd )
24 18 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ Fin )
25 9 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
26 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
27 25 26 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑃 ∈ Ring )
28 9 anim1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0 ) )
29 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
30 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
31 1 6 29 5 30 ply1moncl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
32 28 31 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
33 simpl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ CRing )
34 10 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
35 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
36 eqid ⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
37 1 2 3 11 36 decpmatcl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
38 33 34 35 37 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
39 7 11 36 1 2 3 mat2pmatbas0 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑀 decompPMat 𝑛 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ∈ 𝐵 )
40 24 25 38 39 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ∈ 𝐵 )
41 30 2 3 4 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ∈ 𝐵 ) ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ∈ 𝐵 )
42 24 27 32 40 41 syl22anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ∈ 𝐵 )
43 42 ralrimiva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ ℕ0 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ∈ 𝐵 )
44 43 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) ) → ∀ 𝑛 ∈ ℕ0 ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ∈ 𝐵 )
45 simplr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) ) → 𝑠 ∈ ℕ0 )
46 fveq2 ⊢ ( ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) = ( 𝑇 ‘ ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) )
47 9 18 jca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
48 47 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) )
49 eqid ⊢ ( 0g ‘ ( 𝑁 Mat 𝑃 ) ) = ( 0g ‘ ( 𝑁 Mat 𝑃 ) )
50 7 1 12 49 0mat2pmat ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝑇 ‘ ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) = ( 0g ‘ ( 𝑁 Mat 𝑃 ) ) )
51 48 50 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) = ( 0g ‘ ( 𝑁 Mat 𝑃 ) ) )
52 46 51 sylan9eqr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) → ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) = ( 0g ‘ ( 𝑁 Mat 𝑃 ) ) )
53 52 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) = ( ( 𝑛 ↑ 𝑋 ) ∗ ( 0g ‘ ( 𝑁 Mat 𝑃 ) ) ) )
54 1 2 pmatlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ LMod )
55 18 9 54 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐶 ∈ LMod )
56 55 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ LMod )
57 28 adantlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0 ) )
58 57 31 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
59 1 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
60 59 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
61 60 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
62 2 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝐶 ) )
63 61 62 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 = ( Scalar ‘ 𝐶 ) )
64 63 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝐶 ) = 𝑃 )
65 64 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( Scalar ‘ 𝐶 ) = 𝑃 )
66 65 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ 𝑃 ) )
67 58 66 eleqtrrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
68 2 eqcomi ⊢ ( 𝑁 Mat 𝑃 ) = 𝐶
69 68 fveq2i ⊢ ( 0g ‘ ( 𝑁 Mat 𝑃 ) ) = ( 0g ‘ 𝐶 )
70 69 oveq2i ⊢ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 0g ‘ ( 𝑁 Mat 𝑃 ) ) ) = ( ( 𝑛 ↑ 𝑋 ) ∗ ( 0g ‘ 𝐶 ) )
71 eqid ⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
72 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
73 71 4 72 17 lmodvs0 ⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 0g ‘ 𝐶 ) ) = ( 0g ‘ 𝐶 ) )
74 70 73 syl5eq ⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑛 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 0g ‘ ( 𝑁 Mat 𝑃 ) ) ) = ( 0g ‘ 𝐶 ) )
75 56 67 74 syl2anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 0g ‘ ( 𝑁 Mat 𝑃 ) ) ) = ( 0g ‘ 𝐶 ) )
76 75 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 0g ‘ ( 𝑁 Mat 𝑃 ) ) ) = ( 0g ‘ 𝐶 ) )
77 53 76 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) )
78 77 ex ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) )
79 78 imim2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) → ( 𝑠 < 𝑛 → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
80 79 ralimdva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
81 80 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) )
82 3 17 23 44 45 81 gsummptnn0fz ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) ) → ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
83 16 82 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
84 83 ex ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) ) )
85 84 reximdva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( 𝑠 < 𝑛 → ( 𝑀 decompPMat 𝑛 ) = ( 0g ‘ ( 𝑁 Mat 𝑅 ) ) ) → ∃ 𝑠 ∈ ℕ0 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) ) )
86 14 85 mpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ0 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )