Proof of Theorem gsummpt2d
Step | Hyp | Ref
| Expression |
1 | | gsummpt2d.b |
. . 3
⊢ 𝐵 = (Base‘𝑊) |
2 | | eqid 2610 |
. . 3
⊢
(0g‘𝑊) = (0g‘𝑊) |
3 | | gsummpt2d.m |
. . 3
⊢ (𝜑 → 𝑊 ∈ CMnd) |
4 | | gsummpt2d.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
5 | | dmexg 6989 |
. . . 4
⊢ (𝐴 ∈ Fin → dom 𝐴 ∈ V) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝐴 ∈ V) |
7 | | gsummpt2d.3 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) |
8 | | gsummpt2d.r |
. . . 4
⊢ (𝜑 → Rel 𝐴) |
9 | | 1stdm 7106 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴) |
10 | 8, 9 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1st ‘𝑥) ∈ dom 𝐴) |
11 | | fo1st 7079 |
. . . . . 6
⊢
1st :V–onto→V |
12 | | fofn 6030 |
. . . . . 6
⊢
(1st :V–onto→V → 1st Fn V) |
13 | | dffn5 6151 |
. . . . . . 7
⊢
(1st Fn V ↔ 1st = (𝑥 ∈ V ↦ (1st
‘𝑥))) |
14 | 13 | biimpi 205 |
. . . . . 6
⊢
(1st Fn V → 1st = (𝑥 ∈ V ↦ (1st
‘𝑥))) |
15 | 11, 12, 14 | mp2b 10 |
. . . . 5
⊢
1st = (𝑥
∈ V ↦ (1st ‘𝑥)) |
16 | 15 | reseq1i 5313 |
. . . 4
⊢
(1st ↾ 𝐴) = ((𝑥 ∈ V ↦ (1st
‘𝑥)) ↾ 𝐴) |
17 | | ssv 3588 |
. . . . 5
⊢ 𝐴 ⊆ V |
18 | | resmpt 5369 |
. . . . 5
⊢ (𝐴 ⊆ V → ((𝑥 ∈ V ↦
(1st ‘𝑥))
↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥))) |
19 | 17, 18 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ V ↦
(1st ‘𝑥))
↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥)) |
20 | 16, 19 | eqtri 2632 |
. . 3
⊢
(1st ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (1st ‘𝑥)) |
21 | 1, 2, 3, 4, 6, 7, 10, 20 | gsummpt2co 29111 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))))) |
22 | | gsummpt2d.0 |
. . . 4
⊢
Ⅎ𝑦𝜑 |
23 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → 𝑊 ∈ CMnd) |
24 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → 𝐴 ∈ Fin) |
25 | | imaexg 6995 |
. . . . . . 7
⊢ (𝐴 ∈ Fin → (𝐴 “ {𝑦}) ∈ V) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝐴 “ {𝑦}) ∈ V) |
27 | | gsummpt2d.1 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑦, 𝑧〉 → 𝐶 = 𝐷) |
28 | 27 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝐶 = 𝐷) |
29 | | simp-4l 802 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝜑) |
30 | | simplr 788 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝑥 ∈ 𝐴) |
31 | 29, 30, 7 | syl2anc 691 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝐶 ∈ 𝐵) |
32 | 28, 31 | eqeltrrd 2689 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝐷 ∈ 𝐵) |
33 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
34 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
35 | 33, 34 | elimasn 5409 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐴 “ {𝑦}) ↔ 〈𝑦, 𝑧〉 ∈ 𝐴) |
36 | 35 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴 “ {𝑦}) → 〈𝑦, 𝑧〉 ∈ 𝐴) |
37 | 36 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → 〈𝑦, 𝑧〉 ∈ 𝐴) |
38 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 = 〈𝑦, 𝑧〉) → 𝑥 = 〈𝑦, 𝑧〉) |
39 | 38 | eqeq1d 2612 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) ∧ 𝑥 = 〈𝑦, 𝑧〉) → (𝑥 = 〈𝑦, 𝑧〉 ↔ 〈𝑦, 𝑧〉 = 〈𝑦, 𝑧〉)) |
40 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → 〈𝑦, 𝑧〉 = 〈𝑦, 𝑧〉) |
41 | 37, 39, 40 | rspcedvd 3289 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → ∃𝑥 ∈ 𝐴 𝑥 = 〈𝑦, 𝑧〉) |
42 | 32, 41 | r19.29a 3060 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑧 ∈ (𝐴 “ {𝑦})) → 𝐷 ∈ 𝐵) |
43 | | eqid 2610 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) = (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) |
44 | 42, 43 | fmptd 6292 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷):(𝐴 “ {𝑦})⟶𝐵) |
45 | | imafi2 28872 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin → (𝐴 “ {𝑦}) ∈ Fin) |
46 | 4, 45 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 “ {𝑦}) ∈ Fin) |
47 | 46 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝐴 “ {𝑦}) ∈ Fin) |
48 | | fvex 6113 |
. . . . . . . 8
⊢
(0g‘𝑊) ∈ V |
49 | 48 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (0g‘𝑊) ∈ V) |
50 | 43, 47, 42, 49 | fsuppmptdm 8169 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) finSupp (0g‘𝑊)) |
51 | | 2ndconst 7153 |
. . . . . . . 8
⊢ (𝑦 ∈ dom 𝐴 → (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦})) |
52 | 51 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦})) |
53 | | 1stpreimas 28866 |
. . . . . . . . . 10
⊢ ((Rel
𝐴 ∧ 𝑦 ∈ dom 𝐴) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦}))) |
54 | 8, 53 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦}))) |
55 | 54 | reseq2d 5317 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (2nd ↾ ({𝑦} × (𝐴 “ {𝑦})))) |
56 | | f1oeq1 6040 |
. . . . . . . 8
⊢
((2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))) → ((2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}) ↔ (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}))) |
57 | 55, 56 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}) ↔ (2nd ↾ ({𝑦} × (𝐴 “ {𝑦}))):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦}))) |
58 | 52, 57 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})):({𝑦} × (𝐴 “ {𝑦}))–1-1-onto→(𝐴 “ {𝑦})) |
59 | 1, 2, 23, 26, 44, 50, 58 | gsumf1o 18140 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)) = (𝑊 Σg ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦}))))) |
60 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) |
61 | 54 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → (◡(1st ↾ 𝐴) “ {𝑦}) = ({𝑦} × (𝐴 “ {𝑦}))) |
62 | 60, 61 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → 𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦}))) |
63 | | xp2nd 7090 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑦})) |
64 | 62, 63 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → (2nd ‘𝑥) ∈ (𝐴 “ {𝑦})) |
65 | 64 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ∀𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})(2nd ‘𝑥) ∈ (𝐴 “ {𝑦})) |
66 | | fo2nd 7080 |
. . . . . . . . . . . 12
⊢
2nd :V–onto→V |
67 | | fofn 6030 |
. . . . . . . . . . . 12
⊢
(2nd :V–onto→V → 2nd Fn V) |
68 | | dffn5 6151 |
. . . . . . . . . . . . 13
⊢
(2nd Fn V ↔ 2nd = (𝑥 ∈ V ↦ (2nd
‘𝑥))) |
69 | 68 | biimpi 205 |
. . . . . . . . . . . 12
⊢
(2nd Fn V → 2nd = (𝑥 ∈ V ↦ (2nd
‘𝑥))) |
70 | 66, 67, 69 | mp2b 10 |
. . . . . . . . . . 11
⊢
2nd = (𝑥
∈ V ↦ (2nd ‘𝑥)) |
71 | 70 | reseq1i 5313 |
. . . . . . . . . 10
⊢
(2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = ((𝑥 ∈ V ↦ (2nd
‘𝑥)) ↾ (◡(1st ↾ 𝐴) “ {𝑦})) |
72 | | ssv 3588 |
. . . . . . . . . . 11
⊢ (◡(1st ↾ 𝐴) “ {𝑦}) ⊆ V |
73 | | resmpt 5369 |
. . . . . . . . . . 11
⊢ ((◡(1st ↾ 𝐴) “ {𝑦}) ⊆ V → ((𝑥 ∈ V ↦ (2nd
‘𝑥)) ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥))) |
74 | 72, 73 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ↦
(2nd ‘𝑥))
↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥)) |
75 | 71, 74 | eqtri 2632 |
. . . . . . . . 9
⊢
(2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥)) |
76 | 75 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ (2nd ‘𝑥))) |
77 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) = (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)) |
78 | 65, 76, 77 | fmptcos 6305 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦}))) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ ⦋(2nd
‘𝑥) / 𝑧⦌𝐷)) |
79 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑧((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) |
80 | | gsummpt2d.c |
. . . . . . . . . 10
⊢
Ⅎ𝑧𝐶 |
81 | 80 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → Ⅎ𝑧𝐶) |
82 | 62 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦}))) |
83 | | xp1st 7089 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) → (1st ‘𝑥) ∈ {𝑦}) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (1st ‘𝑥) ∈ {𝑦}) |
85 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(1st ‘𝑥) ∈ V |
86 | 85 | elsn 4140 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑥) ∈ {𝑦} ↔ (1st ‘𝑥) = 𝑦) |
87 | 84, 86 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (1st ‘𝑥) = 𝑦) |
88 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑧 = (2nd ‘𝑥)) |
89 | 88 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → (2nd ‘𝑥) = 𝑧) |
90 | | eqopi 7093 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ({𝑦} × (𝐴 “ {𝑦})) ∧ ((1st ‘𝑥) = 𝑦 ∧ (2nd ‘𝑥) = 𝑧)) → 𝑥 = 〈𝑦, 𝑧〉) |
91 | 82, 87, 89, 90 | syl12anc 1316 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝑥 = 〈𝑦, 𝑧〉) |
92 | 91, 27 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝐶 = 𝐷) |
93 | 92 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) ∧ 𝑧 = (2nd ‘𝑥)) → 𝐷 = 𝐶) |
94 | 79, 81, 64, 93 | csbiedf 3520 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ dom 𝐴) ∧ 𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦})) → ⦋(2nd
‘𝑥) / 𝑧⦌𝐷 = 𝐶) |
95 | 94 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ ⦋(2nd
‘𝑥) / 𝑧⦌𝐷) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)) |
96 | 78, 95 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦}))) = (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)) |
97 | 96 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg ((𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷) ∘ (2nd ↾ (◡(1st ↾ 𝐴) “ {𝑦})))) = (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))) |
98 | 59, 97 | eqtr2d 2645 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐴) → (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)) = (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))) |
99 | 22, 98 | mpteq2da 4671 |
. . 3
⊢ (𝜑 → (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶))) = (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))) |
100 | 99 | oveq2d 6565 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑥 ∈ (◡(1st ↾ 𝐴) “ {𝑦}) ↦ 𝐶)))) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))) |
101 | 21, 100 | eqtrd 2644 |
1
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))) |