Metamath Proof Explorer

Definition df-mat2pmat

Description: Transformation of a matrix (over a ring) into a matrix over the corresponding polynomial ring. (Contributed by AV, 31-Jul-2019)

Ref Expression
Assertion df-mat2pmat ⊢ matToPolyMat = n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat r ⟼ x ∈ n , y ∈ n ⟼ algSc ⁡ Poly 1 ⁡ r ⁡ x m y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmat2pmat class matToPolyMat
1 vn setvar n
2 cfn class Fin
3 vr setvar r
4 cvv class V
5 vm setvar m
6 cbs class Base
7 1 cv setvar n
8 cmat class Mat
9 3 cv setvar r
10 7 9 8 co class n Mat r
11 10 6 cfv class Base n Mat r
12 vx setvar x
13 vy setvar y
14 cascl class algSc
15 cpl1 class Poly 1
16 9 15 cfv class Poly 1 ⁡ r
17 16 14 cfv class algSc ⁡ Poly 1 ⁡ r
18 12 cv setvar x
19 5 cv setvar m
20 13 cv setvar y
21 18 20 19 co class x m y
22 21 17 cfv class algSc ⁡ Poly 1 ⁡ r ⁡ x m y
23 12 13 7 7 22 cmpo class x ∈ n , y ∈ n ⟼ algSc ⁡ Poly 1 ⁡ r ⁡ x m y
24 5 11 23 cmpt class m ∈ Base n Mat r ⟼ x ∈ n , y ∈ n ⟼ algSc ⁡ Poly 1 ⁡ r ⁡ x m y
25 1 3 2 4 24 cmpo class n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat r ⟼ x ∈ n , y ∈ n ⟼ algSc ⁡ Poly 1 ⁡ r ⁡ x m y
26 0 25 wceq wff matToPolyMat = n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat r ⟼ x ∈ n , y ∈ n ⟼ algSc ⁡ Poly 1 ⁡ r ⁡ x m y