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 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ) |