| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prdsgsum.y | . . . 4
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) | 
| 2 |  | eqid 2736 | . . . 4
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 3 |  | prdsgsum.s | . . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑋) | 
| 4 |  | prdsgsum.i | . . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 5 |  | prdsgsum.r | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CMnd) | 
| 6 | 5 | fmpttd 7134 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑅):𝐼⟶CMnd) | 
| 7 | 6 | ffnd 6736 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑅) Fn 𝐼) | 
| 8 |  | prdsgsum.z | . . . . 5
⊢  0 =
(0g‘𝑌) | 
| 9 | 1, 4, 3, 6 | prdscmnd 19880 | . . . . 5
⊢ (𝜑 → 𝑌 ∈ CMnd) | 
| 10 |  | prdsgsum.j | . . . . 5
⊢ (𝜑 → 𝐽 ∈ 𝑊) | 
| 11 |  | prdsgsum.f | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵) | 
| 12 | 11 | anassrs 467 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → 𝑈 ∈ 𝐵) | 
| 13 | 12 | an32s 652 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ 𝐵) | 
| 14 | 13 | ralrimiva 3145 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ∀𝑥 ∈ 𝐼 𝑈 ∈ 𝐵) | 
| 15 | 5 | ralrimiva 3145 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ CMnd) | 
| 16 |  | prdsgsum.b | . . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) | 
| 17 | 1, 2, 3, 4, 15, 16 | prdsbasmpt2 17528 | . . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑈) ∈ (Base‘𝑌) ↔ ∀𝑥 ∈ 𝐼 𝑈 ∈ 𝐵)) | 
| 18 | 17 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐼 ↦ 𝑈) ∈ (Base‘𝑌) ↔ ∀𝑥 ∈ 𝐼 𝑈 ∈ 𝐵)) | 
| 19 | 14, 18 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝐼 ↦ 𝑈) ∈ (Base‘𝑌)) | 
| 20 | 19 | fmpttd 7134 | . . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)):𝐽⟶(Base‘𝑌)) | 
| 21 |  | prdsgsum.w | . . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 ) | 
| 22 | 2, 8, 9, 10, 20, 21 | gsumcl 19934 | . . . 4
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) ∈ (Base‘𝑌)) | 
| 23 | 1, 2, 3, 4, 7, 22 | prdsbasfn 17517 | . . 3
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) Fn 𝐼) | 
| 24 |  | nfcv 2904 | . . . . 5
⊢
Ⅎ𝑥𝑌 | 
| 25 |  | nfcv 2904 | . . . . 5
⊢
Ⅎ𝑥
Σg | 
| 26 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑥𝐽 | 
| 27 |  | nfmpt1 5249 | . . . . . 6
⊢
Ⅎ𝑥(𝑥 ∈ 𝐼 ↦ 𝑈) | 
| 28 | 26, 27 | nfmpt 5248 | . . . . 5
⊢
Ⅎ𝑥(𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) | 
| 29 | 24, 25, 28 | nfov 7462 | . . . 4
⊢
Ⅎ𝑥(𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) | 
| 30 | 29 | dffn5f 6979 | . . 3
⊢ ((𝑌 Σg
(𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) Fn 𝐼 ↔ (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥))) | 
| 31 | 23, 30 | sylib 218 | . 2
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥))) | 
| 32 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) | 
| 33 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐼 ↦ 𝑈) = (𝑥 ∈ 𝐼 ↦ 𝑈) | 
| 34 | 33 | fvmpt2 7026 | . . . . . . 7
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑈 ∈ 𝐵) → ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥) = 𝑈) | 
| 35 | 32, 12, 34 | syl2an2r 685 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥) = 𝑈) | 
| 36 | 35 | mpteq2dva 5241 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐽 ↦ ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥)) = (𝑦 ∈ 𝐽 ↦ 𝑈)) | 
| 37 | 36 | oveq2d 7448 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) | 
| 38 | 9 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑌 ∈ CMnd) | 
| 39 |  | cmnmnd 19816 | . . . . . 6
⊢ (𝑅 ∈ CMnd → 𝑅 ∈ Mnd) | 
| 40 | 5, 39 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Mnd) | 
| 41 | 10 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐽 ∈ 𝑊) | 
| 42 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑉) | 
| 43 | 3 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑋) | 
| 44 | 40 | fmpttd 7134 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑅):𝐼⟶Mnd) | 
| 45 | 44 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∈ 𝐼 ↦ 𝑅):𝐼⟶Mnd) | 
| 46 | 1, 2, 42, 43, 45, 32 | prdspjmhm 18843 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (Base‘𝑌) ↦ (𝑎‘𝑥)) ∈ (𝑌 MndHom ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑥))) | 
| 47 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 ↦ 𝑅) = (𝑥 ∈ 𝐼 ↦ 𝑅) | 
| 48 | 47 | fvmpt2 7026 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑅 ∈ CMnd) → ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑥) = 𝑅) | 
| 49 | 32, 5, 48 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑥) = 𝑅) | 
| 50 | 49 | oveq2d 7448 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑌 MndHom ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑥)) = (𝑌 MndHom 𝑅)) | 
| 51 | 46, 50 | eleqtrd 2842 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (Base‘𝑌) ↦ (𝑎‘𝑥)) ∈ (𝑌 MndHom 𝑅)) | 
| 52 | 19 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝐼 ↦ 𝑈) ∈ (Base‘𝑌)) | 
| 53 | 21 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 ) | 
| 54 |  | fveq1 6904 | . . . . 5
⊢ (𝑎 = (𝑥 ∈ 𝐼 ↦ 𝑈) → (𝑎‘𝑥) = ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥)) | 
| 55 |  | fveq1 6904 | . . . . 5
⊢ (𝑎 = (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) → (𝑎‘𝑥) = ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥)) | 
| 56 | 2, 8, 38, 40, 41, 51, 52, 53, 54, 55 | gsummhm2 19958 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥))) = ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥)) | 
| 57 | 37, 56 | eqtr3d 2778 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)) = ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥)) | 
| 58 | 57 | mpteq2dva 5241 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥))) | 
| 59 | 31, 58 | eqtr4d 2779 | 1
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |