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		eqid	⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
46		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
47	45 46	mgpbas	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( mulGrp ‘ 𝑄 ) )
48	9	ply1ring	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
49	36 48	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
50	45	ringmgp	⊢ ( 𝑄 ∈ Ring → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
51	49 50	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
52	51	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
53		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
54	6 9 46	vr1cl	⊢ ( 𝐴 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑄 ) )
55	36 54	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑋 ∈ ( Base ‘ 𝑄 ) )
56	55	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑄 ) )
57	47 5 52 53 56	mulgnn0cld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) )
58		eqid	⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
59		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑄 ) ) = ( 0g ‘ ( Scalar ‘ 𝑄 ) )
60		eqid	⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
61	46 58 4 59 60	lmod0vs	⊢ ( ( 𝑄 ∈ LMod ∧ ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
62	44 57 61	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ ( Scalar ‘ 𝑄 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
63	41 62	eqtrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 0g ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑄 ) )
64	63	ifeq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( ( 0g ‘ 𝐴 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) )
65	35 64	eqtrid	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 𝐿 , 𝑀 , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) )
66	34 65	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 𝐿 , 𝑀 , ( 0g ‘ 𝐴 ) ) ∗ ( 𝑘 ↑ 𝑋 ) ) = if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) )
67	30 66	eqtrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) )
68	67	mpteq2dva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) ) )
69	68	oveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) ) ) )
70		ringmnd	⊢ ( 𝑄 ∈ Ring → 𝑄 ∈ Mnd )
71	49 70	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Mnd )
72	71	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → 𝑄 ∈ Mnd )
73		nn0ex	⊢ ℕ0 ∈ V
74	73	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ℕ0 ∈ V )
75		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → 𝐿 ∈ ℕ0 )
76		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) )
77	38	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝐴 ) = ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
78	8 77	eqtrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
79	78	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝐾 ↔ 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) )
80	79	biimpcd	⊢ ( 𝑀 ∈ 𝐾 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) )
81	80	adantr	⊢ ( ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ) )
82	81	impcom	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
83	82	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) )
84		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑄 ) ) = ( Base ‘ ( Scalar ‘ 𝑄 ) )
85	46 58 4 84	lmodvscl	⊢ ( ( 𝑄 ∈ LMod ∧ 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑄 ) ) ∧ ( 𝑘 ↑ 𝑋 ) ∈ ( Base ‘ 𝑄 ) ) → ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑄 ) )
86	44 83 57 85	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑄 ) )
87	86	ralrimiva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑄 ) )
88	60 72 74 75 76 87	gsummpt1n0	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) )
89	15 88	sylanl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝐿 , ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) , ( 0g ‘ 𝑄 ) ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) )
90	69 89	eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) )
91		csbov2g	⊢ ( 𝐿 ∈ ℕ0 → ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑀 ∗ ⦋ 𝐿 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) ) )
92		csbov1g	⊢ ( 𝐿 ∈ ℕ0 → ⦋ 𝐿 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) = ( ⦋ 𝐿 / 𝑘 ⦌ 𝑘 ↑ 𝑋 ) )
93		csbvarg	⊢ ( 𝐿 ∈ ℕ0 → ⦋ 𝐿 / 𝑘 ⦌ 𝑘 = 𝐿 )
94	93	oveq1d	⊢ ( 𝐿 ∈ ℕ0 → ( ⦋ 𝐿 / 𝑘 ⦌ 𝑘 ↑ 𝑋 ) = ( 𝐿 ↑ 𝑋 ) )
95	92 94	eqtrd	⊢ ( 𝐿 ∈ ℕ0 → ⦋ 𝐿 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) = ( 𝐿 ↑ 𝑋 ) )
96	95	oveq2d	⊢ ( 𝐿 ∈ ℕ0 → ( 𝑀 ∗ ⦋ 𝐿 / 𝑘 ⦌ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑀 ∗ ( 𝐿 ↑ 𝑋 ) ) )
97	91 96	eqtrd	⊢ ( 𝐿 ∈ ℕ0 → ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑀 ∗ ( 𝐿 ↑ 𝑋 ) ) )
98	97	ad2antll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ⦋ 𝐿 / 𝑘 ⦌ ( 𝑀 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝑀 ∗ ( 𝐿 ↑ 𝑋 ) ) )
99	21 90 98	3eqtrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐼 ‘ ( ( 𝐿 𝐸 𝑌 ) · ( 𝑇 ‘ 𝑀 ) ) ) = ( 𝑀 ∗ ( 𝐿 ↑ 𝑋 ) ) )