cpmadugsumlemC

	Ref	Expression
Hypotheses	cpmadugsum.a	$⊢ A = N Mat R$
	cpmadugsum.b	$⊢ B = {Base}_{A}$
	cpmadugsum.p	$⊢ P = {Poly}_{1} (R)$
	cpmadugsum.y	$⊢ Y = N Mat P$
	cpmadugsum.t	$⊢ T = N matToPolyMat R$
	cpmadugsum.x	$⊢ X = {var}_{1} (R)$
	cpmadugsum.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	cpmadugsum.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	cpmadugsum.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	cpmadugsum.1	$⊢ \underset{˙}{1} = 1_{Y}$
Assertion	cpmadugsumlemC	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = {\sum_{Y}}_{i = 0}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))$

Proof

Step	Hyp	Ref	Expression
1		cpmadugsum.a	$⊢ A = N Mat R$
2		cpmadugsum.b	$⊢ B = {Base}_{A}$
3		cpmadugsum.p	$⊢ P = {Poly}_{1} (R)$
4		cpmadugsum.y	$⊢ Y = N Mat P$
5		cpmadugsum.t	$⊢ T = N matToPolyMat R$
6		cpmadugsum.x	$⊢ X = {var}_{1} (R)$
7		cpmadugsum.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
8		cpmadugsum.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
9		cpmadugsum.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
10		cpmadugsum.1	$⊢ \underset{˙}{1} = 1_{Y}$
11		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
12		eqid	$⊢ 0_{Y} = 0_{Y}$
13		crngring	$⊢ R \in CRing \to R \in Ring$
14	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
15	13 14	syl	$⊢ R \in CRing \to P \in Ring$
16	15	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in Ring)$
17	4	matring	$⊢ (N \in Fin \land P \in Ring) \to Y \in Ring$
18	16 17	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
19	18	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
20	19	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to Y \in Ring$
21		ovexd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to (0 \dots s) \in V$
22	5 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
23	13 22	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
24	23	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to T (M) \in {Base}_{Y}$
25	16	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in Ring)$
26	4	matlmod	$⊢ (N \in Fin \land P \in Ring) \to Y \in LMod$
27	25 26	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in LMod$
28	27	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to Y \in LMod$
29		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
30		eqid	$⊢ {Base}_{P} = {Base}_{P}$
31	29 30	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
32	15	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in Ring$
33	29	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
34	32 33	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{P} \in Mnd$
35	34	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to {mulGrp}_{P} \in Mnd$
36		elfznn0	$⊢ i \in (0 \dots s) \to i \in ℕ_{0}$
37	36	adantl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \in ℕ_{0}$
38	13	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
39	6 3 30	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
40	38 39	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \in {Base}_{P}$
41	40	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to X \in {Base}_{P}$
42	31 7 35 37 41	mulgnn0cld	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \underset{˙}{\times} X \in {Base}_{P}$
43	3	ply1crng	$⊢ R \in CRing \to P \in CRing$
44	43	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in CRing)$
45	44	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in CRing)$
46	4	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (Y)$
47	45 46	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P = Scalar (Y)$
48	47	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (Y) = P$
49	48	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (Y)} = {Base}_{P}$
50	49	eleq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (i \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \leftrightarrow i \underset{˙}{\times} X \in {Base}_{P})$
51	50	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (i \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \leftrightarrow i \underset{˙}{\times} X \in {Base}_{P})$
52	42 51	mpbird	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \underset{˙}{\times} X \in {Base}_{Scalar (Y)}$
53		simpll1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to N \in Fin$
54	38	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to R \in Ring$
55		simplrl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to s \in ℕ_{0}$
56		simprr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to b \in (B^{(0 \dots s)})$
57	56	anim1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (b \in (B^{(0 \dots s)}) \land i \in (0 \dots s))$
58	1 2 3 4 5	m2pmfzmap	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land (b \in (B^{(0 \dots s)}) \land i \in (0 \dots s))) \to T (b (i)) \in {Base}_{Y}$
59	53 54 55 57 58	syl31anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to T (b (i)) \in {Base}_{Y}$
60		eqid	$⊢ Scalar (Y) = Scalar (Y)$
61		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
62	11 60 8 61	lmodvscl	$⊢ (Y \in LMod \land i \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \land T (b (i)) \in {Base}_{Y}) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
63	28 52 59 62	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
64		simpl1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to N \in Fin$
65	38	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to R \in Ring$
66		simprl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to s \in ℕ_{0}$
67		eqid	$⊢ (i \in (0 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = (i \in (0 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$
68		fzfid	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land b \in (B^{(0 \dots s)})) \to (0 \dots s) \in Fin$
69		ovexd	$⊢ (((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land b \in (B^{(0 \dots s)})) \land i \in (0 \dots s)) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in V$
70		fvexd	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land b \in (B^{(0 \dots s)})) \to 0_{Y} \in V$
71	67 68 69 70	fsuppmptdm	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land b \in (B^{(0 \dots s)})) \to {finSupp}_{0_{Y}} ((i \in (0 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
72	64 65 66 56 71	syl31anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to {finSupp}_{0_{Y}} ((i \in (0 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
73	11 12 9 20 21 24 63 72	gsummulc2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to {\sum_{Y}}_{i = 0}^{s} (T (M) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
74	4	matassa	$⊢ (N \in Fin \land P \in CRing) \to Y \in AssAlg$
75	44 74	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in AssAlg$
76	75	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in AssAlg$
77	76	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to Y \in AssAlg$
78	15	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in Ring$
79	78 33	syl	$⊢ (N \in Fin \land R \in CRing) \to {mulGrp}_{P} \in Mnd$
80	79	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{P} \in Mnd$
81	80	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to {mulGrp}_{P} \in Mnd$
82	31 7 81 37 41	mulgnn0cld	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \underset{˙}{\times} X \in {Base}_{P}$
83	49	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to {Base}_{Scalar (Y)} = {Base}_{P}$
84	82 83	eleqtrrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \underset{˙}{\times} X \in {Base}_{Scalar (Y)}$
85	23	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to T (M) \in {Base}_{Y}$
86	11 60 61 8 9	assaassr	$⊢ (Y \in AssAlg \land (i \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \land T (M) \in {Base}_{Y} \land T (b (i)) \in {Base}_{Y})) \to T (M) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))$
87	77 84 85 59 86	syl13anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to T (M) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))$
88	87	mpteq2dva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to (i \in (0 \dots s) ⟼ T (M) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = (i \in (0 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))$
89	88	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to {\sum_{Y}}_{i = 0}^{s} (T (M) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = {\sum_{Y}}_{i = 0}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))$
90	73 89	eqtr3d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = {\sum_{Y}}_{i = 0}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))$

Metamath Proof Explorer

Theorem cpmadugsumlemC

Proof