Metamath Proof Explorer

Theorem 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 ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
frlmgsum.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
frlmgsum.z ⊢ 0 = ( 0g ‘ 𝑌 )
frlmgsum.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
frlmgsum.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
frlmgsum.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
frlmgsum.f ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ 𝐵 )
frlmgsum.w ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 0 )
Assertion frlmgsum ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )

Proof

Step Hyp Ref Expression
1 frlmgsum.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
2 frlmgsum.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 frlmgsum.z ⊢ 0 = ( 0g ‘ 𝑌 )
4 frlmgsum.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 frlmgsum.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
6 frlmgsum.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 frlmgsum.f ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ 𝐵 )
8 frlmgsum.w ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 0 )
9 1 2 frlmpws ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
10 6 4 9 syl2anc ⊢ ( 𝜑 → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
11 10 oveq1d ⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) )
12 eqid ⊢ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
13 eqid ⊢ ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
14 eqid ⊢ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 )
15 ovexd ⊢ ( 𝜑 → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ V )
16 eqid ⊢ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
17 1 2 16 frlmlss ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
18 6 4 17 syl2anc ⊢ ( 𝜑 → 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
19 12 16 lssss ⊢ ( 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) → 𝐵 ⊆ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
20 18 19 syl ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
21 7 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) : 𝐽 ⟶ 𝐵 )
22 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
23 6 22 syl ⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ LMod )
24 eqid ⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
25 24 pwslmod ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼 ∈ 𝑉 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod )
26 23 4 25 syl2anc ⊢ ( 𝜑 → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod )
27 eqid ⊢ ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
28 27 16 lss0cl ⊢ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod ∧ 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) → ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ∈ 𝐵 )
29 26 18 28 syl2anc ⊢ ( 𝜑 → ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ∈ 𝐵 )
30 lmodcmn ⊢ ( ( ringLMod ‘ 𝑅 ) ∈ LMod → ( ringLMod ‘ 𝑅 ) ∈ CMnd )
31 23 30 syl ⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ CMnd )
32 cmnmnd ⊢ ( ( ringLMod ‘ 𝑅 ) ∈ CMnd → ( ringLMod ‘ 𝑅 ) ∈ Mnd )
33 31 32 syl ⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ Mnd )
34 24 pwsmnd ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ Mnd )
35 33 4 34 syl2anc ⊢ ( 𝜑 → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ Mnd )
36 12 13 27 mndlrid ⊢ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) → ( ( ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) = 𝑥 ) )
37 35 36 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) → ( ( ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) = 𝑥 ) )
38 12 13 14 15 5 20 21 29 37 gsumress ⊢ ( 𝜑 → ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) )
39 rlmbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
40 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
41 1 40 2 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ 𝐵 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
42 4 7 41 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
43 42 fvmptelcdm ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑈 ∈ ( Base ‘ 𝑅 ) )
44 43 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑈 ∈ ( Base ‘ 𝑅 ) )
45 44 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑈 ∈ ( Base ‘ 𝑅 ) )
46 10 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝑌 ) = ( 0g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
47 16 lsssubg ⊢ ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod ∧ 𝐵 ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) → 𝐵 ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
48 26 18 47 syl2anc ⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
49 14 27 subg0 ⊢ ( 𝐵 ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) → ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( 0g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
50 48 49 syl ⊢ ( 𝜑 → ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( 0g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
51 46 50 eqtr4d ⊢ ( 𝜑 → ( 0g ‘ 𝑌 ) = ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
52 3 51 eqtrid ⊢ ( 𝜑 → 0 = ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
53 8 52 breqtrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
54 24 39 27 4 5 31 45 53 pwsgsum ⊢ ( 𝜑 → ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ringLMod ‘ 𝑅 ) Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )
55 5 mptexd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ∈ V )
56 fvexd ⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ V )
57 39 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) )
58 rlmplusg ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
59 58 a1i ⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) ) )
60 55 6 56 57 59 gsumpropd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) = ( ( ringLMod ‘ 𝑅 ) Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) )
61 60 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ringLMod ‘ 𝑅 ) Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )
62 54 61 eqtr4d ⊢ ( 𝜑 → ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )
63 11 38 62 3eqtr2d ⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )