Metamath Proof Explorer

Theorem decpmatval0

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power, most general version. (Contributed by AV, 2-Dec-2019)

Ref Expression
Assertion decpmatval0 ( ( 𝑀 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) = ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 df-decpmat ⊢ decompPMat = ( 𝑚 ∈ V , 𝑘 ∈ ℕ0 ↦ ( 𝑖 ∈ dom dom 𝑚 , 𝑗 ∈ dom dom 𝑚 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) )
2 1 a1i ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → decompPMat = ( 𝑚 ∈ V , 𝑘 ∈ ℕ0 ↦ ( 𝑖 ∈ dom dom 𝑚 , 𝑗 ∈ dom dom 𝑚 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) ) )
3 dmeq ⊢ ( 𝑚 = 𝑀 → dom 𝑚 = dom 𝑀 )
4 3 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ) → dom 𝑚 = dom 𝑀 )
5 4 dmeqd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ) → dom dom 𝑚 = dom dom 𝑀 )
6 oveq ⊢ ( 𝑚 = 𝑀 → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
7 6 fveq2d ⊢ ( 𝑚 = 𝑀 → ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) )
8 7 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ) → ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) )
9 simpr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ) → 𝑘 = 𝐾 )
10 8 9 fveq12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ) → ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) )
11 5 5 10 mpoeq123dv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ) → ( 𝑖 ∈ dom dom 𝑚 , 𝑗 ∈ dom dom 𝑚 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )
12 11 adantl ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑘 = 𝐾 ) ) → ( 𝑖 ∈ dom dom 𝑚 , 𝑗 ∈ dom dom 𝑚 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )
13 elex ⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
14 13 adantr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → 𝑀 ∈ V )
15 simpr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
16 dmexg ⊢ ( 𝑀 ∈ 𝑉 → dom 𝑀 ∈ V )
17 16 dmexd ⊢ ( 𝑀 ∈ 𝑉 → dom dom 𝑀 ∈ V )
18 17 17 jca ⊢ ( 𝑀 ∈ 𝑉 → ( dom dom 𝑀 ∈ V ∧ dom dom 𝑀 ∈ V ) )
19 18 adantr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( dom dom 𝑀 ∈ V ∧ dom dom 𝑀 ∈ V ) )
20 mpoexga ⊢ ( ( dom dom 𝑀 ∈ V ∧ dom dom 𝑀 ∈ V ) → ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) ∈ V )
21 19 20 syl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) ∈ V )
22 2 12 14 15 21 ovmpod ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 decompPMat 𝐾 ) = ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝐾 ) ) )