Proof of Theorem gsummpt2d
Step | Hyp | Ref
| Expression |
1 | | gsummpt2d.b |
. . 3
⊢ 𝐵 = (Base‘𝑊) |
2 | | eqid 2825 |
. . 3
⊢
(0g‘𝑊) = (0g‘𝑊) |
3 | | gsummpt2d.m |
. . 3
⊢ (𝜑 → 𝑊 ∈ CMnd) |
4 | | gsummpt2d.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
5 | 4 | dmexd 7365 |
. . 3
⊢ (𝜑 → dom 𝐴 ∈ V) |
6 | | gsummpt2d.3 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) |
7 | | gsummpt2d.r |
. . . 4
⊢ (𝜑 → Rel 𝐴) |
8 | | 1stdm 7482 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴) |
9 | 7, 8 | sylan 575 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴) |
10 | | fo1st 7453 |
. . . . . 6
⊢
1st :V–onto→V |
11 | | fofn 6359 |
. . . . . 6
⊢
(1st :V–onto→V → 1st Fn V) |
12 | | dffn5 6492 |
. . . . . . 7
⊢
(1st Fn V ↔ 1st = (𝑥 ∈ V ↦ (1st
‘𝑥))) |
13 | 12 | biimpi 208 |
. . . . . 6
⊢
(1st Fn V → 1st = (𝑥 ∈ V ↦ (1st
‘𝑥))) |
14 | 10, 11, 13 | mp2b 10 |
. . . . 5
⊢
1st = (𝑥
∈ V ↦ (1st ‘𝑥)) |
15 | 14 | reseq1i 5629 |
. . . 4
⊢
(1st ↾ 𝐴) = ((𝑥 ∈ V ↦ (1st
‘𝑥)) ↾ 𝐴) |
16 | | ssv 3850 |
. . . . 5
⊢ 𝐴 ⊆ V |
17 | | resmpt 5690 |
. . . . 5
⊢ (𝐴 ⊆ V → ((𝑥 ∈ V ↦
(1st ‘𝑥))
↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥))) |
18 | 16, 17 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ V ↦
(1st ‘𝑥))
↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥)) |
19 | 15, 18 | eqtri 2849 |
. . 3
⊢
(1st ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥)) |
20 | 1, 2, 3, 4, 5, 6, 9, 19 | gsummpt2co 30321 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))))) |
21 | | gsummpt2d.0 |
. . . 4
⊢
Ⅎ𝑦𝜑 |
22 | 3 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → 𝑊 ∈ CMnd) |
23 | 4 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → 𝐴 ∈ Fin) |
24 | | imaexg 7370 |
. . . . . . 7
⊢ (𝐴 ∈ Fin → (𝐴 “ {𝑦}) ∈ V) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝐴 “ {𝑦}) ∈ V) |
26 | | gsummpt2d.1 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑦, 𝑧〉 → 𝐶 = 𝐷) |
27 | 26 | adantl 475 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝐶 = 𝐷) |
28 | | simp-4l 801 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝜑) |
29 | | simplr 785 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝑥 ∈ 𝐴) |
30 | 28, 29, 6 | syl2anc 579 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝐶 ∈ 𝐵) |
31 | 27, 30 | eqeltrrd 2907 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝐷 ∈ 𝐵) |
32 | | vex 3417 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
33 | | vex 3417 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
34 | 32, 33 | elimasn 5735 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐴 “ {𝑦}) ↔ 〈𝑦, 𝑧〉 ∈ 𝐴) |
35 | 34 | biimpi 208 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴 “ {𝑦}) → 〈𝑦, 𝑧〉 ∈ 𝐴) |
36 | 35 | adantl 475 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → 〈𝑦, 𝑧〉 ∈ 𝐴) |
37 | | simpr 479 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝑥 = 〈𝑦, 𝑧〉) |
38 | 37 | eqeq1d 2827 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 = 〈𝑦, 𝑧〉) → (𝑥 = 〈𝑦, 𝑧〉 ↔ 〈𝑦, 𝑧〉 = 〈𝑦, 𝑧〉)) |
39 | | eqidd 2826 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → 〈𝑦, 𝑧〉 = 〈𝑦, 𝑧〉) |
40 | 36, 38, 39 | rspcedvd 3533 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → ∃𝑥 ∈ 𝐴 𝑥 = 〈𝑦, 𝑧〉) |
41 | 31, 40 | r19.29a 3288 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → 𝐷 ∈ 𝐵) |
42 | 41 | fmpttd 6639 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷):(𝐴 “ {𝑦})⟶𝐵) |
43 | | eqid 2825 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) = (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) |
44 | | imafi2 30033 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin → (𝐴 “ {𝑦}) ∈ Fin) |
45 | 4, 44 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 “ {𝑦}) ∈ Fin) |
46 | 45 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝐴 “ {𝑦}) ∈ Fin) |
47 | | fvex 6450 |
. . . . . . . 8
⊢
(0g‘𝑊) ∈ V |
48 | 47 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (0g‘𝑊) ∈ V) |
49 | 43, 46, 41, 48 | fsuppmptdm 8561 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) finSupp (0g‘𝑊)) |
50 | | 2ndconst 7535 |
. . . . . . . 8
⊢ (𝑦 ∈ dom 𝐴 → (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦})) |
51 | 50 | adantl 475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦})) |
52 | | 1stpreimas 30027 |
. . . . . . . . . 10
⊢ ((Rel
𝐴 ∧ 𝑦 ∈ dom 𝐴) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦}))) |
53 | 7, 52 | sylan 575 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦}))) |
54 | 53 | reseq2d 5633 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (2nd ↾ ({𝑦} × (𝐴 “ {𝑦})))) |
55 | | f1oeq1 6371 |
. . . . . . . 8
⊢
((2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))) → ((2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}) ↔ (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}))) |
56 | 54, 55 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}) ↔ (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}))) |
57 | 51, 56 | mpbird 249 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦})) |
58 | 1, 2, 22, 25, 42, 49, 57 | gsumf1o 18677 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)) = (𝑊 Σg ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦}))))) |
59 | | simpr 479 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) |
60 | 53 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦}))) |
61 | 59, 60 | eleqtrd 2908 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → 𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦}))) |
62 | | xp2nd 7466 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑦})) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑦})) |
64 | 63 | ralrimiva 3175 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ∀𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})(2nd ‘𝑥) ∈ (𝐴 “ {𝑦})) |
65 | | fo2nd 7454 |
. . . . . . . . . . . 12
⊢
2nd :V–onto→V |
66 | | fofn 6359 |
. . . . . . . . . . . 12
⊢
(2nd :V–onto→V → 2nd Fn V) |
67 | | dffn5 6492 |
. . . . . . . . . . . . 13
⊢
(2nd Fn V ↔ 2nd = (𝑥 ∈ V ↦ (2nd
‘𝑥))) |
68 | 67 | biimpi 208 |
. . . . . . . . . . . 12
⊢
(2nd Fn V → 2nd = (𝑥 ∈ V ↦ (2nd
‘𝑥))) |
69 | 65, 66, 68 | mp2b 10 |
. . . . . . . . . . 11
⊢
2nd = (𝑥
∈ V ↦ (2nd ‘𝑥)) |
70 | 69 | reseq1i 5629 |
. . . . . . . . . 10
⊢
(2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = ((𝑥 ∈ V ↦ (2nd
‘𝑥)) ↾ (◡(1st ↾ 𝐴) “ {𝑦})) |
71 | | ssv 3850 |
. . . . . . . . . . 11
⊢ (◡(1st ↾ 𝐴) “ {𝑦}) ⊆ V |
72 | | resmpt 5690 |
. . . . . . . . . . 11
⊢ ((◡(1st ↾ 𝐴) “ {𝑦}) ⊆ V → ((𝑥 ∈ V ↦ (2nd
‘𝑥)) ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥))) |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ↦
(2nd ‘𝑥))
↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥)) |
74 | 70, 73 | eqtri 2849 |
. . . . . . . . 9
⊢
(2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥)) |
75 | 74 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥))) |
76 | | eqidd 2826 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) = (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)) |
77 | 64, 75, 76 | fmptcos 6653 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦}))) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ ⦋(2nd
‘𝑥) / 𝑧⦌𝐷)) |
78 | | nfv 2013 |
. . . . . . . . 9
⊢
Ⅎ𝑧((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) |
79 | | gsummpt2d.c |
. . . . . . . . . 10
⊢
Ⅎ𝑧𝐶 |
80 | 79 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → Ⅎ𝑧𝐶) |
81 | 61 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦}))) |
82 | | xp1st 7465 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) → (1st ‘𝑥) ∈ {𝑦}) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (1st ‘𝑥) ∈ {𝑦}) |
84 | | fvex 6450 |
. . . . . . . . . . . . . 14
⊢
(1st ‘𝑥) ∈ V |
85 | 84 | elsn 4414 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑥) ∈ {𝑦} ↔ (1st ‘𝑥) = 𝑦) |
86 | 83, 85 | sylib 210 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (1st ‘𝑥) = 𝑦) |
87 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑧 = (2nd ‘𝑥)) |
88 | 87 | eqcomd 2831 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (2nd ‘𝑥) = 𝑧) |
89 | | eqopi 7469 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) ∧ ((1st ‘𝑥) = 𝑦 ∧ (2nd ‘𝑥) = 𝑧)) → 𝑥 = 〈𝑦, 𝑧〉) |
90 | 81, 86, 88, 89 | syl12anc 870 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑥 = 〈𝑦, 𝑧〉) |
91 | 90, 26 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝐶 = 𝐷) |
92 | 91 | eqcomd 2831 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝐷 = 𝐶) |
93 | 78, 80, 63, 92 | csbiedf 3778 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → ⦋(2nd
‘𝑥) / 𝑧⦌𝐷 = 𝐶) |
94 | 93 | mpteq2dva 4969 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ ⦋(2nd
‘𝑥) / 𝑧⦌𝐷) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)) |
95 | 77, 94 | eqtrd 2861 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦}))) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)) |
96 | 95 | oveq2d 6926 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})))) = (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))) |
97 | 58, 96 | eqtr2d 2862 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)) = (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))) |
98 | 21, 97 | mpteq2da 4968 |
. . 3
⊢ (𝜑 → (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))) = (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))) |
99 | 98 | oveq2d 6926 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)))) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))) |
100 | 20, 99 | eqtrd 2861 |
1
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))) |