Metamath Proof Explorer

Definition df-cpmat2mat

Description: Transformation of a constant polynomial matrix (over a ring) into a matrix over the corresponding ring. Since this function is the inverse function of matToPolyMat , see m2cpminv , it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019)

Ref Expression
Assertion df-cpmat2mat ⊢ cPolyMatToMat = n ∈ Fin , r ∈ V ⟼ m ∈ n ConstPolyMat r ⟼ x ∈ n , y ∈ n ⟼ coe 1 ⁡ x m y ⁡ 0

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccpmat2mat class cPolyMatToMat
1 vn setvar n
2 cfn class Fin
3 vr setvar r
4 cvv class V
5 vm setvar m
6 1 cv setvar n
7 ccpmat class ConstPolyMat
8 3 cv setvar r
9 6 8 7 co class n ConstPolyMat r
10 vx setvar x
11 vy setvar y
12 cco1 class coe 1
13 10 cv setvar x
14 5 cv setvar m
15 11 cv setvar y
16 13 15 14 co class x m y
17 16 12 cfv class coe 1 ⁡ x m y
18 cc0 class 0
19 18 17 cfv class coe 1 ⁡ x m y ⁡ 0
20 10 11 6 6 19 cmpo class x ∈ n , y ∈ n ⟼ coe 1 ⁡ x m y ⁡ 0
21 5 9 20 cmpt class m ∈ n ConstPolyMat r ⟼ x ∈ n , y ∈ n ⟼ coe 1 ⁡ x m y ⁡ 0
22 1 3 2 4 21 cmpo class n ∈ Fin , r ∈ V ⟼ m ∈ n ConstPolyMat r ⟼ x ∈ n , y ∈ n ⟼ coe 1 ⁡ x m y ⁡ 0
23 0 22 wceq wff cPolyMatToMat = n ∈ Fin , r ∈ V ⟼ m ∈ n ConstPolyMat r ⟼ x ∈ n , y ∈ n ⟼ coe 1 ⁡ x m y ⁡ 0