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 ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsgprod.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
pwsgprod.o ⊢ 1 = ( 1r ‘ 𝑌 )
pwsgprod.m ⊢ 𝑀 = ( mulGrp ‘ 𝑌 )
pwsgprod.t ⊢ 𝑇 = ( mulGrp ‘ 𝑅 )
pwsgprod.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
pwsgprod.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
pwsgprod.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
pwsgprod.f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑈 ∈ 𝐵 )
pwsgprod.w ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 1 )
Assertion pwsgprod ( 𝜑 → ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑇 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )

Proof

Step Hyp Ref Expression
1 pwsgprod.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsgprod.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 pwsgprod.o ⊢ 1 = ( 1r ‘ 𝑌 )
4 pwsgprod.m ⊢ 𝑀 = ( mulGrp ‘ 𝑌 )
5 pwsgprod.t ⊢ 𝑇 = ( mulGrp ‘ 𝑅 )
6 pwsgprod.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7 pwsgprod.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
8 pwsgprod.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
9 pwsgprod.f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) ) → 𝑈 ∈ 𝐵 )
10 pwsgprod.w ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 1 )
11 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
12 4 11 mgpbas ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑀 )
13 4 3 ringidval ⊢ 1 = ( 0g ‘ 𝑀 )
14 1 pwscrng ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ CRing )
15 8 6 14 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ CRing )
16 4 crngmgp ⊢ ( 𝑌 ∈ CRing → 𝑀 ∈ CMnd )
17 15 16 syl ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
18 8 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → 𝑅 ∈ CRing )
19 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → 𝐼 ∈ 𝑉 )
20 9 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑈 ∈ 𝐵 )
21 20 an32s ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑈 ∈ 𝐵 )
22 21 fmpttd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) : 𝐼 ⟶ 𝐵 )
23 1 2 11 18 19 22 pwselbasr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ ( Base ‘ 𝑌 ) )
24 23 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) : 𝐽 ⟶ ( Base ‘ 𝑌 ) )
25 12 13 17 7 24 10 gsumcl ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ∈ ( Base ‘ 𝑌 ) )
26 1 2 11 8 6 25 pwselbas ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) : 𝐼 ⟶ 𝐵 )
27 26 ffnd ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) Fn 𝐼 )
28 nfcv ⊢ Ⅎ 𝑥 𝑀
29 nfcv ⊢ Ⅎ 𝑥 Σg
30 nfcv ⊢ Ⅎ 𝑥 𝐽
31 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐼 ↦ 𝑈 )
32 30 31 nfmpt ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) )
33 28 29 32 nfov ⊢ Ⅎ 𝑥 ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) )
34 33 dffn5f ⊢ ( ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) Fn 𝐼 ↔ ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) ) )
35 27 34 sylib ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
37 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑈 )
38 37 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑈 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) = 𝑈 )
39 36 20 38 syl2an2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) = 𝑈 )
40 39 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∈ 𝐽 ↦ ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) )
41 40 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑇 Σg ( 𝑦 ∈ 𝐽 ↦ ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) ) ) = ( 𝑇 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) )
42 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑀 ∈ CMnd )
43 5 crngmgp ⊢ ( 𝑅 ∈ CRing → 𝑇 ∈ CMnd )
44 8 43 syl ⊢ ( 𝜑 → 𝑇 ∈ CMnd )
45 44 cmnmndd ⊢ ( 𝜑 → 𝑇 ∈ Mnd )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑇 ∈ Mnd )
47 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐽 ∈ 𝑊 )
48 8 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ Ring )
50 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑉 )
51 1 11 4 5 49 50 36 pwspjmhmmgpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑎 ∈ ( Base ‘ 𝑌 ) ↦ ( 𝑎 ‘ 𝑥 ) ) ∈ ( 𝑀 MndHom 𝑇 ) )
52 23 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ∈ ( Base ‘ 𝑌 ) )
53 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) finSupp 1 )
54 fveq1 ⊢ ( 𝑎 = ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) → ( 𝑎 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) )
55 fveq1 ⊢ ( 𝑎 = ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) → ( 𝑎 ‘ 𝑥 ) = ( ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) )
56 12 13 42 46 47 51 52 53 54 55 gsummhm2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑇 Σg ( 𝑦 ∈ 𝐽 ↦ ( ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ‘ 𝑥 ) ) ) = ( ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) )
57 41 56 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑇 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) = ( ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) )
58 57 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑇 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) ‘ 𝑥 ) ) )
59 35 58 eqtr4d ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑦 ∈ 𝐽 ↦ ( 𝑥 ∈ 𝐼 ↦ 𝑈 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑇 Σg ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )