Step | Hyp | Ref
| Expression |
1 | | nfcsb1v 3814 |
. . . 4
⊢
Ⅎ𝑥⦋(2nd ‘𝑝) / 𝑥⦌𝐶 |
2 | | gsummpt2co.b |
. . . 4
⊢ 𝐵 = (Base‘𝑊) |
3 | | gsummpt2co.z |
. . . 4
⊢ 0 =
(0g‘𝑊) |
4 | | csbeq1a 3804 |
. . . 4
⊢ (𝑥 = (2nd ‘𝑝) → 𝐶 = ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) |
5 | | gsummpt2co.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ CMnd) |
6 | | gsummpt2co.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
7 | | ssidd 3900 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ 𝐵) |
8 | | gsummpt2co.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) |
9 | | elcnv 5719 |
. . . . . 6
⊢ (𝑝 ∈ ◡𝐹 ↔ ∃𝑧∃𝑥(𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧)) |
10 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
11 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
12 | 10, 11 | op2ndd 7725 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑧, 𝑥〉 → (2nd ‘𝑝) = 𝑥) |
13 | 12 | adantr 484 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → (2nd ‘𝑝) = 𝑥) |
14 | | gsummpt2co.3 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐷) |
15 | 14 | dmmptss 6073 |
. . . . . . . . . 10
⊢ dom 𝐹 ⊆ 𝐴 |
16 | 11, 10 | breldm 5751 |
. . . . . . . . . 10
⊢ (𝑥𝐹𝑧 → 𝑥 ∈ dom 𝐹) |
17 | 15, 16 | sseldi 3875 |
. . . . . . . . 9
⊢ (𝑥𝐹𝑧 → 𝑥 ∈ 𝐴) |
18 | 17 | adantl 485 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → 𝑥 ∈ 𝐴) |
19 | 13, 18 | eqeltrd 2833 |
. . . . . . 7
⊢ ((𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → (2nd ‘𝑝) ∈ 𝐴) |
20 | 19 | exlimivv 1939 |
. . . . . 6
⊢
(∃𝑧∃𝑥(𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → (2nd ‘𝑝) ∈ 𝐴) |
21 | 9, 20 | sylbi 220 |
. . . . 5
⊢ (𝑝 ∈ ◡𝐹 → (2nd ‘𝑝) ∈ 𝐴) |
22 | 21 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ◡𝐹) → (2nd ‘𝑝) ∈ 𝐴) |
23 | 14 | funmpt2 6378 |
. . . . . . 7
⊢ Fun 𝐹 |
24 | | funcnvcnv 6406 |
. . . . . . 7
⊢ (Fun
𝐹 → Fun ◡◡𝐹) |
25 | 23, 24 | ax-mp 5 |
. . . . . 6
⊢ Fun ◡◡𝐹 |
26 | 25 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun ◡◡𝐹) |
27 | | dfdm4 5738 |
. . . . . . . 8
⊢ dom 𝐹 = ran ◡𝐹 |
28 | 14 | dmeqi 5747 |
. . . . . . . . 9
⊢ dom 𝐹 = dom (𝑥 ∈ 𝐴 ↦ 𝐷) |
29 | | gsummpt2co.2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐸) |
30 | 29 | ralrimiva 3096 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐷 ∈ 𝐸) |
31 | | dmmptg 6074 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 𝐷 ∈ 𝐸 → dom (𝑥 ∈ 𝐴 ↦ 𝐷) = 𝐴) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐷) = 𝐴) |
33 | 28, 32 | syl5eq 2785 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐹 = 𝐴) |
34 | 27, 33 | eqtr3id 2787 |
. . . . . . 7
⊢ (𝜑 → ran ◡𝐹 = 𝐴) |
35 | 34 | eleq2d 2818 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ran ◡𝐹 ↔ 𝑥 ∈ 𝐴)) |
36 | 35 | biimpar 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ran ◡𝐹) |
37 | | relcnv 5941 |
. . . . . 6
⊢ Rel ◡𝐹 |
38 | | fcnvgreu 30585 |
. . . . . 6
⊢ (((Rel
◡𝐹 ∧ Fun ◡◡𝐹) ∧ 𝑥 ∈ ran ◡𝐹) → ∃!𝑝 ∈ ◡ 𝐹𝑥 = (2nd ‘𝑝)) |
39 | 37, 38 | mpanl1 700 |
. . . . 5
⊢ ((Fun
◡◡𝐹 ∧ 𝑥 ∈ ran ◡𝐹) → ∃!𝑝 ∈ ◡ 𝐹𝑥 = (2nd ‘𝑝)) |
40 | 26, 36, 39 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑝 ∈ ◡ 𝐹𝑥 = (2nd ‘𝑝)) |
41 | 1, 2, 3, 4, 5, 6, 7, 8, 22, 40 | gsummptf1o 19202 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶))) |
42 | 14 | rnmptss 6896 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝐷 ∈ 𝐸 → ran 𝐹 ⊆ 𝐸) |
43 | 30, 42 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ 𝐸) |
44 | | dfcnv2 30588 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ 𝐸 → ◡𝐹 = ∪ 𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧}))) |
45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → ◡𝐹 = ∪ 𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧}))) |
46 | 45 | mpteq1d 5119 |
. . . . 5
⊢ (𝜑 → (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) = (𝑝 ∈ ∪
𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧})) ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶)) |
47 | | nfcv 2899 |
. . . . . 6
⊢
Ⅎ𝑧⦋(2nd ‘𝑝) / 𝑥⦌𝐶 |
48 | | csbeq1 3793 |
. . . . . . . 8
⊢
((2nd ‘𝑝) = 𝑥 → ⦋(2nd
‘𝑝) / 𝑥⦌𝐶 = ⦋𝑥 / 𝑥⦌𝐶) |
49 | 12, 48 | syl 17 |
. . . . . . 7
⊢ (𝑝 = 〈𝑧, 𝑥〉 → ⦋(2nd
‘𝑝) / 𝑥⦌𝐶 = ⦋𝑥 / 𝑥⦌𝐶) |
50 | | csbid 3803 |
. . . . . . 7
⊢
⦋𝑥 /
𝑥⦌𝐶 = 𝐶 |
51 | 49, 50 | eqtrdi 2789 |
. . . . . 6
⊢ (𝑝 = 〈𝑧, 𝑥〉 → ⦋(2nd
‘𝑝) / 𝑥⦌𝐶 = 𝐶) |
52 | 47, 1, 51 | mpomptxf 30591 |
. . . . 5
⊢ (𝑝 ∈ ∪ 𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧})) ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) = (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶) |
53 | 46, 52 | eqtrdi 2789 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) = (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) |
54 | 53 | oveq2d 7186 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶)) = (𝑊 Σg (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))) |
55 | | gsummpt2co.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ 𝑉) |
56 | | mptfi 8896 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin → (𝑥 ∈ 𝐴 ↦ 𝐷) ∈ Fin) |
57 | 14, 56 | eqeltrid 2837 |
. . . . . . 7
⊢ (𝐴 ∈ Fin → 𝐹 ∈ Fin) |
58 | | cnvfi 8777 |
. . . . . . 7
⊢ (𝐹 ∈ Fin → ◡𝐹 ∈ Fin) |
59 | 6, 57, 58 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ◡𝐹 ∈ Fin) |
60 | | imaexg 7646 |
. . . . . 6
⊢ (◡𝐹 ∈ Fin → (◡𝐹 “ {𝑧}) ∈ V) |
61 | 59, 60 | syl 17 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ {𝑧}) ∈ V) |
62 | 61 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐸) → (◡𝐹 “ {𝑧}) ∈ V) |
63 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝜑) |
64 | | imassrn 5914 |
. . . . . . . . 9
⊢ (◡𝐹 “ {𝑧}) ⊆ ran ◡𝐹 |
65 | 64, 27 | sseqtrri 3914 |
. . . . . . . 8
⊢ (◡𝐹 “ {𝑧}) ⊆ dom 𝐹 |
66 | 65, 15 | sstri 3886 |
. . . . . . 7
⊢ (◡𝐹 “ {𝑧}) ⊆ 𝐴 |
67 | 10, 11 | elimasn 5928 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡𝐹 “ {𝑧}) ↔ 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
68 | 67 | biimpi 219 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡𝐹 “ {𝑧}) → 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
69 | 68 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
70 | 69, 67 | sylibr 237 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝑥 ∈ (◡𝐹 “ {𝑧})) |
71 | 66, 70 | sseldi 3875 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝑥 ∈ 𝐴) |
72 | 63, 71, 8 | syl2anc 587 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝐶 ∈ 𝐵) |
73 | 72 | anasss 470 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) → 𝐶 ∈ 𝐵) |
74 | | df-br 5031 |
. . . . . . . . 9
⊢ (𝑧◡𝐹𝑥 ↔ 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
75 | 69, 74 | sylibr 237 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝑧◡𝐹𝑥) |
76 | 75 | anasss 470 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) → 𝑧◡𝐹𝑥) |
77 | 76 | pm2.24d 154 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) → (¬ 𝑧◡𝐹𝑥 → 𝐶 = 0 )) |
78 | 77 | imp 410 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) ∧ ¬ 𝑧◡𝐹𝑥) → 𝐶 = 0 ) |
79 | 78 | anasss 470 |
. . . 4
⊢ ((𝜑 ∧ ((𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) ∧ ¬ 𝑧◡𝐹𝑥)) → 𝐶 = 0 ) |
80 | 2, 3, 5, 55, 62, 73, 59, 79 | gsum2d2 19213 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) = (𝑊 Σg (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))))) |
81 | 41, 54, 80 | 3eqtrd 2777 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))))) |
82 | | nfcv 2899 |
. . . 4
⊢
Ⅎ𝑧(𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶)) |
83 | | nfcv 2899 |
. . . 4
⊢
Ⅎ𝑦(𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) |
84 | | sneq 4526 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → {𝑦} = {𝑧}) |
85 | 84 | imaeq2d 5903 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑧})) |
86 | 85 | mpteq1d 5119 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶) = (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) |
87 | 86 | oveq2d 7186 |
. . . 4
⊢ (𝑦 = 𝑧 → (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶)) = (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))) |
88 | 82, 83, 87 | cbvmpt 5131 |
. . 3
⊢ (𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶))) = (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))) |
89 | 88 | oveq2i 7181 |
. 2
⊢ (𝑊 Σg
(𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶)))) = (𝑊 Σg (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)))) |
90 | 81, 89 | eqtr4di 2791 |
1
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶))))) |