Theorem mp2pm2mplem2

Description: Lemma 2 for mp2pm2mp . (Contributed by AV, 10-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 ‘ 𝑅 )
	mp2pm2mplem2.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	mp2pm2mplem2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	mp2pm2mplem2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ∈ 𝐵 )

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		mp2pm2mplem2.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
10		mp2pm2mplem2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
11		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
12		simp1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑁 ∈ Fin )
13	8	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
14	13	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑃 ∈ Ring )
15		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
16		ringcmn	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
17	13 16	syl	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ CMnd )
18	17	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑃 ∈ CMnd )
19	18	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ CMnd )
20		nn0ex	⊢ ℕ0 ∈ V
21	20	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ℕ0 ∈ V )
22		simpl12	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
23		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
24		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
25		simpl2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑖 ∈ 𝑁 )
26		simpl3	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑗 ∈ 𝑁 )
27		simp13	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑂 ∈ 𝐿 )
28		eqid	⊢ ( coe1 ‘ 𝑂 ) = ( coe1 ‘ 𝑂 )
29	28 3 2 24	coe1fvalcl	⊢ ( ( 𝑂 ∈ 𝐿 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
30	27 29	sylan	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝐴 ) )
31	1 23 24 25 26 30	matecld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
32		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
33		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
34	23 8 6 4 33 5 11	ply1tmcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ∈ ( Base ‘ 𝑃 ) )
35	22 31 32 34	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ∈ ( Base ‘ 𝑃 ) )
36	35	fmpttd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) : ℕ0 ⟶ ( Base ‘ 𝑃 ) )
37	1 2 3 8 4 5 6	mply1topmatcllem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) finSupp ( 0g ‘ 𝑃 ) )
38	11 15 19 21 36 37	gsumcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
39	9 11 10 12 14 38	matbas2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑖 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝑗 ) · ( 𝑘 𝐸 𝑌 ) ) ) ) ) ∈ 𝐵 )