Metamath Proof Explorer


Theorem pmatcollpw3

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

Ref Expression
Hypotheses pmatcollpw.p 𝑃 = ( Poly1𝑅 )
pmatcollpw.c 𝐶 = ( 𝑁 Mat 𝑃 )
pmatcollpw.b 𝐵 = ( Base ‘ 𝐶 )
pmatcollpw.m = ( ·𝑠𝐶 )
pmatcollpw.e = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
pmatcollpw.x 𝑋 = ( var1𝑅 )
pmatcollpw.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
pmatcollpw3.a 𝐴 = ( 𝑁 Mat 𝑅 )
pmatcollpw3.d 𝐷 = ( Base ‘ 𝐴 )
Assertion pmatcollpw3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ∃ 𝑓 ∈ ( 𝐷m0 ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑋 ) ( 𝑇 ‘ ( 𝑓𝑛 ) ) ) ) ) )

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 pmatcollpw3.a 𝐴 = ( 𝑁 Mat 𝑅 )
9 pmatcollpw3.d 𝐷 = ( Base ‘ 𝐴 )
10 1 2 3 4 5 6 7 pmatcollpw ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑋 ) ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
11 ssid 0 ⊆ ℕ0
12 0nn0 0 ∈ ℕ0
13 12 ne0ii 0 ≠ ∅
14 1 2 3 4 5 6 7 8 9 pmatcollpw3lem ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( ℕ0 ⊆ ℕ0 ∧ ℕ0 ≠ ∅ ) ) → ( 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑋 ) ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) → ∃ 𝑓 ∈ ( 𝐷m0 ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑋 ) ( 𝑇 ‘ ( 𝑓𝑛 ) ) ) ) ) ) )
15 11 13 14 mpanr12 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑋 ) ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) → ∃ 𝑓 ∈ ( 𝐷m0 ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑋 ) ( 𝑇 ‘ ( 𝑓𝑛 ) ) ) ) ) ) )
16 10 15 mpd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ∃ 𝑓 ∈ ( 𝐷m0 ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑋 ) ( 𝑇 ‘ ( 𝑓𝑛 ) ) ) ) ) )