Metamath Proof Explorer

Theorem 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 ^s I )
pwsgprod.b 
|- B = ( Base ` R )
pwsgprod.o 
|- .1. = ( 1r ` Y )
pwsgprod.m 
|- M = ( mulGrp ` Y )
pwsgprod.t 
|- T = ( mulGrp ` R )
pwsgprod.i 
|- ( ph -> I e. V )
pwsgprod.j 
|- ( ph -> J e. W )
pwsgprod.r 
|- ( ph -> R e. CRing )
pwsgprod.f 
|- ( ( ph /\ ( x e. I /\ y e. J ) ) -> U e. B )
pwsgprod.w 
|- ( ph -> ( y e. J |-> ( x e. I |-> U ) ) finSupp .1. )
Assertion pwsgprod 
|- ( ph -> ( M gsum ( y e. J |-> ( x e. I |-> U ) ) ) = ( x e. I |-> ( T gsum ( y e. J |-> U ) ) ) )

Proof

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