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