| Step | Hyp | Ref
| Expression |
| 1 | | nfcsb1v 3923 |
. . . 4
⊢
Ⅎ𝑥⦋(2nd ‘𝑝) / 𝑥⦌𝐶 |
| 2 | | gsummpt2co.b |
. . . 4
⊢ 𝐵 = (Base‘𝑊) |
| 3 | | gsummpt2co.z |
. . . 4
⊢ 0 =
(0g‘𝑊) |
| 4 | | csbeq1a 3913 |
. . . 4
⊢ (𝑥 = (2nd ‘𝑝) → 𝐶 = ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) |
| 5 | | gsummpt2co.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ CMnd) |
| 6 | | gsummpt2co.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 7 | | ssidd 4007 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ 𝐵) |
| 8 | | gsummpt2co.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) |
| 9 | | elcnv 5887 |
. . . . . 6
⊢ (𝑝 ∈ ◡𝐹 ↔ ∃𝑧∃𝑥(𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧)) |
| 10 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
| 11 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 12 | 10, 11 | op2ndd 8025 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑧, 𝑥〉 → (2nd ‘𝑝) = 𝑥) |
| 13 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → (2nd ‘𝑝) = 𝑥) |
| 14 | | gsummpt2co.3 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐷) |
| 15 | 14 | dmmptss 6261 |
. . . . . . . . . 10
⊢ dom 𝐹 ⊆ 𝐴 |
| 16 | 11, 10 | breldm 5919 |
. . . . . . . . . 10
⊢ (𝑥𝐹𝑧 → 𝑥 ∈ dom 𝐹) |
| 17 | 15, 16 | sselid 3981 |
. . . . . . . . 9
⊢ (𝑥𝐹𝑧 → 𝑥 ∈ 𝐴) |
| 18 | 17 | adantl 481 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → 𝑥 ∈ 𝐴) |
| 19 | 13, 18 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → (2nd ‘𝑝) ∈ 𝐴) |
| 20 | 19 | exlimivv 1932 |
. . . . . 6
⊢
(∃𝑧∃𝑥(𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → (2nd ‘𝑝) ∈ 𝐴) |
| 21 | 9, 20 | sylbi 217 |
. . . . 5
⊢ (𝑝 ∈ ◡𝐹 → (2nd ‘𝑝) ∈ 𝐴) |
| 22 | 21 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ◡𝐹) → (2nd ‘𝑝) ∈ 𝐴) |
| 23 | 14 | funmpt2 6605 |
. . . . . . 7
⊢ Fun 𝐹 |
| 24 | | funcnvcnv 6633 |
. . . . . . 7
⊢ (Fun
𝐹 → Fun ◡◡𝐹) |
| 25 | 23, 24 | ax-mp 5 |
. . . . . 6
⊢ Fun ◡◡𝐹 |
| 26 | 25 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun ◡◡𝐹) |
| 27 | | dfdm4 5906 |
. . . . . . . 8
⊢ dom 𝐹 = ran ◡𝐹 |
| 28 | 14 | dmeqi 5915 |
. . . . . . . . 9
⊢ dom 𝐹 = dom (𝑥 ∈ 𝐴 ↦ 𝐷) |
| 29 | | gsummpt2co.2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐸) |
| 30 | 29 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐷 ∈ 𝐸) |
| 31 | | dmmptg 6262 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 𝐷 ∈ 𝐸 → dom (𝑥 ∈ 𝐴 ↦ 𝐷) = 𝐴) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐷) = 𝐴) |
| 33 | 28, 32 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐹 = 𝐴) |
| 34 | 27, 33 | eqtr3id 2791 |
. . . . . . 7
⊢ (𝜑 → ran ◡𝐹 = 𝐴) |
| 35 | 34 | eleq2d 2827 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ran ◡𝐹 ↔ 𝑥 ∈ 𝐴)) |
| 36 | 35 | biimpar 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ran ◡𝐹) |
| 37 | | relcnv 6122 |
. . . . . 6
⊢ Rel ◡𝐹 |
| 38 | | fcnvgreu 32683 |
. . . . . 6
⊢ (((Rel
◡𝐹 ∧ Fun ◡◡𝐹) ∧ 𝑥 ∈ ran ◡𝐹) → ∃!𝑝 ∈ ◡ 𝐹𝑥 = (2nd ‘𝑝)) |
| 39 | 37, 38 | mpanl1 700 |
. . . . 5
⊢ ((Fun
◡◡𝐹 ∧ 𝑥 ∈ ran ◡𝐹) → ∃!𝑝 ∈ ◡ 𝐹𝑥 = (2nd ‘𝑝)) |
| 40 | 26, 36, 39 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑝 ∈ ◡ 𝐹𝑥 = (2nd ‘𝑝)) |
| 41 | 1, 2, 3, 4, 5, 6, 7, 8, 22, 40 | gsummptf1o 19981 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶))) |
| 42 | 14 | rnmptss 7143 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝐷 ∈ 𝐸 → ran 𝐹 ⊆ 𝐸) |
| 43 | 30, 42 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ 𝐸) |
| 44 | | dfcnv2 32686 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ 𝐸 → ◡𝐹 = ∪ 𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧}))) |
| 45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → ◡𝐹 = ∪ 𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧}))) |
| 46 | 45 | mpteq1d 5237 |
. . . . 5
⊢ (𝜑 → (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) = (𝑝 ∈ ∪
𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧})) ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶)) |
| 47 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑧⦋(2nd ‘𝑝) / 𝑥⦌𝐶 |
| 48 | | csbeq1 3902 |
. . . . . . . 8
⊢
((2nd ‘𝑝) = 𝑥 → ⦋(2nd
‘𝑝) / 𝑥⦌𝐶 = ⦋𝑥 / 𝑥⦌𝐶) |
| 49 | 12, 48 | syl 17 |
. . . . . . 7
⊢ (𝑝 = 〈𝑧, 𝑥〉 → ⦋(2nd
‘𝑝) / 𝑥⦌𝐶 = ⦋𝑥 / 𝑥⦌𝐶) |
| 50 | | csbid 3912 |
. . . . . . 7
⊢
⦋𝑥 /
𝑥⦌𝐶 = 𝐶 |
| 51 | 49, 50 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑝 = 〈𝑧, 𝑥〉 → ⦋(2nd
‘𝑝) / 𝑥⦌𝐶 = 𝐶) |
| 52 | 47, 1, 51 | mpomptxf 32687 |
. . . . 5
⊢ (𝑝 ∈ ∪ 𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧})) ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) = (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶) |
| 53 | 46, 52 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) = (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) |
| 54 | 53 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶)) = (𝑊 Σg (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))) |
| 55 | | gsummpt2co.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ 𝑉) |
| 56 | | mptfi 9391 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin → (𝑥 ∈ 𝐴 ↦ 𝐷) ∈ Fin) |
| 57 | 14, 56 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝐴 ∈ Fin → 𝐹 ∈ Fin) |
| 58 | | cnvfi 9216 |
. . . . . . 7
⊢ (𝐹 ∈ Fin → ◡𝐹 ∈ Fin) |
| 59 | 6, 57, 58 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ◡𝐹 ∈ Fin) |
| 60 | | imaexg 7935 |
. . . . . 6
⊢ (◡𝐹 ∈ Fin → (◡𝐹 “ {𝑧}) ∈ V) |
| 61 | 59, 60 | syl 17 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ {𝑧}) ∈ V) |
| 62 | 61 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐸) → (◡𝐹 “ {𝑧}) ∈ V) |
| 63 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝜑) |
| 64 | | imassrn 6089 |
. . . . . . . . 9
⊢ (◡𝐹 “ {𝑧}) ⊆ ran ◡𝐹 |
| 65 | 64, 27 | sseqtrri 4033 |
. . . . . . . 8
⊢ (◡𝐹 “ {𝑧}) ⊆ dom 𝐹 |
| 66 | 65, 15 | sstri 3993 |
. . . . . . 7
⊢ (◡𝐹 “ {𝑧}) ⊆ 𝐴 |
| 67 | 10, 11 | elimasn 6108 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡𝐹 “ {𝑧}) ↔ 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
| 68 | 67 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡𝐹 “ {𝑧}) → 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
| 69 | 68 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
| 70 | 69, 67 | sylibr 234 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝑥 ∈ (◡𝐹 “ {𝑧})) |
| 71 | 66, 70 | sselid 3981 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝑥 ∈ 𝐴) |
| 72 | 63, 71, 8 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝐶 ∈ 𝐵) |
| 73 | 72 | anasss 466 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) → 𝐶 ∈ 𝐵) |
| 74 | | df-br 5144 |
. . . . . . . . 9
⊢ (𝑧◡𝐹𝑥 ↔ 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
| 75 | 69, 74 | sylibr 234 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝑧◡𝐹𝑥) |
| 76 | 75 | anasss 466 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) → 𝑧◡𝐹𝑥) |
| 77 | 76 | pm2.24d 151 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) → (¬ 𝑧◡𝐹𝑥 → 𝐶 = 0 )) |
| 78 | 77 | imp 406 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) ∧ ¬ 𝑧◡𝐹𝑥) → 𝐶 = 0 ) |
| 79 | 78 | anasss 466 |
. . . 4
⊢ ((𝜑 ∧ ((𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) ∧ ¬ 𝑧◡𝐹𝑥)) → 𝐶 = 0 ) |
| 80 | 2, 3, 5, 55, 62, 73, 59, 79 | gsum2d2 19992 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) = (𝑊 Σg (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))))) |
| 81 | 41, 54, 80 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))))) |
| 82 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑧(𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶)) |
| 83 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑦(𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) |
| 84 | | sneq 4636 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → {𝑦} = {𝑧}) |
| 85 | 84 | imaeq2d 6078 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑧})) |
| 86 | 85 | mpteq1d 5237 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶) = (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) |
| 87 | 86 | oveq2d 7447 |
. . . 4
⊢ (𝑦 = 𝑧 → (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶)) = (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))) |
| 88 | 82, 83, 87 | cbvmpt 5253 |
. . 3
⊢ (𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶))) = (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))) |
| 89 | 88 | oveq2i 7442 |
. 2
⊢ (𝑊 Σg
(𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶)))) = (𝑊 Σg (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)))) |
| 90 | 81, 89 | eqtr4di 2795 |
1
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶))))) |