Theorem monmat2matmon

Description: The transformation of a polynomial matrix having scaled monomials with the same power as entries into a scaled monomial as a polynomial over matrices. (Contributed by AV, 11-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	monmat2matmon	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ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		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
16		simpll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → 𝑁 ∈ Fin )
17		simplr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → 𝑅 ∈ Ring )
18	7 8 14 1 2 3 13 11 12	mat2pmatscmxcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) ∈ 𝐵 )
19	1 2 3 4 5 6 7 9 10	pm2mpfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) ∈ 𝐵 ) → ( 𝐼 ‘ ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
20	16 17 18 19	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐼 ‘ ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
21	15 20	sylanl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐼 ‘ ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
22		simpll	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) )
23		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) )
24	23	anim1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) )
25		df-3an	⊢ ( ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ↔ ( ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) )
26	24 25	sylibr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) )
27		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
28	1 2 7 8 27 11 12 13 14	monmatcollpw	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) ) → ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) = if ( 𝑘 = 𝐿 , 𝑀 , ( 0g ‘ 𝐴 ) ) )
29	22 26 28	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) = if ( 𝑘 = 𝐿 , 𝑀 , ( 0g ‘ 𝐴 ) ) )
30	29	oveq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( if ( 𝑘 = 𝐿 , 𝑀 , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) )
31	15	a1i	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑅 ∈ CRing → 𝑅 ∈ Ring ) )
32	31	anim2d	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ) )
33	32	anim1d	⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ) )
34	33	imdistanri	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) )
35		ovif	⊢ ( if ( 𝑘 = 𝐿 , 𝑀 , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( ( 0g ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) )
36	7	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
37	9	ply1sca	⊢ ( 𝐴 ∈ Ring → 𝐴 = ( Scalar ‘ 𝑄 ) )
38	36 37	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
39	38	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
40	39	fveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 0g ‘ 𝐴 ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) ) )
41	40	oveq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) )
42	9	ply1lmod	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ LMod )
43	36 42	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ LMod )
44	43	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑄 ∈ LMod )
45	9	ply1ring	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
46	36 45	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
47		eqid	⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
48	47	ringmgp	⊢ ( 𝑄 ∈ Ring → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
49	46 48	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
50	49	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
51		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
52		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
53	6 9 52	vr1cl	⊢ ( 𝐴 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑄 ) )
54	36 53	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑋 ∈ ( Base ‘ 𝑄 ) )
55	54	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑄 ) )
56	47 52	mgpbas	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( mulGrp ‘ 𝑄 ) )
57	56 5	mulgnn0cl	⊢ ( ( ( mulGrp ‘ 𝑄 ) ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑋 ∈ ( Base ‘ 𝑄 ) ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) )
58	50 51 55 57	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) )
59		eqid	⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
60		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑄 ) ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) )
61		eqid	⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
62	52 59 4 60 61	lmod0vs	⊢ ( ( 𝑄 ∈ LMod ∧ ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
63	44 58 62	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
64	41 63	eqtrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
65	64	ifeq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( ( 0g ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) )
66	35 65	eqtrid	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 𝐿 , 𝑀 , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) )
67	34 66	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 𝐿 , 𝑀 , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) )
68	30 67	eqtrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) )
69	68	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) ) )
70	69	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) ) ) )
71		ringmnd	⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ Mnd )
72	46 71	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Mnd )
73	72	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → 𝑄 ∈ Mnd )
74		nn0ex	⊢ ℕ0 ∈ V
75	74	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ℕ0 ∈ V )
76		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → 𝐿 ∈ ℕ0 )
77		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) )
78	38	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝐴 ) = ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
79	8 78	eqtrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
80	79	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝐾 ↔ 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) )
81	80	biimpcd	⊢ ( 𝑀 ∈ 𝐾 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) )
82	81	adantr	⊢ ( ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) )
83	82	impcom	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
84	83	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
85		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑄 ) ) = ( Base ‘ ( Scalar ‘ 𝑄 ) )
86	52 59 4 85	lmodvscl	⊢ ( ( 𝑄 ∈ LMod ∧ 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ∧ ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) ) → ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑄 ) )
87	44 84 58 86	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑄 ) )
88	87	ralrimiva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑄 ) )
89	61 73 75 76 77 88	gsummpt1n0	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) )
90	15 89	sylanl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) )
91	70 90	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) )
92		csbov2g	⊢ ( 𝐿 ∈ ℕ0 → ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑀 ∗ ⦋ 𝐿 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) ) )
93		csbov1g	⊢ ( 𝐿 ∈ ℕ0 → ⦋ 𝐿 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) = ( ⦋ 𝐿 / 𝑘 ⦌ 𝑘 ↑ 𝑋 ) )
94		csbvarg	⊢ ( 𝐿 ∈ ℕ0 → ⦋ 𝐿 / 𝑘 ⦌ 𝑘 = 𝐿 )
95	94	oveq1d	⊢ ( 𝐿 ∈ ℕ0 → ( ⦋ 𝐿 / 𝑘 ⦌ 𝑘 ↑ 𝑋 ) = ( 𝐿 ↑ 𝑋 ) )
96	93 95	eqtrd	⊢ ( 𝐿 ∈ ℕ0 → ⦋ 𝐿 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) = ( 𝐿 ↑ 𝑋 ) )
97	96	oveq2d	⊢ ( 𝐿 ∈ ℕ0 → ( 𝑀 ∗ ⦋ 𝐿 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑀 ∗ ( 𝐿 ↑ 𝑋 ) ) )
98	92 97	eqtrd	⊢ ( 𝐿 ∈ ℕ0 → ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑀 ∗ ( 𝐿 ↑ 𝑋 ) ) )
99	98	ad2antll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑀 ∗ ( 𝐿 ↑ 𝑋 ) ) )
100	21 91 99	3eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐼 ‘ ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) ) = ( 𝑀 ∗ ( 𝐿 ↑ 𝑋 ) ) )