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