frlmgsum

Description: Finite commutative sums in a free module are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Mario Carneiro, 5-Jul-2015) (Revised by AV, 23-Jun-2019)

	Ref	Expression
Hypotheses	frlmgsum.y	$⊢ Y = R freeLMod I$
	frlmgsum.b	$⊢ B = {Base}_{Y}$
	frlmgsum.z	$⊢ \underset{˙}{0} = 0_{Y}$
	frlmgsum.i	$⊢ φ \to I \in V$
	frlmgsum.j	$⊢ φ \to J \in W$
	frlmgsum.r	$⊢ φ \to R \in Ring$
	frlmgsum.f	$⊢ (φ \land y \in J) \to (x \in I ⟼ U) \in B$
	frlmgsum.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((y \in J ⟼ (x \in I ⟼ U)))$
Assertion	frlmgsum	$⊢ φ \to \underset{y \in J}{\sum_{Y}} (x \in I ⟼ U) = (x \in I ⟼ \underset{y \in J}{\sum_{R}} U)$

Proof

Step	Hyp	Ref	Expression
1		frlmgsum.y	$⊢ Y = R freeLMod I$
2		frlmgsum.b	$⊢ B = {Base}_{Y}$
3		frlmgsum.z	$⊢ \underset{˙}{0} = 0_{Y}$
4		frlmgsum.i	$⊢ φ \to I \in V$
5		frlmgsum.j	$⊢ φ \to J \in W$
6		frlmgsum.r	$⊢ φ \to R \in Ring$
7		frlmgsum.f	$⊢ (φ \land y \in J) \to (x \in I ⟼ U) \in B$
8		frlmgsum.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((y \in J ⟼ (x \in I ⟼ U)))$
9	1 2	frlmpws	$⊢ (R \in Ring \land I \in V) \to Y = (ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} B$
10	6 4 9	syl2anc	$⊢ φ \to Y = (ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} B$
11	10	oveq1d	$⊢ φ \to \underset{y \in J}{\sum_{Y}} (x \in I ⟼ U) = \underset{y \in J}{\sum_{(ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} B}} (x \in I ⟼ U)$
12		eqid	$⊢ {Base}_{(ringLMod (R) ↑_{𝑠} I)} = {Base}_{(ringLMod (R) ↑_{𝑠} I)}$
13		eqid	$⊢ +_{(ringLMod (R) ↑_{𝑠} I)} = +_{(ringLMod (R) ↑_{𝑠} I)}$
14		eqid	$⊢ (ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} B = (ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} B$
15		ovexd	$⊢ φ \to ringLMod (R) ↑_{𝑠} I \in V$
16		eqid	$⊢ LSubSp (ringLMod (R) ↑_{𝑠} I) = LSubSp (ringLMod (R) ↑_{𝑠} I)$
17	1 2 16	frlmlss	$⊢ (R \in Ring \land I \in V) \to B \in LSubSp (ringLMod (R) ↑_{𝑠} I)$
18	6 4 17	syl2anc	$⊢ φ \to B \in LSubSp (ringLMod (R) ↑_{𝑠} I)$
19	12 16	lssss	$⊢ B \in LSubSp (ringLMod (R) ↑_{𝑠} I) \to B \subseteq {Base}_{(ringLMod (R) ↑_{𝑠} I)}$
20	18 19	syl	$⊢ φ \to B \subseteq {Base}_{(ringLMod (R) ↑_{𝑠} I)}$
21	7	fmpttd	$⊢ φ \to (y \in J ⟼ (x \in I ⟼ U)) : J ⟶ B$
22		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
23	6 22	syl	$⊢ φ \to ringLMod (R) \in LMod$
24		eqid	$⊢ ringLMod (R) ↑_{𝑠} I = ringLMod (R) ↑_{𝑠} I$
25	24	pwslmod	$⊢ (ringLMod (R) \in LMod \land I \in V) \to ringLMod (R) ↑_{𝑠} I \in LMod$
26	23 4 25	syl2anc	$⊢ φ \to ringLMod (R) ↑_{𝑠} I \in LMod$
27		eqid	$⊢ 0_{(ringLMod (R) ↑_{𝑠} I)} = 0_{(ringLMod (R) ↑_{𝑠} I)}$
28	27 16	lss0cl	$⊢ (ringLMod (R) ↑_{𝑠} I \in LMod \land B \in LSubSp (ringLMod (R) ↑_{𝑠} I)) \to 0_{(ringLMod (R) ↑_{𝑠} I)} \in B$
29	26 18 28	syl2anc	$⊢ φ \to 0_{(ringLMod (R) ↑_{𝑠} I)} \in B$
30		lmodcmn	$⊢ ringLMod (R) \in LMod \to ringLMod (R) \in CMnd$
31	23 30	syl	$⊢ φ \to ringLMod (R) \in CMnd$
32		cmnmnd	$⊢ ringLMod (R) \in CMnd \to ringLMod (R) \in Mnd$
33	31 32	syl	$⊢ φ \to ringLMod (R) \in Mnd$
34	24	pwsmnd	$⊢ (ringLMod (R) \in Mnd \land I \in V) \to ringLMod (R) ↑_{𝑠} I \in Mnd$
35	33 4 34	syl2anc	$⊢ φ \to ringLMod (R) ↑_{𝑠} I \in Mnd$
36	12 13 27	mndlrid	$⊢ (ringLMod (R) ↑_{𝑠} I \in Mnd \land x \in {Base}_{(ringLMod (R) ↑_{𝑠} I)}) \to (0_{(ringLMod (R) ↑_{𝑠} I)} +_{(ringLMod (R) ↑_{𝑠} I)} x = x \land x +_{(ringLMod (R) ↑_{𝑠} I)} 0_{(ringLMod (R) ↑_{𝑠} I)} = x)$
37	35 36	sylan	$⊢ (φ \land x \in {Base}_{(ringLMod (R) ↑_{𝑠} I)}) \to (0_{(ringLMod (R) ↑_{𝑠} I)} +_{(ringLMod (R) ↑_{𝑠} I)} x = x \land x +_{(ringLMod (R) ↑_{𝑠} I)} 0_{(ringLMod (R) ↑_{𝑠} I)} = x)$
38	12 13 14 15 5 20 21 29 37	gsumress	$⊢ φ \to \underset{y \in J}{\sum_{ringLMod (R) ↑_{𝑠} I}} (x \in I ⟼ U) = \underset{y \in J}{\sum_{(ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} B}} (x \in I ⟼ U)$
39		rlmbas	$⊢ {Base}_{R} = {Base}_{ringLMod (R)}$
40		eqid	$⊢ {Base}_{R} = {Base}_{R}$
41	1 40 2	frlmbasf	$⊢ (I \in V \land (x \in I ⟼ U) \in B) \to (x \in I ⟼ U) : I ⟶ {Base}_{R}$
42	4 7 41	syl2an2r	$⊢ (φ \land y \in J) \to (x \in I ⟼ U) : I ⟶ {Base}_{R}$
43	42	fvmptelcdm	$⊢ ((φ \land y \in J) \land x \in I) \to U \in {Base}_{R}$
44	43	an32s	$⊢ ((φ \land x \in I) \land y \in J) \to U \in {Base}_{R}$
45	44	anasss	$⊢ (φ \land (x \in I \land y \in J)) \to U \in {Base}_{R}$
46	10	fveq2d	$⊢ φ \to 0_{Y} = 0_{((ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} B)}$
47	16	lsssubg	$⊢ (ringLMod (R) ↑_{𝑠} I \in LMod \land B \in LSubSp (ringLMod (R) ↑_{𝑠} I)) \to B \in SubGrp (ringLMod (R) ↑_{𝑠} I)$
48	26 18 47	syl2anc	$⊢ φ \to B \in SubGrp (ringLMod (R) ↑_{𝑠} I)$
49	14 27	subg0	$⊢ B \in SubGrp (ringLMod (R) ↑_{𝑠} I) \to 0_{(ringLMod (R) ↑_{𝑠} I)} = 0_{((ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} B)}$
50	48 49	syl	$⊢ φ \to 0_{(ringLMod (R) ↑_{𝑠} I)} = 0_{((ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} B)}$
51	46 50	eqtr4d	$⊢ φ \to 0_{Y} = 0_{(ringLMod (R) ↑_{𝑠} I)}$
52	3 51	eqtrid	$⊢ φ \to \underset{˙}{0} = 0_{(ringLMod (R) ↑_{𝑠} I)}$
53	8 52	breqtrd	$⊢ φ \to {finSupp}_{0_{(ringLMod (R) ↑_{𝑠} I)}} ((y \in J ⟼ (x \in I ⟼ U)))$
54	24 39 27 4 5 31 45 53	pwsgsum	$⊢ φ \to \underset{y \in J}{\sum_{ringLMod (R) ↑_{𝑠} I}} (x \in I ⟼ U) = (x \in I ⟼ \underset{y \in J}{\sum_{ringLMod (R)}} U)$
55	5	mptexd	$⊢ φ \to (y \in J ⟼ U) \in V$
56		fvexd	$⊢ φ \to ringLMod (R) \in V$
57	39	a1i	$⊢ φ \to {Base}_{R} = {Base}_{ringLMod (R)}$
58		rlmplusg	$⊢ +_{R} = +_{ringLMod (R)}$
59	58	a1i	$⊢ φ \to +_{R} = +_{ringLMod (R)}$
60	55 6 56 57 59	gsumpropd	$⊢ φ \to \underset{y \in J}{\sum_{R}} U = \underset{y \in J}{\sum_{ringLMod (R)}} U$
61	60	mpteq2dv	$⊢ φ \to (x \in I ⟼ \underset{y \in J}{\sum_{R}} U) = (x \in I ⟼ \underset{y \in J}{\sum_{ringLMod (R)}} U)$
62	54 61	eqtr4d	$⊢ φ \to \underset{y \in J}{\sum_{ringLMod (R) ↑_{𝑠} I}} (x \in I ⟼ U) = (x \in I ⟼ \underset{y \in J}{\sum_{R}} U)$
63	11 38 62	3eqtr2d	$⊢ φ \to \underset{y \in J}{\sum_{Y}} (x \in I ⟼ U) = (x \in I ⟼ \underset{y \in J}{\sum_{R}} U)$

Metamath Proof Explorer

Theorem frlmgsum

Proof