Step | Hyp | Ref
| Expression |
1 | | nfcsb1v 3549 |
. . . 4
⊢
Ⅎ𝑥⦋(2nd ‘𝑝) / 𝑥⦌𝐶 |
2 | | gsummpt2co.b |
. . . 4
⊢ 𝐵 = (Base‘𝑊) |
3 | | gsummpt2co.z |
. . . 4
⊢ 0 =
(0g‘𝑊) |
4 | | csbeq1a 3542 |
. . . 4
⊢ (𝑥 = (2nd ‘𝑝) → 𝐶 = ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) |
5 | | gsummpt2co.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ CMnd) |
6 | | gsummpt2co.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
7 | | ssid 3624 |
. . . . 5
⊢ 𝐵 ⊆ 𝐵 |
8 | 7 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ 𝐵) |
9 | | gsummpt2co.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) |
10 | | elcnv 5299 |
. . . . . 6
⊢ (𝑝 ∈ ◡𝐹 ↔ ∃𝑧∃𝑥(𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧)) |
11 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
12 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
13 | 11, 12 | op2ndd 7179 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑧, 𝑥〉 → (2nd ‘𝑝) = 𝑥) |
14 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → (2nd ‘𝑝) = 𝑥) |
15 | | gsummpt2co.3 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐷) |
16 | 15 | dmmptss 5631 |
. . . . . . . . . 10
⊢ dom 𝐹 ⊆ 𝐴 |
17 | 12, 11 | breldm 5329 |
. . . . . . . . . 10
⊢ (𝑥𝐹𝑧 → 𝑥 ∈ dom 𝐹) |
18 | 16, 17 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝑥𝐹𝑧 → 𝑥 ∈ 𝐴) |
19 | 18 | adantl 482 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → 𝑥 ∈ 𝐴) |
20 | 14, 19 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → (2nd ‘𝑝) ∈ 𝐴) |
21 | 20 | exlimivv 1860 |
. . . . . 6
⊢
(∃𝑧∃𝑥(𝑝 = 〈𝑧, 𝑥〉 ∧ 𝑥𝐹𝑧) → (2nd ‘𝑝) ∈ 𝐴) |
22 | 10, 21 | sylbi 207 |
. . . . 5
⊢ (𝑝 ∈ ◡𝐹 → (2nd ‘𝑝) ∈ 𝐴) |
23 | 22 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ◡𝐹) → (2nd ‘𝑝) ∈ 𝐴) |
24 | 15 | funmpt2 5927 |
. . . . . . 7
⊢ Fun 𝐹 |
25 | | funcnvcnv 5956 |
. . . . . . 7
⊢ (Fun
𝐹 → Fun ◡◡𝐹) |
26 | 24, 25 | ax-mp 5 |
. . . . . 6
⊢ Fun ◡◡𝐹 |
27 | 26 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun ◡◡𝐹) |
28 | | dfdm4 5316 |
. . . . . . . 8
⊢ dom 𝐹 = ran ◡𝐹 |
29 | 15 | dmeqi 5325 |
. . . . . . . . 9
⊢ dom 𝐹 = dom (𝑥 ∈ 𝐴 ↦ 𝐷) |
30 | | gsummpt2co.2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐸) |
31 | 30 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐷 ∈ 𝐸) |
32 | | dmmptg 5632 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 𝐷 ∈ 𝐸 → dom (𝑥 ∈ 𝐴 ↦ 𝐷) = 𝐴) |
33 | 31, 32 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐷) = 𝐴) |
34 | 29, 33 | syl5eq 2668 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐹 = 𝐴) |
35 | 28, 34 | syl5eqr 2670 |
. . . . . . 7
⊢ (𝜑 → ran ◡𝐹 = 𝐴) |
36 | 35 | eleq2d 2687 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ran ◡𝐹 ↔ 𝑥 ∈ 𝐴)) |
37 | 36 | biimpar 502 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ran ◡𝐹) |
38 | | relcnv 5503 |
. . . . . 6
⊢ Rel ◡𝐹 |
39 | | fcnvgreu 29472 |
. . . . . 6
⊢ (((Rel
◡𝐹 ∧ Fun ◡◡𝐹) ∧ 𝑥 ∈ ran ◡𝐹) → ∃!𝑝 ∈ ◡ 𝐹𝑥 = (2nd ‘𝑝)) |
40 | 38, 39 | mpanl1 716 |
. . . . 5
⊢ ((Fun
◡◡𝐹 ∧ 𝑥 ∈ ran ◡𝐹) → ∃!𝑝 ∈ ◡ 𝐹𝑥 = (2nd ‘𝑝)) |
41 | 27, 37, 40 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑝 ∈ ◡ 𝐹𝑥 = (2nd ‘𝑝)) |
42 | 1, 2, 3, 4, 5, 6, 8, 9, 23, 41 | gsummptf1o 18362 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶))) |
43 | 15 | rnmptss 6392 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝐷 ∈ 𝐸 → ran 𝐹 ⊆ 𝐸) |
44 | 31, 43 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ 𝐸) |
45 | | dfcnv2 29476 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ 𝐸 → ◡𝐹 = ∪ 𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧}))) |
46 | 44, 45 | syl 17 |
. . . . . 6
⊢ (𝜑 → ◡𝐹 = ∪ 𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧}))) |
47 | 46 | mpteq1d 4738 |
. . . . 5
⊢ (𝜑 → (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) = (𝑝 ∈ ∪
𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧})) ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶)) |
48 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑧⦋(2nd ‘𝑝) / 𝑥⦌𝐶 |
49 | | csbeq1 3536 |
. . . . . . . 8
⊢
((2nd ‘𝑝) = 𝑥 → ⦋(2nd
‘𝑝) / 𝑥⦌𝐶 = ⦋𝑥 / 𝑥⦌𝐶) |
50 | 13, 49 | syl 17 |
. . . . . . 7
⊢ (𝑝 = 〈𝑧, 𝑥〉 → ⦋(2nd
‘𝑝) / 𝑥⦌𝐶 = ⦋𝑥 / 𝑥⦌𝐶) |
51 | | csbid 3541 |
. . . . . . 7
⊢
⦋𝑥 /
𝑥⦌𝐶 = 𝐶 |
52 | 50, 51 | syl6eq 2672 |
. . . . . 6
⊢ (𝑝 = 〈𝑧, 𝑥〉 → ⦋(2nd
‘𝑝) / 𝑥⦌𝐶 = 𝐶) |
53 | 48, 1, 52 | mpt2mptxf 29477 |
. . . . 5
⊢ (𝑝 ∈ ∪ 𝑧 ∈ 𝐸 ({𝑧} × (◡𝐹 “ {𝑧})) ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) = (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶) |
54 | 47, 53 | syl6eq 2672 |
. . . 4
⊢ (𝜑 → (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶) = (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) |
55 | 54 | oveq2d 6666 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑝 ∈ ◡𝐹 ↦ ⦋(2nd
‘𝑝) / 𝑥⦌𝐶)) = (𝑊 Σg (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))) |
56 | | gsummpt2co.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ 𝑉) |
57 | | mptfi 8265 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin → (𝑥 ∈ 𝐴 ↦ 𝐷) ∈ Fin) |
58 | 15, 57 | syl5eqel 2705 |
. . . . . . 7
⊢ (𝐴 ∈ Fin → 𝐹 ∈ Fin) |
59 | | cnvfi 8248 |
. . . . . . 7
⊢ (𝐹 ∈ Fin → ◡𝐹 ∈ Fin) |
60 | 6, 58, 59 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ◡𝐹 ∈ Fin) |
61 | | imaexg 7103 |
. . . . . 6
⊢ (◡𝐹 ∈ Fin → (◡𝐹 “ {𝑧}) ∈ V) |
62 | 60, 61 | syl 17 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ {𝑧}) ∈ V) |
63 | 62 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐸) → (◡𝐹 “ {𝑧}) ∈ V) |
64 | | simpll 790 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝜑) |
65 | | imassrn 5477 |
. . . . . . . . 9
⊢ (◡𝐹 “ {𝑧}) ⊆ ran ◡𝐹 |
66 | 65, 28 | sseqtr4i 3638 |
. . . . . . . 8
⊢ (◡𝐹 “ {𝑧}) ⊆ dom 𝐹 |
67 | 66, 16 | sstri 3612 |
. . . . . . 7
⊢ (◡𝐹 “ {𝑧}) ⊆ 𝐴 |
68 | 11, 12 | elimasn 5490 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (◡𝐹 “ {𝑧}) ↔ 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
69 | 68 | biimpi 206 |
. . . . . . . . 9
⊢ (𝑥 ∈ (◡𝐹 “ {𝑧}) → 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
70 | 69 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
71 | 70, 68 | sylibr 224 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝑥 ∈ (◡𝐹 “ {𝑧})) |
72 | 67, 71 | sseldi 3601 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝑥 ∈ 𝐴) |
73 | 64, 72, 9 | syl2anc 693 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝐶 ∈ 𝐵) |
74 | 73 | anasss 679 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) → 𝐶 ∈ 𝐵) |
75 | | df-br 4654 |
. . . . . . . . 9
⊢ (𝑧◡𝐹𝑥 ↔ 〈𝑧, 𝑥〉 ∈ ◡𝐹) |
76 | 70, 75 | sylibr 224 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐸) ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) → 𝑧◡𝐹𝑥) |
77 | 76 | anasss 679 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) → 𝑧◡𝐹𝑥) |
78 | 77 | pm2.24d 147 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) → (¬ 𝑧◡𝐹𝑥 → 𝐶 = 0 )) |
79 | 78 | imp 445 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧}))) ∧ ¬ 𝑧◡𝐹𝑥) → 𝐶 = 0 ) |
80 | 79 | anasss 679 |
. . . 4
⊢ ((𝜑 ∧ ((𝑧 ∈ 𝐸 ∧ 𝑥 ∈ (◡𝐹 “ {𝑧})) ∧ ¬ 𝑧◡𝐹𝑥)) → 𝐶 = 0 ) |
81 | 2, 3, 5, 56, 63, 74, 60, 80 | gsum2d2 18373 |
. . 3
⊢ (𝜑 → (𝑊 Σg (𝑧 ∈ 𝐸, 𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) = (𝑊 Σg (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))))) |
82 | 42, 55, 81 | 3eqtrd 2660 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))))) |
83 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑧(𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶)) |
84 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑦(𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) |
85 | | sneq 4187 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → {𝑦} = {𝑧}) |
86 | 85 | imaeq2d 5466 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑧})) |
87 | 86 | mpteq1d 4738 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶) = (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)) |
88 | 87 | oveq2d 6666 |
. . . 4
⊢ (𝑦 = 𝑧 → (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶)) = (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))) |
89 | 83, 84, 88 | cbvmpt 4749 |
. . 3
⊢ (𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶))) = (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶))) |
90 | 89 | oveq2i 6661 |
. 2
⊢ (𝑊 Σg
(𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶)))) = (𝑊 Σg (𝑧 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑧}) ↦ 𝐶)))) |
91 | 82, 90 | syl6eqr 2674 |
1
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶))))) |