mply1topmatcllem

	Ref	Expression
Hypotheses	mply1topmat.a	$⊢ A = N Mat R$
	mply1topmat.q	$⊢ Q = {Poly}_{1} (A)$
	mply1topmat.l	$⊢ L = {Base}_{Q}$
	mply1topmat.p	$⊢ P = {Poly}_{1} (R)$
	mply1topmat.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	mply1topmat.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
	mply1topmat.y	$⊢ Y = {var}_{1} (R)$
Assertion	mply1topmatcllem	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to {finSupp}_{0_{P}} ((k \in ℕ_{0} ⟼ (I {coe}_{1} (O) (k) J) \underset{˙}{\cdot} (k E Y)))$

Proof

Step	Hyp	Ref	Expression
1		mply1topmat.a	$⊢ A = N Mat R$
2		mply1topmat.q	$⊢ Q = {Poly}_{1} (A)$
3		mply1topmat.l	$⊢ L = {Base}_{Q}$
4		mply1topmat.p	$⊢ P = {Poly}_{1} (R)$
5		mply1topmat.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		mply1topmat.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
7		mply1topmat.y	$⊢ Y = {var}_{1} (R)$
8		nn0ex	$⊢ ℕ_{0} \in V$
9	8	a1i	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to ℕ_{0} \in V$
10	4	ply1lmod	$⊢ R \in Ring \to P \in LMod$
11	10	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to P \in LMod$
12	11	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to P \in LMod$
13		simp12	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to R \in Ring$
14	4	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
15	13 14	syl	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to R = Scalar (P)$
16		eqid	$⊢ {Base}_{P} = {Base}_{P}$
17		ovexd	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land k \in ℕ_{0}) \to I {coe}_{1} (O) (k) J \in V$
18	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
19		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
20	19	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
21	18 20	syl	$⊢ R \in Ring \to {mulGrp}_{P} \in Mnd$
22	21	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to {mulGrp}_{P} \in Mnd$
23	22	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to {mulGrp}_{P} \in Mnd$
24	23	adantr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land k \in ℕ_{0}) \to {mulGrp}_{P} \in Mnd$
25		simpr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
26	7 4 16	vr1cl	$⊢ R \in Ring \to Y \in {Base}_{P}$
27	26	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to Y \in {Base}_{P}$
28	27	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to Y \in {Base}_{P}$
29	28	adantr	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land k \in ℕ_{0}) \to Y \in {Base}_{P}$
30	19 16	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
31	30 6	mulgnn0cl	$⊢ ({mulGrp}_{P} \in Mnd \land k \in ℕ_{0} \land Y \in {Base}_{P}) \to k E Y \in {Base}_{P}$
32	24 25 29 31	syl3anc	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \land k \in ℕ_{0}) \to k E Y \in {Base}_{P}$
33		eqid	$⊢ 0_{P} = 0_{P}$
34		eqid	$⊢ 0_{R} = 0_{R}$
35	1 2 3	mptcoe1matfsupp	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to {finSupp}_{0_{R}} ((k \in ℕ_{0} ⟼ I {coe}_{1} (O) (k) J))$
36	9 12 15 16 17 32 33 34 5 35	mptscmfsupp0	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land I \in N \land J \in N) \to {finSupp}_{0_{P}} ((k \in ℕ_{0} ⟼ (I {coe}_{1} (O) (k) J) \underset{˙}{\cdot} (k E Y)))$

Metamath Proof Explorer

Theorem mply1topmatcllem

Proof