Theorem mply1topmatcllem

Description: Lemma for mply1topmatcl . (Contributed by AV, 6-Oct-2019)

	Ref	Expression
Hypotheses	mply1topmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mply1topmat.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	mply1topmat.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
	mply1topmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mply1topmat.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
	mply1topmat.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	mply1topmat.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
Assertion	mply1topmatcllem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) · ( 𝑘 𝐸 𝑌 ) ) ) finSupp ( 0g ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		mply1topmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mply1topmat.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
3		mply1topmat.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
4		mply1topmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		mply1topmat.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
6		mply1topmat.e	⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
7		mply1topmat.y	⊢ 𝑌 = ( var1 ‘ 𝑅 )
8		nn0ex	⊢ ℕ0 ∈ V
9	8	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ℕ0 ∈ V )
10	4	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
11	10	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑃 ∈ LMod )
12	11	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → 𝑃 ∈ LMod )
13		simp12	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → 𝑅 ∈ Ring )
14	4	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
15	13 14	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
16		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
17		ovexd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) ∈ V )
18	4	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
19		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
20	19	ringmgp	⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
21	18 20	syl	⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
22	21	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
23	22	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
24	23	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
25		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
26	7 4 16	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ ( Base ‘ 𝑃 ) )
27	26	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) → 𝑌 ∈ ( Base ‘ 𝑃 ) )
28	27	3ad2ant1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → 𝑌 ∈ ( Base ‘ 𝑃 ) )
29	28	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑌 ∈ ( Base ‘ 𝑃 ) )
30	19 16	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
31	30 6	mulgnn0cl	⊢ ( ( ( mulGrp ‘ 𝑃 ) ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑘 𝐸 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
32	24 25 29 31	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 𝐸 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
33		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
34		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
35	1 2 3	mptcoe1matfsupp	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) ) finSupp ( 0g ‘ 𝑅 ) )
36	9 12 15 16 17 32 33 34 5 35	mptscmfsupp0	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐼 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) 𝐽 ) · ( 𝑘 𝐸 𝑌 ) ) ) finSupp ( 0g ‘ 𝑃 ) )