Step | Hyp | Ref
| Expression |
1 | | prdsgsum.y |
. . . 4
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) |
2 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑌) =
(Base‘𝑌) |
3 | | prdsgsum.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑋) |
4 | | prdsgsum.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
5 | | prdsgsum.r |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CMnd) |
6 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐼 ↦ 𝑅) = (𝑥 ∈ 𝐼 ↦ 𝑅) |
7 | 5, 6 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑅):𝐼⟶CMnd) |
8 | | ffn 5958 |
. . . . 5
⊢ ((𝑥 ∈ 𝐼 ↦ 𝑅):𝐼⟶CMnd → (𝑥 ∈ 𝐼 ↦ 𝑅) Fn 𝐼) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑅) Fn 𝐼) |
10 | | prdsgsum.z |
. . . . 5
⊢ 0 =
(0g‘𝑌) |
11 | 1, 4, 3, 7 | prdscmnd 18087 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ CMnd) |
12 | | prdsgsum.j |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ 𝑊) |
13 | | prdsgsum.f |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵) |
14 | 13 | anassrs 678 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → 𝑈 ∈ 𝐵) |
15 | 14 | an32s 842 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐽) ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ 𝐵) |
16 | 15 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ∀𝑥 ∈ 𝐼 𝑈 ∈ 𝐵) |
17 | 5 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ CMnd) |
18 | | prdsgsum.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
19 | 1, 2, 3, 4, 17, 18 | prdsbasmpt2 15965 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑈) ∈ (Base‘𝑌) ↔ ∀𝑥 ∈ 𝐼 𝑈 ∈ 𝐵)) |
20 | 19 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐼 ↦ 𝑈) ∈ (Base‘𝑌) ↔ ∀𝑥 ∈ 𝐼 𝑈 ∈ 𝐵)) |
21 | 16, 20 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝐼 ↦ 𝑈) ∈ (Base‘𝑌)) |
22 | | eqid 2610 |
. . . . . 6
⊢ (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) = (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) |
23 | 21, 22 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)):𝐽⟶(Base‘𝑌)) |
24 | | prdsgsum.w |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 ) |
25 | 2, 10, 11, 12, 23, 24 | gsumcl 18139 |
. . . 4
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) ∈ (Base‘𝑌)) |
26 | 1, 2, 3, 4, 9, 25 | prdsbasfn 15954 |
. . 3
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) Fn 𝐼) |
27 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑥𝑌 |
28 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑥
Σg |
29 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥𝐽 |
30 | | nfmpt1 4675 |
. . . . . 6
⊢
Ⅎ𝑥(𝑥 ∈ 𝐼 ↦ 𝑈) |
31 | 29, 30 | nfmpt 4674 |
. . . . 5
⊢
Ⅎ𝑥(𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) |
32 | 27, 28, 31 | nfov 6575 |
. . . 4
⊢
Ⅎ𝑥(𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) |
33 | 32 | dffn5f 6162 |
. . 3
⊢ ((𝑌 Σg
(𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) Fn 𝐼 ↔ (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥))) |
34 | 26, 33 | sylib 207 |
. 2
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥))) |
35 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → 𝑥 ∈ 𝐼) |
37 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐼 ↦ 𝑈) = (𝑥 ∈ 𝐼 ↦ 𝑈) |
38 | 37 | fvmpt2 6200 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑈 ∈ 𝐵) → ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥) = 𝑈) |
39 | 36, 14, 38 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥) = 𝑈) |
40 | 39 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐽 ↦ ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥)) = (𝑦 ∈ 𝐽 ↦ 𝑈)) |
41 | 40 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥))) = (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) |
42 | 11 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑌 ∈ CMnd) |
43 | | cmnmnd 18031 |
. . . . . 6
⊢ (𝑅 ∈ CMnd → 𝑅 ∈ Mnd) |
44 | 5, 43 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Mnd) |
45 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐽 ∈ 𝑊) |
46 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑉) |
47 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑋) |
48 | 44, 6 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑅):𝐼⟶Mnd) |
49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑥 ∈ 𝐼 ↦ 𝑅):𝐼⟶Mnd) |
50 | 1, 2, 46, 47, 49, 35 | prdspjmhm 17190 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (Base‘𝑌) ↦ (𝑎‘𝑥)) ∈ (𝑌 MndHom ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑥))) |
51 | 6 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑅 ∈ CMnd) → ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑥) = 𝑅) |
52 | 35, 5, 51 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑥) = 𝑅) |
53 | 52 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑌 MndHom ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑥)) = (𝑌 MndHom 𝑅)) |
54 | 50, 53 | eleqtrd 2690 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑎 ∈ (Base‘𝑌) ↦ (𝑎‘𝑥)) ∈ (𝑌 MndHom 𝑅)) |
55 | 21 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝐼 ↦ 𝑈) ∈ (Base‘𝑌)) |
56 | 24 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 ) |
57 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑥 ∈ 𝐼 ↦ 𝑈) → (𝑎‘𝑥) = ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥)) |
58 | | fveq1 6102 |
. . . . 5
⊢ (𝑎 = (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) → (𝑎‘𝑥) = ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥)) |
59 | 2, 10, 42, 44, 45, 54, 55, 56, 57, 58 | gsummhm2 18162 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ ((𝑥 ∈ 𝐼 ↦ 𝑈)‘𝑥))) = ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥)) |
60 | 41, 59 | eqtr3d 2646 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)) = ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥)) |
61 | 60 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ ((𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)))‘𝑥))) |
62 | 34, 61 | eqtr4d 2647 |
1
⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |