Theorem mp2pm2mplem5

Description: Lemma 5 for mp2pm2mp . (Contributed by AV, 12-Oct-2019) (Revised by AV, 5-Dec-2019)

	Ref	Expression
Hypotheses	mp2pm2mp.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mp2pm2mp.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	mp2pm2mp.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
	mp2pm2mp.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
	mp2pm2mp.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	mp2pm2mp.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
	mp2pm2mp.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
	mp2pm2mplem2.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mp2pm2mplem5.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
	mp2pm2mplem5.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
	mp2pm2mplem5.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
Assertion	mp2pm2mplem5	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		mp2pm2mp.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mp2pm2mp.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
3		mp2pm2mp.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
4		mp2pm2mp.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
5		mp2pm2mp.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6		mp2pm2mp.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
7		mp2pm2mp.i	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) )
8		mp2pm2mplem2.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
9		mp2pm2mplem5.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
10		mp2pm2mplem5.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
11		mp2pm2mplem5.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
12		nn0ex	⊢ ℕ0 ∈ V
13	12	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ℕ0 ∈ V )
14	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
15	2	ply1lmod	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ LMod )
16	14 15	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ LMod )
17	16	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑄 ∈ LMod )
18	14	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝐴 ∈ Ring )
19	2	ply1sca	⊢ ( 𝐴 ∈ Ring → 𝐴 = ( Scalar ‘ 𝑄 ) )
20	18 19	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝐴 = ( Scalar ‘ 𝑄 ) )
21		simpl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
22		eqid	⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 )
23		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ ( 𝑁 Mat 𝑃 ) )
24	1 2 3 8 4 5 6 7 22 23	mply1topmatcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝐼 ‘ 𝑂 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
25	24	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐼 ‘ 𝑂 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
26		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
27		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
28	8 22 23 1 27	decpmatcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ‘ 𝑂 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
29	21 25 26 28	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
30		eqid	⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
31	2 11 30 10 3	ply1moncl	⊢ ( ( 𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐿 )
32	18 31	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐿 )
33		eqid	⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
34		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
35		fveq2	⊢ ( 𝑘 = 𝑙 → ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑝 ) ‘ 𝑙 ) )
36	35	oveqd	⊢ ( 𝑘 = 𝑙 → ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) = ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑙 ) 𝑗 ) )
37		oveq1	⊢ ( 𝑘 = 𝑙 → ( 𝑘 𝐸 𝑌 ) = ( 𝑙 𝐸 𝑌 ) )
38	36 37	oveq12d	⊢ ( 𝑘 = 𝑙 → ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) = ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑙 ) 𝑗 ) · ( 𝑙 𝐸 𝑌 ) ) )
39	38	cbvmptv	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑙 ) 𝑗 ) · ( 𝑙 𝐸 𝑌 ) ) )
40	39	oveq2i	⊢ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) = ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑙 ) 𝑗 ) · ( 𝑙 𝐸 𝑌 ) ) ) )
41	40	a1i	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) = ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑙 ) 𝑗 ) · ( 𝑙 𝐸 𝑌 ) ) ) ) )
42	41	mpoeq3ia	⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑙 ) 𝑗 ) · ( 𝑙 𝐸 𝑌 ) ) ) ) )
43	42	mpteq2i	⊢ ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ) = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑙 ) 𝑗 ) · ( 𝑙 𝐸 𝑌 ) ) ) ) ) )
44	7 43	eqtri	⊢ 𝐼 = ( 𝑝 ∈ 𝐿 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑝 ) ‘ 𝑙 ) 𝑗 ) · ( 𝑙 𝐸 𝑌 ) ) ) ) ) )
45	1 2 3 4 5 6 44 8	mp2pm2mplem4	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑘 ) = ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) )
46	45	mpteq2dva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑘 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ) )
47	2 3 34	mptcoe1fsupp	⊢ ( ( 𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
48	14 47	stoic3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
49	46 48	eqbrtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑘 ) ) finSupp ( 0g ‘ 𝐴 ) )
50	13 17 20 3 29 32 33 34 9 49	mptscmfsupp0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝐼 ‘ 𝑂 ) decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑄 ) )