mp2pm2mplem2

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

	Ref	Expression
Hypotheses	mp2pm2mp.a	$⊢ A = N Mat R$
	mp2pm2mp.q	$⊢ Q = {Poly}_{1} (A)$
	mp2pm2mp.l	$⊢ L = {Base}_{Q}$
	mp2pm2mp.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	mp2pm2mp.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
	mp2pm2mp.y	$⊢ Y = {var}_{1} (R)$
	mp2pm2mp.i	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))))$
	mp2pm2mplem2.p	$⊢ P = {Poly}_{1} (R)$
	mp2pm2mplem2.c	$⊢ C = N Mat P$
	mp2pm2mplem2.b	$⊢ B = {Base}_{C}$
Assertion	mp2pm2mplem2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) \in B$

Proof

Step	Hyp	Ref	Expression
1		mp2pm2mp.a	$⊢ A = N Mat R$
2		mp2pm2mp.q	$⊢ Q = {Poly}_{1} (A)$
3		mp2pm2mp.l	$⊢ L = {Base}_{Q}$
4		mp2pm2mp.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		mp2pm2mp.e	$⊢ E = \cdot_{{mulGrp}_{P}}$
6		mp2pm2mp.y	$⊢ Y = {var}_{1} (R)$
7		mp2pm2mp.i	$⊢ I = (p \in L ⟼ (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (p) (k) j) \underset{˙}{\cdot} (k E Y))))$
8		mp2pm2mplem2.p	$⊢ P = {Poly}_{1} (R)$
9		mp2pm2mplem2.c	$⊢ C = N Mat P$
10		mp2pm2mplem2.b	$⊢ B = {Base}_{C}$
11		eqid	$⊢ {Base}_{P} = {Base}_{P}$
12		simp1	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to N \in Fin$
13	8	ply1ring	$⊢ R \in Ring \to P \in Ring$
14	13	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to P \in Ring$
15		eqid	$⊢ 0_{P} = 0_{P}$
16		ringcmn	$⊢ P \in Ring \to P \in CMnd$
17	13 16	syl	$⊢ R \in Ring \to P \in CMnd$
18	17	3ad2ant2	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to P \in CMnd$
19	18	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to P \in CMnd$
20		nn0ex	$⊢ ℕ_{0} \in V$
21	20	a1i	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to ℕ_{0} \in V$
22		simpl12	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to R \in Ring$
23		eqid	$⊢ {Base}_{R} = {Base}_{R}$
24		eqid	$⊢ {Base}_{A} = {Base}_{A}$
25		simpl2	$⊢ (((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 \in N$
26		simpl3	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to j \in N$
27		simp13	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to O \in L$
28		eqid	$⊢ {coe}_{1} (O) = {coe}_{1} (O)$
29	28 3 2 24	coe1fvalcl	$⊢ (O \in L \land k \in ℕ_{0}) \to {coe}_{1} (O) (k) \in {Base}_{A}$
30	27 29	sylan	$⊢ (((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \land k \in ℕ_{0}) \to {coe}_{1} (O) (k) \in {Base}_{A}$
31	1 23 24 25 26 30	matecld	$⊢ (((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 {Base}_{R}$
32		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}$
33		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
34	23 8 6 4 33 5 11	ply1tmcl	$⊢ (R \in Ring \land i {coe}_{1} (O) (k) j \in {Base}_{R} \land k \in ℕ_{0}) \to (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) \in {Base}_{P}$
35	22 31 32 34	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 (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y) \in {Base}_{P}$
36	35	fmpttd	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to (k \in ℕ_{0} ⟼ (i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) : ℕ_{0} ⟶ {Base}_{P}$
37	1 2 3 8 4 5 6	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)))$
38	11 15 19 21 36 37	gsumcl	$⊢ ((N \in Fin \land R \in Ring \land O \in L) \land i \in N \land j \in N) \to \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y)) \in {Base}_{P}$
39	9 11 10 12 14 38	matbas2d	$⊢ (N \in Fin \land R \in Ring \land O \in L) \to (i \in N, j \in N ⟼ \underset{k \in ℕ_{0}}{\sum_{P}} ((i {coe}_{1} (O) (k) j) \underset{˙}{\cdot} (k E Y))) \in B$

Metamath Proof Explorer

Theorem mp2pm2mplem2

Proof