Metamath Proof Explorer

Theorem decpmatcl

Description: Closure of the decomposition of a polynomial matrix: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power is a matrix. (Contributed by AV, 28-Sep-2019) (Revised by AV, 2-Dec-2019)

Ref Expression
Hypotheses decpmate.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
decpmate.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
decpmate.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
decpmatcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
decpmatcl.d ⊢ 𝐷 = ( Base ‘ 𝐴 )
Assertion decpmatcl ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 decpmate.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 decpmate.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 decpmate.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 decpmatcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
5 decpmatcl.d ⊢ 𝐷 = ( Base ‘ 𝐴 )
6 2 3 decpmatval ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )
7 6 3adant1 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 2 3 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ V ) )
10 9 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
11 10 3ad2ant2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ Fin )
12 simp1 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → 𝑅 ∈ 𝑉 )
13 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
14 simp2 ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
15 simp3 ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
16 simp2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → 𝑀 ∈ 𝐵 )
17 16 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
18 2 13 3 14 15 17 matecld ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
19 simp3 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
20 19 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐾 ∈ ℕ0 )
21 eqid ⊢ ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) )
22 21 13 1 8 coe1fvalcl ⊢ ( ( ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝐾 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ∈ ( Base ‘ 𝑅 ) )
23 18 20 22 syl2anc ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ∈ ( Base ‘ 𝑅 ) )
24 4 8 5 11 12 23 matbas2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) ∈ 𝐷 )
25 7 24 eqeltrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) ∈ 𝐷 )