This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsgsum

Description: Finite commutative sums in a product structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Mario Carneiro, 3-Jul-2015) (Revised by AV, 9-Jun-2019)

Ref Expression
Hypotheses prdsgsum.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
prdsgsum.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
prdsgsum.z ⊢ 0 = ( 0g ‘ 𝑌 )
prdsgsum.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
prdsgsum.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
prdsgsum.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑋 )
prdsgsum.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ CMnd )
prdsgsum.f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑈 ∈ 𝐵 )
prdsgsum.w ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 0 )
Assertion prdsgsum ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )

Proof

Step Hyp Ref Expression
1 prdsgsum.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
2 prdsgsum.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 prdsgsum.z ⊢ 0 = ( 0g ‘ 𝑌 )
4 prdsgsum.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 prdsgsum.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
6 prdsgsum.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑋 )
7 prdsgsum.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ CMnd )
8 prdsgsum.f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑈 ∈ 𝐵 )
9 prdsgsum.w ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 0 )
10 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
11 7 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) : 𝐼 ⟶ CMnd )
12 11 ffnd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
13 1 4 6 11 prdscmnd ⊢ ( 𝜑 → 𝑌 ∈ CMnd )
14 8 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑈 ∈ 𝐵 )
15 14 an32s ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑈 ∈ 𝐵 )
16 15 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ∀ 𝑥 ∈ 𝐼 𝑈 ∈ 𝐵 )
17 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ CMnd )
18 1 10 6 4 17 2 prdsbasmpt2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ ( Base ‘ 𝑌 ) ↔ ∀ 𝑥 ∈ 𝐼 𝑈 ∈ 𝐵 ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ ( Base ‘ 𝑌 ) ↔ ∀ 𝑥 ∈ 𝐼 𝑈 ∈ 𝐵 ) )
20 16 19 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ ( Base ‘ 𝑌 ) )
21 20 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) : 𝐽 ⟶ ( Base ‘ 𝑌 ) )
22 10 3 13 5 21 9 gsumcl ⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ∈ ( Base ‘ 𝑌 ) )
23 1 10 6 4 12 22 prdsbasfn ⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) Fn 𝐼 )
24 nfcv ⊢ Ⅎ 𝑥 𝑌
25 nfcv ⊢ Ⅎ 𝑥 Σg
26 nfcv ⊢ Ⅎ 𝑥 𝐽
27 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐼 ↦ 𝑈 )
28 26 27 nfmpt ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) )
29 24 25 28 nfov ⊢ Ⅎ 𝑥 ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) )
30 29 dffn5f ⊢ ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) Fn 𝐼 ↔ ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) ) )
31 23 30 sylib ⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) ) )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
33 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑈 )
34 33 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑈 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) = 𝑈 )
35 32 14 34 syl2an2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) = 𝑈 )
36 35 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∈ 𝐽 ↦ ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) )
37 36 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) )
38 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑌 ∈ CMnd )
39 cmnmnd ⊢ ( 𝑅 ∈ CMnd → 𝑅 ∈ Mnd )
40 7 39 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ Mnd )
41 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐽 ∈ 𝑊 )
42 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑉 )
43 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ 𝑋 )
44 40 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) : 𝐼 ⟶ Mnd )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) : 𝐼 ⟶ Mnd )
46 1 10 42 43 45 32 prdspjmhm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( 𝑌 MndHom ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) )
47 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 )
48 47 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑅 ∈ CMnd ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
49 32 7 48 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
50 49 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑌 MndHom ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑥 ) ) = ( 𝑌 MndHom 𝑅 ) )
51 46 50 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( 𝑌 MndHom 𝑅 ) )
52 20 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ ( Base ‘ 𝑌 ) )
53 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 0 )
54 fveq1 ⊢ ( 𝑎 = ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) → ( 𝑎 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) )
55 fveq1 ⊢ ( 𝑎 = ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) → ( 𝑎 ‘ 𝑥 ) = ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) )
56 10 3 38 40 41 51 52 53 54 55 gsummhm2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) ) ) = ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) )
57 37 56 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) = ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) )
58 57 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) ) )
59 31 58 eqtr4d ⊢ ( 𝜑 → ( 𝑌 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑅 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )