Theorem prdsgsum 18818

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
prdsgsum	⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))))

Distinct variable groups:   𝑥,𝑦,𝐼   𝑥,𝐽,𝑦   𝑥,𝑌,𝑦   𝜑,𝑥,𝑦

Allowed substitution hints:   𝐵(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝑆(𝑥,𝑦)   𝑈(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)   𝑋(𝑥,𝑦)   0 (𝑥,𝑦)

Proof of Theorem prdsgsum

Dummy variable 𝑎 is distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2080  ∀wral 3104   class class class wbr 4964   ↦ cmpt 5043   Fn wfn 6223  ⟶wf 6224  ‘cfv 6228  (class class class)co 7019   finSupp cfsupp 8682  Basecbs 16312  0_gc0g 16542   Σ_g cgsu 16543  X_scprds 16548  Mndcmnd 17733   MndHom cmhm 17772  CMndccmn 18633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322  ax-cnex 10442  ax-resscn 10443  ax-1cn 10444  ax-icn 10445  ax-addcl 10446  ax-addrcl 10447  ax-mulcl 10448  ax-mulrcl 10449  ax-mulcom 10450  ax-addass 10451  ax-mulass 10452  ax-distr 10453  ax-i2m1 10454  ax-1ne0 10455  ax-1rid 10456  ax-rnegex 10457  ax-rrecex 10458  ax-cnre 10459  ax-pre-lttri 10460  ax-pre-lttrn 10461  ax-pre-ltadd 10462  ax-pre-mulgt0 10463

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-nel 3090  df-ral 3109  df-rex 3110  df-reu 3111  df-rmo 3112  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-int 4785  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-se 5406  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-pred 6026  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-isom 6237  df-riota 6980  df-ov 7022  df-oprab 7023  df-mpo 7024  df-om 7440  df-1st 7548  df-2nd 7549  df-supp 7685  df-wrecs 7801  df-recs 7863  df-rdg 7901  df-1o 7956  df-oadd 7960  df-er 8142  df-map 8261  df-ixp 8314  df-en 8361  df-dom 8362  df-sdom 8363  df-fin 8364  df-fsupp 8683  df-sup 8755  df-oi 8823  df-card 9217  df-pnf 10526  df-mnf 10527  df-xr 10528  df-ltxr 10529  df-le 10530  df-sub 10721  df-neg 10722  df-nn 11489  df-2 11550  df-3 11551  df-4 11552  df-5 11553  df-6 11554  df-7 11555  df-8 11556  df-9 11557  df-n0 11748  df-z 11832  df-dec 11949  df-uz 12094  df-fz 12743  df-fzo 12884  df-seq 13220  df-hash 13541  df-struct 16314  df-ndx 16315  df-slot 16316  df-base 16318  df-plusg 16407  df-mulr 16408  df-sca 16410  df-vsca 16411  df-ip 16412  df-tset 16413  df-ple 16414  df-ds 16416  df-hom 16418  df-cco 16419  df-0g 16544  df-gsum 16545  df-prds 16550  df-mgm 17681  df-sgrp 17723  df-mnd 17734  df-mhm 17774  df-cntz 18188  df-cmn 18635

This theorem is referenced by:  pwsgsum  18819