Metamath Proof Explorer

Theorem mply1topmatval

Description: A polynomial over matrices transformed into a polynomial matrix. I is the inverse function of the transformation T of polynomial matrices into polynomials over matrices: ( T( IO ) ) = O ) (see mp2pm2mp ). (Contributed by AV, 6-Oct-2019)

Ref Expression
Hypotheses mply1topmat.a ⊢ A = N Mat R
mply1topmat.q ⊢ Q = Poly 1 ⁡ A
mply1topmat.l ⊢ L = Base Q
mply1topmat.p ⊢ P = Poly 1 ⁡ R
mply1topmat.m ⊢ · ˙ = ⋅ P
mply1topmat.e ⊢ E = ⋅ mulGrp P
mply1topmat.y ⊢ Y = var 1 ⁡ R
mply1topmat.i ⊢ I = p ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ p ⁡ k j · ˙ k E Y
Assertion mply1topmatval ⊢ N ∈ V ∧ O ∈ L → I ⁡ O = i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y

Proof

Step Hyp Ref Expression
1 mply1topmat.a ⊢ A = N Mat R
2 mply1topmat.q ⊢ Q = Poly 1 ⁡ A
3 mply1topmat.l ⊢ L = Base Q
4 mply1topmat.p ⊢ P = Poly 1 ⁡ R
5 mply1topmat.m ⊢ · ˙ = ⋅ P
6 mply1topmat.e ⊢ E = ⋅ mulGrp P
7 mply1topmat.y ⊢ Y = var 1 ⁡ R
8 mply1topmat.i ⊢ I = p ∈ L ⟼ i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ p ⁡ k j · ˙ k E Y
9 fveq2 ⊢ p = O → coe 1 ⁡ p = coe 1 ⁡ O
10 9 fveq1d ⊢ p = O → coe 1 ⁡ p ⁡ k = coe 1 ⁡ O ⁡ k
11 10 oveqd ⊢ p = O → i coe 1 ⁡ p ⁡ k j = i coe 1 ⁡ O ⁡ k j
12 11 oveq1d ⊢ p = O → i coe 1 ⁡ p ⁡ k j · ˙ k E Y = i coe 1 ⁡ O ⁡ k j · ˙ k E Y
13 12 mpteq2dv ⊢ p = O → k ∈ ℕ 0 ⟼ i coe 1 ⁡ p ⁡ k j · ˙ k E Y = k ∈ ℕ 0 ⟼ i coe 1 ⁡ O ⁡ k j · ˙ k E Y
14 13 oveq2d ⊢ p = O → ∑ P k ∈ ℕ 0 i coe 1 ⁡ p ⁡ k j · ˙ k E Y = ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y
15 14 mpoeq3dv ⊢ p = O → i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ p ⁡ k j · ˙ k E Y = i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y
16 simpr ⊢ N ∈ V ∧ O ∈ L → O ∈ L
17 simpl ⊢ N ∈ V ∧ O ∈ L → N ∈ V
18 mpoexga ⊢ N ∈ V ∧ N ∈ V → i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y ∈ V
19 17 18 syldan ⊢ N ∈ V ∧ O ∈ L → i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y ∈ V
20 8 15 16 19 fvmptd3 ⊢ N ∈ V ∧ O ∈ L → I ⁡ O = i ∈ N , j ∈ N ⟼ ∑ P k ∈ ℕ 0 i coe 1 ⁡ O ⁡ k j · ˙ k E Y