pwsgprod

Description: Finite products in a power structure are taken componentwise. Compare pwsgsum . (Contributed by SN, 30-Jul-2024)

	Ref	Expression
Hypotheses	pwsgprod.y	$⊢ Y = R ↑_{𝑠} I$
	pwsgprod.b	$⊢ B = {Base}_{R}$
	pwsgprod.o	$⊢ \underset{˙}{1} = 1_{Y}$
	pwsgprod.m	$⊢ M = {mulGrp}_{Y}$
	pwsgprod.t	$⊢ T = {mulGrp}_{R}$
	pwsgprod.i	$⊢ φ \to I \in V$
	pwsgprod.j	$⊢ φ \to J \in W$
	pwsgprod.r	$⊢ φ \to R \in CRing$
	pwsgprod.f	$⊢ (φ \land (x \in I \land y \in J)) \to U \in B$
	pwsgprod.w	$⊢ φ \to {finSupp}_{\underset{˙}{1}} ((y \in J ⟼ (x \in I ⟼ U)))$
Assertion	pwsgprod	$⊢ φ \to \underset{y \in J}{\sum_{M}} (x \in I ⟼ U) = (x \in I ⟼ \underset{y \in J}{\sum_{T}} U)$

Proof

Step	Hyp	Ref	Expression
1		pwsgprod.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsgprod.b	$⊢ B = {Base}_{R}$
3		pwsgprod.o	$⊢ \underset{˙}{1} = 1_{Y}$
4		pwsgprod.m	$⊢ M = {mulGrp}_{Y}$
5		pwsgprod.t	$⊢ T = {mulGrp}_{R}$
6		pwsgprod.i	$⊢ φ \to I \in V$
7		pwsgprod.j	$⊢ φ \to J \in W$
8		pwsgprod.r	$⊢ φ \to R \in CRing$
9		pwsgprod.f	$⊢ (φ \land (x \in I \land y \in J)) \to U \in B$
10		pwsgprod.w	$⊢ φ \to {finSupp}_{\underset{˙}{1}} ((y \in J ⟼ (x \in I ⟼ U)))$
11		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
12	4 11	mgpbas	$⊢ {Base}_{Y} = {Base}_{M}$
13	4 3	ringidval	$⊢ \underset{˙}{1} = 0_{M}$
14	1	pwscrng	$⊢ (R \in CRing \land I \in V) \to Y \in CRing$
15	8 6 14	syl2anc	$⊢ φ \to Y \in CRing$
16	4	crngmgp	$⊢ Y \in CRing \to M \in CMnd$
17	15 16	syl	$⊢ φ \to M \in CMnd$
18	8	adantr	$⊢ (φ \land y \in J) \to R \in CRing$
19	6	adantr	$⊢ (φ \land y \in J) \to I \in V$
20	9	anassrs	$⊢ ((φ \land x \in I) \land y \in J) \to U \in B$
21	20	an32s	$⊢ ((φ \land y \in J) \land x \in I) \to U \in B$
22	21	fmpttd	$⊢ (φ \land y \in J) \to (x \in I ⟼ U) : I ⟶ B$
23	1 2 11 18 19 22	pwselbasr	$⊢ (φ \land y \in J) \to (x \in I ⟼ U) \in {Base}_{Y}$
24	23	fmpttd	$⊢ φ \to (y \in J ⟼ (x \in I ⟼ U)) : J ⟶ {Base}_{Y}$
25	12 13 17 7 24 10	gsumcl	$⊢ φ \to \underset{y \in J}{\sum_{M}} (x \in I ⟼ U) \in {Base}_{Y}$
26	1 2 11 8 6 25	pwselbas	$⊢ φ \to (\underset{y \in J}{\sum_{M}}, (x \in I ⟼ U)) : I ⟶ B$
27	26	ffnd	$⊢ φ \to (\underset{y \in J}{\sum_{M}}, (x \in I ⟼ U)) Fn I$
28		nfcv	$⊢ \underline{Ⅎ} x M$
29		nfcv	$⊢ \underline{Ⅎ} x Σ_{𝑔}$
30		nfcv	$⊢ \underline{Ⅎ} x J$
31		nfmpt1	$⊢ \underline{Ⅎ} x (x \in I ⟼ U)$
32	30 31	nfmpt	$⊢ \underline{Ⅎ} x (y \in J ⟼ (x \in I ⟼ U))$
33	28 29 32	nfov	$⊢ \underline{Ⅎ} x (\underset{y \in J}{\sum_{M}}, (x \in I ⟼ U))$
34	33	dffn5f	$⊢ (\underset{y \in J}{\sum_{M}}, (x \in I ⟼ U)) Fn I \leftrightarrow \underset{y \in J}{\sum_{M}} (x \in I ⟼ U) = (x \in I ⟼ (\underset{y \in J}{\sum_{M}}, (x \in I ⟼ U)) (x))$
35	27 34	sylib	$⊢ φ \to \underset{y \in J}{\sum_{M}} (x \in I ⟼ U) = (x \in I ⟼ (\underset{y \in J}{\sum_{M}}, (x \in I ⟼ U)) (x))$
36		simpr	$⊢ (φ \land x \in I) \to x \in I$
37		eqid	$⊢ (x \in I ⟼ U) = (x \in I ⟼ U)$
38	37	fvmpt2	$⊢ (x \in I \land U \in B) \to (x \in I ⟼ U) (x) = U$
39	36 20 38	syl2an2r	$⊢ ((φ \land x \in I) \land y \in J) \to (x \in I ⟼ U) (x) = U$
40	39	mpteq2dva	$⊢ (φ \land x \in I) \to (y \in J ⟼ (x \in I ⟼ U) (x)) = (y \in J ⟼ U)$
41	40	oveq2d	$⊢ (φ \land x \in I) \to \underset{y \in J}{\sum_{T}} (x \in I ⟼ U) (x) = \underset{y \in J}{\sum_{T}} U$
42	17	adantr	$⊢ (φ \land x \in I) \to M \in CMnd$
43	5	crngmgp	$⊢ R \in CRing \to T \in CMnd$
44	8 43	syl	$⊢ φ \to T \in CMnd$
45	44	cmnmndd	$⊢ φ \to T \in Mnd$
46	45	adantr	$⊢ (φ \land x \in I) \to T \in Mnd$
47	7	adantr	$⊢ (φ \land x \in I) \to J \in W$
48	8	crngringd	$⊢ φ \to R \in Ring$
49	48	adantr	$⊢ (φ \land x \in I) \to R \in Ring$
50	6	adantr	$⊢ (φ \land x \in I) \to I \in V$
51	1 11 4 5 49 50 36	pwspjmhmmgpd	$⊢ (φ \land x \in I) \to (a \in {Base}_{Y} ⟼ a (x)) \in (M MndHom T)$
52	23	adantlr	$⊢ ((φ \land x \in I) \land y \in J) \to (x \in I ⟼ U) \in {Base}_{Y}$
53	10	adantr	$⊢ (φ \land x \in I) \to {finSupp}_{\underset{˙}{1}} ((y \in J ⟼ (x \in I ⟼ U)))$
54		fveq1	$⊢ a = (x \in I ⟼ U) \to a (x) = (x \in I ⟼ U) (x)$
55		fveq1	$⊢ a = \underset{y \in J}{\sum_{M}} (x \in I ⟼ U) \to a (x) = (\underset{y \in J}{\sum_{M}}, (x \in I ⟼ U)) (x)$
56	12 13 42 46 47 51 52 53 54 55	gsummhm2	$⊢ (φ \land x \in I) \to \underset{y \in J}{\sum_{T}} (x \in I ⟼ U) (x) = (\underset{y \in J}{\sum_{M}}, (x \in I ⟼ U)) (x)$
57	41 56	eqtr3d	$⊢ (φ \land x \in I) \to \underset{y \in J}{\sum_{T}} U = (\underset{y \in J}{\sum_{M}}, (x \in I ⟼ U)) (x)$
58	57	mpteq2dva	$⊢ φ \to (x \in I ⟼ \underset{y \in J}{\sum_{T}} U) = (x \in I ⟼ (\underset{y \in J}{\sum_{M}}, (x \in I ⟼ U)) (x))$
59	35 58	eqtr4d	$⊢ φ \to \underset{y \in J}{\sum_{M}} (x \in I ⟼ U) = (x \in I ⟼ \underset{y \in J}{\sum_{T}} U)$

Metamath Proof Explorer

Theorem pwsgprod

Proof