Metamath Proof Explorer


Theorem pm2mpval

Description: Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed by AV, 5-Dec-2019)

Ref Expression
Hypotheses pm2mpval.p 𝑃 = ( Poly1𝑅 )
pm2mpval.c 𝐶 = ( 𝑁 Mat 𝑃 )
pm2mpval.b 𝐵 = ( Base ‘ 𝐶 )
pm2mpval.m = ( ·𝑠𝑄 )
pm2mpval.e = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
pm2mpval.x 𝑋 = ( var1𝐴 )
pm2mpval.a 𝐴 = ( 𝑁 Mat 𝑅 )
pm2mpval.q 𝑄 = ( Poly1𝐴 )
pm2mpval.t 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion pm2mpval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝑇 = ( 𝑚𝐵 ↦ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pm2mpval.p 𝑃 = ( Poly1𝑅 )
2 pm2mpval.c 𝐶 = ( 𝑁 Mat 𝑃 )
3 pm2mpval.b 𝐵 = ( Base ‘ 𝐶 )
4 pm2mpval.m = ( ·𝑠𝑄 )
5 pm2mpval.e = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6 pm2mpval.x 𝑋 = ( var1𝐴 )
7 pm2mpval.a 𝐴 = ( 𝑁 Mat 𝑅 )
8 pm2mpval.q 𝑄 = ( Poly1𝐴 )
9 pm2mpval.t 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
10 df-pm2mp pMatToMatPoly = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1𝑟 ) ) ) ↦ ( 𝑛 Mat 𝑟 ) / 𝑎 ( Poly1𝑎 ) / 𝑞 ( 𝑞 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠𝑞 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1𝑎 ) ) ) ) ) ) )
11 10 a1i ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → pMatToMatPoly = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1𝑟 ) ) ) ↦ ( 𝑛 Mat 𝑟 ) / 𝑎 ( Poly1𝑎 ) / 𝑞 ( 𝑞 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠𝑞 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1𝑎 ) ) ) ) ) ) ) )
12 simpl ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → 𝑛 = 𝑁 )
13 fveq2 ( 𝑟 = 𝑅 → ( Poly1𝑟 ) = ( Poly1𝑅 ) )
14 13 adantl ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( Poly1𝑟 ) = ( Poly1𝑅 ) )
15 12 14 oveq12d ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( 𝑛 Mat ( Poly1𝑟 ) ) = ( 𝑁 Mat ( Poly1𝑅 ) ) )
16 15 fveq2d ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat ( Poly1𝑟 ) ) ) = ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) )
17 1 oveq2i ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat ( Poly1𝑅 ) )
18 2 17 eqtri 𝐶 = ( 𝑁 Mat ( Poly1𝑅 ) )
19 18 fveq2i ( Base ‘ 𝐶 ) = ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) )
20 3 19 eqtri 𝐵 = ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) )
21 16 20 eqtr4di ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat ( Poly1𝑟 ) ) ) = 𝐵 )
22 21 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) ∧ ( 𝑛 = 𝑁𝑟 = 𝑅 ) ) → ( Base ‘ ( 𝑛 Mat ( Poly1𝑟 ) ) ) = 𝐵 )
23 ovex ( 𝑛 Mat 𝑟 ) ∈ V
24 fvexd ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( Poly1𝑎 ) ∈ V )
25 simpr ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → 𝑞 = ( Poly1𝑎 ) )
26 fveq2 ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( Poly1𝑎 ) = ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) )
27 26 adantr ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → ( Poly1𝑎 ) = ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) )
28 25 27 eqtrd ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → 𝑞 = ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) )
29 28 fveq2d ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → ( ·𝑠𝑞 ) = ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) )
30 eqidd ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → ( 𝑚 decompPMat 𝑘 ) = ( 𝑚 decompPMat 𝑘 ) )
31 28 fveq2d ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → ( mulGrp ‘ 𝑞 ) = ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) )
32 31 fveq2d ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → ( .g ‘ ( mulGrp ‘ 𝑞 ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) )
33 eqidd ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → 𝑘 = 𝑘 )
34 fveq2 ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( var1𝑎 ) = ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) )
35 34 adantr ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → ( var1𝑎 ) = ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) )
36 32 33 35 oveq123d ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1𝑎 ) ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) )
37 29 30 36 oveq123d ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠𝑞 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1𝑎 ) ) ) = ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) )
38 37 mpteq2dv ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠𝑞 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1𝑎 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ) )
39 28 38 oveq12d ( ( 𝑎 = ( 𝑛 Mat 𝑟 ) ∧ 𝑞 = ( Poly1𝑎 ) ) → ( 𝑞 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠𝑞 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1𝑎 ) ) ) ) ) = ( ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ) ) )
40 24 39 csbied ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( Poly1𝑎 ) / 𝑞 ( 𝑞 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠𝑞 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1𝑎 ) ) ) ) ) = ( ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ) ) )
41 23 40 csbie ( 𝑛 Mat 𝑟 ) / 𝑎 ( Poly1𝑎 ) / 𝑞 ( 𝑞 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠𝑞 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1𝑎 ) ) ) ) ) = ( ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ) )
42 oveq12 ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = ( 𝑁 Mat 𝑅 ) )
43 42 fveq2d ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) = ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) ) )
44 7 fveq2i ( Poly1𝐴 ) = ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) )
45 8 44 eqtri 𝑄 = ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) )
46 43 45 eqtr4di ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) = 𝑄 )
47 43 fveq2d ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) = ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) ) ) )
48 45 fveq2i ( ·𝑠𝑄 ) = ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) ) )
49 4 48 eqtri = ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) ) )
50 47 49 eqtr4di ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) = )
51 eqidd ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( 𝑚 decompPMat 𝑘 ) = ( 𝑚 decompPMat 𝑘 ) )
52 43 fveq2d ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) = ( mulGrp ‘ ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) ) ) )
53 52 fveq2d ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) ) ) ) )
54 45 fveq2i ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) ) )
55 54 fveq2i ( .g ‘ ( mulGrp ‘ 𝑄 ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) ) ) )
56 5 55 eqtri = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑁 Mat 𝑅 ) ) ) )
57 53 56 eqtr4di ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) = )
58 eqidd ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → 𝑘 = 𝑘 )
59 42 fveq2d ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) = ( var1 ‘ ( 𝑁 Mat 𝑅 ) ) )
60 7 fveq2i ( var1𝐴 ) = ( var1 ‘ ( 𝑁 Mat 𝑅 ) )
61 6 60 eqtri 𝑋 = ( var1 ‘ ( 𝑁 Mat 𝑅 ) )
62 59 61 eqtr4di ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) = 𝑋 )
63 57 58 62 oveq123d ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) = ( 𝑘 𝑋 ) )
64 50 51 63 oveq123d ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) = ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) )
65 64 mpteq2dv ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) ) )
66 46 65 oveq12d ( ( 𝑛 = 𝑁𝑟 = 𝑅 ) → ( ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) ) ) )
67 66 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) ∧ ( 𝑛 = 𝑁𝑟 = 𝑅 ) ) → ( ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠 ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ( 𝑘 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ( var1 ‘ ( 𝑛 Mat 𝑟 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) ) ) )
68 41 67 eqtrid ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) ∧ ( 𝑛 = 𝑁𝑟 = 𝑅 ) ) → ( 𝑛 Mat 𝑟 ) / 𝑎 ( Poly1𝑎 ) / 𝑞 ( 𝑞 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠𝑞 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1𝑎 ) ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) ) ) )
69 22 68 mpteq12dv ( ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) ∧ ( 𝑛 = 𝑁𝑟 = 𝑅 ) ) → ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1𝑟 ) ) ) ↦ ( 𝑛 Mat 𝑟 ) / 𝑎 ( Poly1𝑎 ) / 𝑞 ( 𝑞 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠𝑞 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1𝑎 ) ) ) ) ) ) = ( 𝑚𝐵 ↦ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) ) ) ) )
70 simpl ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝑁 ∈ Fin )
71 elex ( 𝑅𝑉𝑅 ∈ V )
72 71 adantl ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝑅 ∈ V )
73 3 fvexi 𝐵 ∈ V
74 73 mptex ( 𝑚𝐵 ↦ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) ) ) ) ∈ V
75 74 a1i ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑚𝐵 ↦ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) ) ) ) ∈ V )
76 11 69 70 72 75 ovmpod ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑁 pMatToMatPoly 𝑅 ) = ( 𝑚𝐵 ↦ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) ) ) ) )
77 9 76 eqtrid ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝑇 = ( 𝑚𝐵 ↦ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( 𝑘 𝑋 ) ) ) ) ) )