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 syl5eq ⊢ ( ( ( 𝑁 ∈ 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 syl5eq ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑇 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )