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		eqid	$⊢ +_{Y} = +_{Y}$
14		crngring	$⊢ R \in CRing \to R \in Ring$
15	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
16	14 15	syl	$⊢ R \in CRing \to P \in Ring$
17	16	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in Ring)$
18	4	matring	$⊢ (N \in Fin \land P \in Ring) \to Y \in Ring$
19	17 18	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
20	19	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
21	20	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$
22		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$
23	5 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
24	14 23	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
25	24	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}$
26	17	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in Ring)$
27	4	matlmod	$⊢ (N \in Fin \land P \in Ring) \to Y \in LMod$
28	26 27	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in LMod$
29	28	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$
30	16	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in Ring$
31		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
32	31	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
33	30 32	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{P} \in Mnd$
34	33	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$
35		elfznn0	$⊢ i \in (0 \dots s) \to i \in ℕ_{0}$
36	35	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}$
37	14	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
38		eqid	$⊢ {Base}_{P} = {Base}_{P}$
39	6 3 38	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
40	37 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 38	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
43	42 7	mulgnn0cl	$⊢ ({mulGrp}_{P} \in Mnd \land i \in ℕ_{0} \land X \in {Base}_{P}) \to i \underset{˙}{\times} X \in {Base}_{P}$
44	34 36 41 43	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 \in {Base}_{P}$
45	3	ply1crng	$⊢ R \in CRing \to P \in CRing$
46	45	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in CRing)$
47	46	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in CRing)$
48	4	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (Y)$
49	47 48	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P = Scalar (Y)$
50	49	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (Y) = P$
51	50	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (Y)} = {Base}_{P}$
52	51	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})$
53	52	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})$
54	44 53	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)}$
55		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$
56	37	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$
57		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}$
58		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)})$
59	58	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))$
60	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}$
61	55 56 57 59 60	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}$
62		eqid	$⊢ Scalar (Y) = Scalar (Y)$
63		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
64	11 62 8 63	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}$
65	29 54 61 64	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}$
66		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$
67	37	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$
68		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}$
69		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)))$
70		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$
71		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$
72		fvexd	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land b \in (B^{(0 \dots s)})) \to 0_{Y} \in V$
73	69 70 71 72	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))))$
74	66 67 68 58 73	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))))$
75	11 12 13 9 21 22 25 65 74	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))))$
76	4	matassa	$⊢ (N \in Fin \land P \in CRing) \to Y \in AssAlg$
77	46 76	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in AssAlg$
78	77	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in AssAlg$
79	78	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$
80	16	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in Ring$
81	80 32	syl	$⊢ (N \in Fin \land R \in CRing) \to {mulGrp}_{P} \in Mnd$
82	81	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{P} \in Mnd$
83	82	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$
84	83 36 41 43	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 \in {Base}_{P}$
85	51	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}$
86	84 85	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)}$
87	24	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}$
88	11 62 63 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)))$
89	79 86 87 61 88	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)))$
90	89	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))))$
91	90	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))))$
92	75 91	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