Theorem pm2mp

Description: The transformation of a sum of matrices having scaled monomials with the same power as entries into a sum of scaled monomials as a polynomial over matrices. (Contributed by AV, 12-Nov-2019) (Revised by AV, 7-Dec-2019)

	Ref	Expression
Hypotheses	monmat2matmon.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	monmat2matmon.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	monmat2matmon.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	monmat2matmon.m1	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
	monmat2matmon.e1	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
	monmat2matmon.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
	monmat2matmon.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	monmat2matmon.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
	monmat2matmon.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	monmat2matmon.i	⊢ 𝐼 = ( 𝑁 pMatToMatPoly 𝑅 )
	monmat2matmon.e2	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	monmat2matmon.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
	monmat2matmon.m2	⊢ · = ( ·𝑠 ‘ 𝐶 )
	monmat2matmon.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
Assertion	pm2mp	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝐼 ‘ ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		monmat2matmon.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		monmat2matmon.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		monmat2matmon.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		monmat2matmon.m1	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5		monmat2matmon.e1	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6		monmat2matmon.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
7		monmat2matmon.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8		monmat2matmon.k	⊢ 𝐾 = ( Base ‘ 𝐴 )
9		monmat2matmon.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
10		monmat2matmon.i	⊢ 𝐼 = ( 𝑁 pMatToMatPoly 𝑅 )
11		monmat2matmon.e2	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
12		monmat2matmon.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
13		monmat2matmon.m2	⊢ · = ( ·𝑠 ‘ 𝐶 )
14		monmat2matmon.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
15		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
16		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
17	16	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
18	1 2	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
19		ringcmn	⊢ ( 𝐶 ∈ Ring → 𝐶 ∈ CMnd )
20	17 18 19	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ CMnd )
21	20	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → 𝐶 ∈ CMnd )
22	7	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
23	16 22	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
24	9	ply1ring	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
25		ringmnd	⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ Mnd )
26	23 24 25	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑄 ∈ Mnd )
27	26	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → 𝑄 ∈ Mnd )
28		nn0ex	⊢ ℕ0 ∈ V
29	28	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ℕ0 ∈ V )
30		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
31	1 2 3 4 5 6 7 9 30 10	pm2mpghm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 ∈ ( 𝐶 GrpHom 𝑄 ) )
32	16 31	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐼 ∈ ( 𝐶 GrpHom 𝑄 ) )
33	32	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → 𝐼 ∈ ( 𝐶 GrpHom 𝑄 ) )
34		ghmmhm	⊢ ( 𝐼 ∈ ( 𝐶 GrpHom 𝑄 ) → 𝐼 ∈ ( 𝐶 MndHom 𝑄 ) )
35	33 34	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → 𝐼 ∈ ( 𝐶 MndHom 𝑄 ) )
36	17	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
37	36	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
38		elmapi	⊢ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) → 𝑀 : ℕ0 ⟶ 𝐾 )
39	38	adantr	⊢ ( ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) → 𝑀 : ℕ0 ⟶ 𝐾 )
40	39	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → 𝑀 : ℕ0 ⟶ 𝐾 )
41	40	ffvelcdmda	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 ‘ 𝑛 ) ∈ 𝐾 )
42		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
43	7 8 14 1 2 3 13 11 12	mat2pmatscmxcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑀 ‘ 𝑛 ) ∈ 𝐾 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ∈ 𝐵 )
44	37 41 42 43	syl12anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ∈ 𝐵 )
45		fvexd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 0g ‘ 𝐶 ) ∈ V )
46		ovexd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ∈ V )
47		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) → 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) )
48		fvex	⊢ ( 0g ‘ 𝐴 ) ∈ V
49		fsuppmapnn0ub	⊢ ( ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ ( 0g ‘ 𝐴 ) ∈ V ) → ( 𝑀 finSupp ( 0g ‘ 𝐴 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) )
50	47 48 49	sylancl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) → ( 𝑀 finSupp ( 0g ‘ 𝐴 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) ) )
51		csbov12g	⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝑛 𝐸 𝑌 ) · ⦋ 𝑥 / 𝑛 ⦌ ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) )
52		csbov1g	⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑛 𝐸 𝑌 ) = ( ⦋ 𝑥 / 𝑛 ⦌ 𝑛 𝐸 𝑌 ) )
53		csbvarg	⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ 𝑛 = 𝑥 )
54	53	oveq1d	⊢ ( 𝑥 ∈ ℕ0 → ( ⦋ 𝑥 / 𝑛 ⦌ 𝑛 𝐸 𝑌 ) = ( 𝑥 𝐸 𝑌 ) )
55	52 54	eqtrd	⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑛 𝐸 𝑌 ) = ( 𝑥 𝐸 𝑌 ) )
56		csbfv2g	⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) = ( 𝑇 ‘ ⦋ 𝑥 / 𝑛 ⦌ ( 𝑀 ‘ 𝑛 ) ) )
57		csbfv2g	⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑀 ‘ 𝑛 ) = ( 𝑀 ‘ ⦋ 𝑥 / 𝑛 ⦌ 𝑛 ) )
58	53	fveq2d	⊢ ( 𝑥 ∈ ℕ0 → ( 𝑀 ‘ ⦋ 𝑥 / 𝑛 ⦌ 𝑛 ) = ( 𝑀 ‘ 𝑥 ) )
59	57 58	eqtrd	⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑀 ‘ 𝑛 ) = ( 𝑀 ‘ 𝑥 ) )
60	59	fveq2d	⊢ ( 𝑥 ∈ ℕ0 → ( 𝑇 ‘ ⦋ 𝑥 / 𝑛 ⦌ ( 𝑀 ‘ 𝑛 ) ) = ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) )
61	56 60	eqtrd	⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) = ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) )
62	55 61	oveq12d	⊢ ( 𝑥 ∈ ℕ0 → ( ⦋ 𝑥 / 𝑛 ⦌ ( 𝑛 𝐸 𝑌 ) · ⦋ 𝑥 / 𝑛 ⦌ ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
63	51 62	eqtrd	⊢ ( 𝑥 ∈ ℕ0 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
64	63	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
65	64	adantr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
66		fveq2	⊢ ( ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) = ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) )
67	66	oveq2d	⊢ ( ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) ) )
68	14 7 8 1 2 3	mat2pmatghm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
69	16 68	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
70	69	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
71		ghmmhm	⊢ ( 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) → 𝑇 ∈ ( 𝐴 MndHom 𝐶 ) )
72		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
73	72 15	mhm0	⊢ ( 𝑇 ∈ ( 𝐴 MndHom 𝐶 ) → ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) = ( 0g ‘ 𝐶 ) )
74	70 71 73	3syl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) = ( 0g ‘ 𝐶 ) )
75	74	oveq2d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) ) = ( ( 𝑥 𝐸 𝑌 ) · ( 0g ‘ 𝐶 ) ) )
76	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
77	16 76	syl	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
78	2	matlmod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝐶 ∈ LMod )
79	77 78	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ LMod )
80	79	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝐶 ∈ LMod )
81		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
82		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
83	81 82	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
84	77	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ Ring )
85	81	ringmgp	⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
86	84 85	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
87	86	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
88		simpr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
89	16	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
90	12 1 82	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ ( Base ‘ 𝑃 ) )
91	89 90	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ ( Base ‘ 𝑃 ) )
92	91	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑌 ∈ ( Base ‘ 𝑃 ) )
93	83 11 87 88 92	mulgnn0cld	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 𝐸 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
94	1	ply1crng	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
95	2	matsca2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝐶 ) )
96	94 95	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝐶 ) )
97	96	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Scalar ‘ 𝐶 ) = 𝑃 )
98	97	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( Scalar ‘ 𝐶 ) = 𝑃 )
99	98	fveq2d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ 𝑃 ) )
100	93 99	eleqtrrd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 𝐸 𝑌 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
101		eqid	⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
102		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
103	101 13 102 15	lmodvs0	⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑥 𝐸 𝑌 ) ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ) → ( ( 𝑥 𝐸 𝑌 ) · ( 0g ‘ 𝐶 ) ) = ( 0g ‘ 𝐶 ) )
104	80 100 103	syl2anc	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 𝐸 𝑌 ) · ( 0g ‘ 𝐶 ) ) = ( 0g ‘ 𝐶 ) )
105	75 104	eqtrd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 0g ‘ 𝐴 ) ) ) = ( 0g ‘ 𝐶 ) )
106	67 105	sylan9eqr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( ( 𝑥 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑥 ) ) ) = ( 0g ‘ 𝐶 ) )
107	65 106	eqtrd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) )
108	107	ex	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) )
109	108	imim2d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑦 < 𝑥 → ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ( 𝑦 < 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
110	109	ralimdva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
111	110	reximdva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) → ( ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ( 𝑀 ‘ 𝑥 ) = ( 0g ‘ 𝐴 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
112	50 111	syld	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ) → ( 𝑀 finSupp ( 0g ‘ 𝐴 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) ) )
113	112	impr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑦 < 𝑥 → ⦋ 𝑥 / 𝑛 ⦌ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝐶 ) ) )
114	45 46 113	mptnn0fsupp	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) finSupp ( 0g ‘ 𝐶 ) )
115	3 15 21 27 29 35 44 114	gsummptmhm	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝐼 ‘ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) ) = ( 𝐼 ‘ ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) ) )
116		simpll	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
117	1 2 3 4 5 6 7 8 9 10 11 12 13 14	monmat2matmon	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( ( 𝑀 ‘ 𝑛 ) ∈ 𝐾 ∧ 𝑛 ∈ ℕ0 ) ) → ( 𝐼 ‘ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) = ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) )
118	116 41 42 117	syl12anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐼 ‘ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) = ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) )
119	118	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝐼 ‘ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) )
120	119	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝐼 ‘ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )
121	115 120	eqtr3d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝑀 finSupp ( 0g ‘ 𝐴 ) ) ) → ( 𝐼 ‘ ( 𝐶 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 𝑌 ) · ( 𝑇 ‘ ( 𝑀 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑄 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑀 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑋 ) ) ) ) )