| Step | Hyp | Ref
| Expression |
| 1 | | gsumhashmul.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 2 | | suppssdm 8202 |
. . . . . . . 8
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
| 3 | 2, 1 | fssdm 6755 |
. . . . . . 7
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴) |
| 4 | 1, 3 | feqresmpt 6978 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 0 )) = (𝑥 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑥))) |
| 5 | 4 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝐺 Σg (𝑥 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑥)))) |
| 6 | | gsumhashmul.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
| 7 | | gsumhashmul.z |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
| 8 | | gsumhashmul.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ CMnd) |
| 9 | | gsumhashmul.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 finSupp 0 ) |
| 10 | | relfsupp 9403 |
. . . . . . . . 9
⊢ Rel
finSupp |
| 11 | 10 | brrelex1i 5741 |
. . . . . . . 8
⊢ (𝐹 finSupp 0 → 𝐹 ∈ V) |
| 12 | 9, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ V) |
| 13 | 1 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐴) |
| 14 | 12, 13 | fndmexd 7926 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
| 15 | | ssidd 4007 |
. . . . . 6
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
| 16 | 6, 7, 8, 14, 1, 15, 9 | gsumres 19931 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐹 supp 0 ))) = (𝐺 Σg 𝐹)) |
| 17 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥(𝐹‘(1st ‘𝑧)) |
| 18 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = (1st ‘𝑧) → (𝐹‘𝑥) = (𝐹‘(1st ‘𝑧))) |
| 19 | 9 | fsuppimpd 9409 |
. . . . . 6
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
| 20 | | ssidd 4007 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ 𝐵) |
| 21 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → 𝐹:𝐴⟶𝐵) |
| 22 | 3 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → 𝑥 ∈ 𝐴) |
| 23 | 21, 22 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → (𝐹‘𝑥) ∈ 𝐵) |
| 24 | 1 | ffund 6740 |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝐹) |
| 25 | | funrel 6583 |
. . . . . . . . 9
⊢ (Fun
𝐹 → Rel 𝐹) |
| 26 | | reldif 5825 |
. . . . . . . . 9
⊢ (Rel
𝐹 → Rel (𝐹 ∖ (V × { 0
}))) |
| 27 | 24, 25, 26 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → Rel (𝐹 ∖ (V × { 0 }))) |
| 28 | | 1stdm 8065 |
. . . . . . . 8
⊢ ((Rel
(𝐹 ∖ (V × {
0 }))
∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) →
(1st ‘𝑧)
∈ dom (𝐹 ∖ (V
× { 0 }))) |
| 29 | 27, 28 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) →
(1st ‘𝑧)
∈ dom (𝐹 ∖ (V
× { 0 }))) |
| 30 | 7 | fvexi 6920 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
| 31 | 30 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ V) |
| 32 | | fressupp 32697 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ V ∧ 0 ∈ V) → (𝐹 ↾ (𝐹 supp 0 )) = (𝐹 ∖ (V × { 0 }))) |
| 33 | 24, 12, 31, 32 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 0 )) = (𝐹 ∖ (V × { 0 }))) |
| 34 | 33 | dmeqd 5916 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝐹 ↾ (𝐹 supp 0 )) = dom (𝐹 ∖ (V × { 0
}))) |
| 35 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ dom 𝐹) |
| 36 | | ssdmres 6031 |
. . . . . . . . . 10
⊢ ((𝐹 supp 0 ) ⊆ dom 𝐹 ↔ dom (𝐹 ↾ (𝐹 supp 0 )) = (𝐹 supp 0 )) |
| 37 | 35, 36 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝐹 ↾ (𝐹 supp 0 )) = (𝐹 supp 0 )) |
| 38 | 34, 37 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝜑 → dom (𝐹 ∖ (V × { 0 })) = (𝐹 supp 0 )) |
| 39 | 38 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → dom (𝐹 ∖ (V × { 0 })) = (𝐹 supp 0 )) |
| 40 | 29, 39 | eleqtrd 2843 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) →
(1st ‘𝑧)
∈ (𝐹 supp 0
)) |
| 41 | 24 | funresd 6609 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun (𝐹 ↾ (𝐹 supp 0 ))) |
| 42 | 41 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → Fun (𝐹 ↾ (𝐹 supp 0 ))) |
| 43 | 37 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ dom (𝐹 ↾ (𝐹 supp 0 )) ↔ 𝑥 ∈ (𝐹 supp 0 ))) |
| 44 | 43 | biimpar 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → 𝑥 ∈ dom (𝐹 ↾ (𝐹 supp 0 ))) |
| 45 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → 𝑥 ∈ (𝐹 supp 0 )) |
| 46 | 45 | fvresd 6926 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = (𝐹‘𝑥)) |
| 47 | | funopfvb 6963 |
. . . . . . . . . . 11
⊢ ((Fun
(𝐹 ↾ (𝐹 supp 0 )) ∧ 𝑥 ∈ dom (𝐹 ↾ (𝐹 supp 0 ))) → (((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = (𝐹‘𝑥) ↔ 〈𝑥, (𝐹‘𝑥)〉 ∈ (𝐹 ↾ (𝐹 supp 0 )))) |
| 48 | 47 | biimpa 476 |
. . . . . . . . . 10
⊢ (((Fun
(𝐹 ↾ (𝐹 supp 0 )) ∧ 𝑥 ∈ dom (𝐹 ↾ (𝐹 supp 0 ))) ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = (𝐹‘𝑥)) → 〈𝑥, (𝐹‘𝑥)〉 ∈ (𝐹 ↾ (𝐹 supp 0 ))) |
| 49 | 42, 44, 46, 48 | syl21anc 838 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → 〈𝑥, (𝐹‘𝑥)〉 ∈ (𝐹 ↾ (𝐹 supp 0 ))) |
| 50 | 33 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → (𝐹 ↾ (𝐹 supp 0 )) = (𝐹 ∖ (V × { 0 }))) |
| 51 | 49, 50 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → 〈𝑥, (𝐹‘𝑥)〉 ∈ (𝐹 ∖ (V × { 0 }))) |
| 52 | | eqeq2 2749 |
. . . . . . . . . . 11
⊢ (𝑣 = 〈𝑥, (𝐹‘𝑥)〉 → (𝑧 = 𝑣 ↔ 𝑧 = 〈𝑥, (𝐹‘𝑥)〉)) |
| 53 | 52 | bibi2d 342 |
. . . . . . . . . 10
⊢ (𝑣 = 〈𝑥, (𝐹‘𝑥)〉 → ((𝑥 = (1st ‘𝑧) ↔ 𝑧 = 𝑣) ↔ (𝑥 = (1st ‘𝑧) ↔ 𝑧 = 〈𝑥, (𝐹‘𝑥)〉))) |
| 54 | 53 | ralbidv 3178 |
. . . . . . . . 9
⊢ (𝑣 = 〈𝑥, (𝐹‘𝑥)〉 → (∀𝑧 ∈ (𝐹 ∖ (V × { 0 }))(𝑥 = (1st ‘𝑧) ↔ 𝑧 = 𝑣) ↔ ∀𝑧 ∈ (𝐹 ∖ (V × { 0 }))(𝑥 = (1st ‘𝑧) ↔ 𝑧 = 〈𝑥, (𝐹‘𝑥)〉))) |
| 55 | 54 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑣 = 〈𝑥, (𝐹‘𝑥)〉) → (∀𝑧 ∈ (𝐹 ∖ (V × { 0 }))(𝑥 = (1st ‘𝑧) ↔ 𝑧 = 𝑣) ↔ ∀𝑧 ∈ (𝐹 ∖ (V × { 0 }))(𝑥 = (1st ‘𝑧) ↔ 𝑧 = 〈𝑥, (𝐹‘𝑥)〉))) |
| 56 | | fvexd 6921 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → (2nd
‘𝑧) ∈
V) |
| 57 | 27 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → Rel (𝐹 ∖ (V × { 0 }))) |
| 58 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) |
| 59 | | 1st2nd 8064 |
. . . . . . . . . . . . . . . . 17
⊢ ((Rel
(𝐹 ∖ (V × {
0 }))
∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) →
𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
| 60 | 57, 58, 59 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 61 | | opeq1 4873 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (1st ‘𝑧) → 〈𝑥, (2nd ‘𝑧)〉 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
| 62 | 61 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 〈𝑥, (2nd ‘𝑧)〉 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
| 63 | 60, 62 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 𝑧 = 〈𝑥, (2nd ‘𝑧)〉) |
| 64 | | difssd 4137 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → (𝐹 ∖ (V × { 0 })) ⊆
𝐹) |
| 65 | 64 | sselda 3983 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → 𝑧 ∈ 𝐹) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 𝑧 ∈ 𝐹) |
| 67 | 63, 66 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 〈𝑥, (2nd ‘𝑧)〉 ∈ 𝐹) |
| 68 | 63, 67 | jca 511 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → (𝑧 = 〈𝑥, (2nd ‘𝑧)〉 ∧ 〈𝑥, (2nd ‘𝑧)〉 ∈ 𝐹)) |
| 69 | | opeq2 4874 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (2nd ‘𝑧) → 〈𝑥, 𝑦〉 = 〈𝑥, (2nd ‘𝑧)〉) |
| 70 | 69 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (2nd ‘𝑧) → (𝑧 = 〈𝑥, 𝑦〉 ↔ 𝑧 = 〈𝑥, (2nd ‘𝑧)〉)) |
| 71 | 69 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (2nd ‘𝑧) → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝑥, (2nd ‘𝑧)〉 ∈ 𝐹)) |
| 72 | 70, 71 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (2nd ‘𝑧) → ((𝑧 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ (𝑧 = 〈𝑥, (2nd ‘𝑧)〉 ∧ 〈𝑥, (2nd ‘𝑧)〉 ∈ 𝐹))) |
| 73 | 56, 68, 72 | spcedv 3598 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹)) |
| 74 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
| 75 | 74 | elsnres 6039 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝐹 ↾ {𝑥}) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹)) |
| 76 | 73, 75 | sylibr 234 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 𝑧 ∈ (𝐹 ↾ {𝑥})) |
| 77 | 13 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 𝐹 Fn 𝐴) |
| 78 | 22 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 𝑥 ∈ 𝐴) |
| 79 | | fnressn 7178 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
| 80 | 77, 78, 79 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
| 81 | 76, 80 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 𝑧 ∈ {〈𝑥, (𝐹‘𝑥)〉}) |
| 82 | | elsni 4643 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {〈𝑥, (𝐹‘𝑥)〉} → 𝑧 = 〈𝑥, (𝐹‘𝑥)〉) |
| 83 | 81, 82 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑥 = (1st ‘𝑧)) → 𝑧 = 〈𝑥, (𝐹‘𝑥)〉) |
| 84 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑧 = 〈𝑥, (𝐹‘𝑥)〉) → 𝑧 = 〈𝑥, (𝐹‘𝑥)〉) |
| 85 | 84 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑧 = 〈𝑥, (𝐹‘𝑥)〉) → (1st ‘𝑧) = (1st
‘〈𝑥, (𝐹‘𝑥)〉)) |
| 86 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑥) ∈ V |
| 87 | 74, 86 | op1st 8022 |
. . . . . . . . . . 11
⊢
(1st ‘〈𝑥, (𝐹‘𝑥)〉) = 𝑥 |
| 88 | 85, 87 | eqtr2di 2794 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑧 = 〈𝑥, (𝐹‘𝑥)〉) → 𝑥 = (1st ‘𝑧)) |
| 89 | 83, 88 | impbida 801 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → (𝑥 = (1st ‘𝑧) ↔ 𝑧 = 〈𝑥, (𝐹‘𝑥)〉)) |
| 90 | 89 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → ∀𝑧 ∈ (𝐹 ∖ (V × { 0 }))(𝑥 = (1st ‘𝑧) ↔ 𝑧 = 〈𝑥, (𝐹‘𝑥)〉)) |
| 91 | 51, 55, 90 | rspcedvd 3624 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → ∃𝑣 ∈ (𝐹 ∖ (V × { 0 }))∀𝑧 ∈ (𝐹 ∖ (V × { 0 }))(𝑥 = (1st ‘𝑧) ↔ 𝑧 = 𝑣)) |
| 92 | | reu6 3732 |
. . . . . . 7
⊢
(∃!𝑧 ∈
(𝐹 ∖ (V × {
0
}))𝑥 = (1st
‘𝑧) ↔
∃𝑣 ∈ (𝐹 ∖ (V × { 0
}))∀𝑧 ∈ (𝐹 ∖ (V × { 0 }))(𝑥 = (1st ‘𝑧) ↔ 𝑧 = 𝑣)) |
| 93 | 91, 92 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 supp 0 )) → ∃!𝑧 ∈ (𝐹 ∖ (V × { 0 }))𝑥 = (1st ‘𝑧)) |
| 94 | 17, 6, 7, 18, 8, 19, 20, 23, 40, 93 | gsummptf1o 19981 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (𝐹 supp 0 ) ↦ (𝐹‘𝑥))) = (𝐺 Σg (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ↦ (𝐹‘(1st
‘𝑧))))) |
| 95 | 5, 16, 94 | 3eqtr3d 2785 |
. . . 4
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ↦ (𝐹‘(1st
‘𝑧))))) |
| 96 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) |
| 97 | 96 | eldifad 3963 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → 𝑧 ∈ 𝐹) |
| 98 | | funfv1st2nd 8071 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑧 ∈ 𝐹) → (𝐹‘(1st ‘𝑧)) = (2nd
‘𝑧)) |
| 99 | 24, 97, 98 | syl2an2r 685 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → (𝐹‘(1st
‘𝑧)) =
(2nd ‘𝑧)) |
| 100 | 99 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ↦ (𝐹‘(1st
‘𝑧))) = (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ↦
(2nd ‘𝑧))) |
| 101 | 100 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ↦ (𝐹‘(1st
‘𝑧)))) = (𝐺 Σg
(𝑧 ∈ (𝐹 ∖ (V × { 0 })) ↦
(2nd ‘𝑧)))) |
| 102 | 95, 101 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ↦
(2nd ‘𝑧)))) |
| 103 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑧(1st ‘𝑡) |
| 104 | | fvex 6919 |
. . . . 5
⊢
(2nd ‘𝑡) ∈ V |
| 105 | | fvex 6919 |
. . . . 5
⊢
(1st ‘𝑡) ∈ V |
| 106 | 104, 105 | op2ndd 8025 |
. . . 4
⊢ (𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉 →
(2nd ‘𝑧) =
(1st ‘𝑡)) |
| 107 | | resfnfinfin 9377 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ (𝐹 supp 0 ) ∈ Fin) →
(𝐹 ↾ (𝐹 supp 0 )) ∈
Fin) |
| 108 | 13, 19, 107 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐹 supp 0 )) ∈
Fin) |
| 109 | 33, 108 | eqeltrrd 2842 |
. . . 4
⊢ (𝜑 → (𝐹 ∖ (V × { 0 })) ∈
Fin) |
| 110 | 33 | rneqd 5949 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ↾ (𝐹 supp 0 )) = ran (𝐹 ∖ (V × { 0
}))) |
| 111 | | rnresss 6035 |
. . . . . 6
⊢ ran
(𝐹 ↾ (𝐹 supp 0 )) ⊆ ran 𝐹 |
| 112 | 1 | frnd 6744 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ⊆ 𝐵) |
| 113 | 111, 112 | sstrid 3995 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ↾ (𝐹 supp 0 )) ⊆ 𝐵) |
| 114 | 110, 113 | eqsstrrd 4019 |
. . . 4
⊢ (𝜑 → ran (𝐹 ∖ (V × { 0 })) ⊆ 𝐵) |
| 115 | | 2ndrn 8066 |
. . . . 5
⊢ ((Rel
(𝐹 ∖ (V × {
0 }))
∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) →
(2nd ‘𝑧)
∈ ran (𝐹 ∖ (V
× { 0 }))) |
| 116 | 27, 115 | sylan 580 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) →
(2nd ‘𝑧)
∈ ran (𝐹 ∖ (V
× { 0 }))) |
| 117 | | relcnv 6122 |
. . . . . . . 8
⊢ Rel ◡𝐹 |
| 118 | | reldif 5825 |
. . . . . . . 8
⊢ (Rel
◡𝐹 → Rel (◡𝐹 ∖ ({ 0 } ×
V))) |
| 119 | 117, 118 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → Rel (◡𝐹 ∖ ({ 0 } ×
V))) |
| 120 | | 1st2nd 8064 |
. . . . . . 7
⊢ ((Rel
(◡𝐹 ∖ ({ 0 } × V)) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) →
𝑡 = 〈(1st
‘𝑡), (2nd
‘𝑡)〉) |
| 121 | 119, 120 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) →
𝑡 = 〈(1st
‘𝑡), (2nd
‘𝑡)〉) |
| 122 | | cnvdif 6163 |
. . . . . . . . . 10
⊢ ◡(𝐹 ∖ (V × { 0 })) = (◡𝐹 ∖ ◡(V × { 0 })) |
| 123 | | cnvxp 6177 |
. . . . . . . . . . 11
⊢ ◡(V × { 0 }) = ({ 0 } ×
V) |
| 124 | 123 | difeq2i 4123 |
. . . . . . . . . 10
⊢ (◡𝐹 ∖ ◡(V × { 0 })) = (◡𝐹 ∖ ({ 0 } ×
V)) |
| 125 | 122, 124 | eqtri 2765 |
. . . . . . . . 9
⊢ ◡(𝐹 ∖ (V × { 0 })) = (◡𝐹 ∖ ({ 0 } ×
V)) |
| 126 | 125 | eqimss2i 4045 |
. . . . . . . 8
⊢ (◡𝐹 ∖ ({ 0 } × V)) ⊆
◡(𝐹 ∖ (V × { 0 })) |
| 127 | 126 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 ∖ ({ 0 } × V)) ⊆
◡(𝐹 ∖ (V × { 0 }))) |
| 128 | 127 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) →
𝑡 ∈ ◡(𝐹 ∖ (V × { 0 }))) |
| 129 | 121, 128 | eqeltrrd 2842 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) →
〈(1st ‘𝑡), (2nd ‘𝑡)〉 ∈ ◡(𝐹 ∖ (V × { 0 }))) |
| 130 | 105, 104 | opelcnv 5892 |
. . . . 5
⊢
(〈(1st ‘𝑡), (2nd ‘𝑡)〉 ∈ ◡(𝐹 ∖ (V × { 0 })) ↔
〈(2nd ‘𝑡), (1st ‘𝑡)〉 ∈ (𝐹 ∖ (V × { 0 }))) |
| 131 | 129, 130 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) →
〈(2nd ‘𝑡), (1st ‘𝑡)〉 ∈ (𝐹 ∖ (V × { 0 }))) |
| 132 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → Rel (𝐹 ∖ (V × { 0
}))) |
| 133 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → ∪ ◡{𝑧} = ∪
◡{𝑧}) |
| 134 | | cnvf1olem 8135 |
. . . . . . . . 9
⊢ ((Rel
(𝐹 ∖ (V × {
0 }))
∧ (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ∧
∪ ◡{𝑧} = ∪
◡{𝑧})) → (∪
◡{𝑧} ∈ ◡(𝐹 ∖ (V × { 0 })) ∧ 𝑧 = ∪
◡{∪ ◡{𝑧}})) |
| 135 | 134 | simpld 494 |
. . . . . . . 8
⊢ ((Rel
(𝐹 ∖ (V × {
0 }))
∧ (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ∧
∪ ◡{𝑧} = ∪
◡{𝑧})) → ∪ ◡{𝑧} ∈ ◡(𝐹 ∖ (V × { 0 }))) |
| 136 | 132, 96, 133, 135 | syl12anc 837 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → ∪ ◡{𝑧} ∈ ◡(𝐹 ∖ (V × { 0 }))) |
| 137 | 136, 125 | eleqtrdi 2851 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → ∪ ◡{𝑧} ∈ (◡𝐹 ∖ ({ 0 } ×
V))) |
| 138 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (𝑢 = ∪
◡{𝑧} → (𝑡 = 𝑢 ↔ 𝑡 = ∪ ◡{𝑧})) |
| 139 | 138 | bibi2d 342 |
. . . . . . . 8
⊢ (𝑢 = ∪
◡{𝑧} → ((𝑧 = 〈(2nd ‘𝑡), (1st ‘𝑡)〉 ↔ 𝑡 = 𝑢) ↔ (𝑧 = 〈(2nd ‘𝑡), (1st ‘𝑡)〉 ↔ 𝑡 = ∪
◡{𝑧}))) |
| 140 | 139 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑢 = ∪
◡{𝑧} → (∀𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))(𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉 ↔
𝑡 = 𝑢) ↔ ∀𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))(𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉 ↔
𝑡 = ∪ ◡{𝑧}))) |
| 141 | 140 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑢 = ∪
◡{𝑧}) → (∀𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))(𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉 ↔
𝑡 = 𝑢) ↔ ∀𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))(𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉 ↔
𝑡 = ∪ ◡{𝑧}))) |
| 142 | 117, 118 | mp1i 13 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) → Rel
(◡𝐹 ∖ ({ 0 } ×
V))) |
| 143 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) →
𝑡 ∈ (◡𝐹 ∖ ({ 0 } ×
V))) |
| 144 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) →
𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) |
| 145 | | df-rel 5692 |
. . . . . . . . . . . . . 14
⊢ (Rel
(◡𝐹 ∖ ({ 0 } × V)) ↔
(◡𝐹 ∖ ({ 0 } × V)) ⊆ (V
× V)) |
| 146 | 119, 145 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝐹 ∖ ({ 0 } × V)) ⊆ (V
× V)) |
| 147 | 146 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) →
(◡𝐹 ∖ ({ 0 } × V)) ⊆ (V
× V)) |
| 148 | 147, 143 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) →
𝑡 ∈ (V ×
V)) |
| 149 | | 2nd1st 8063 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (V × V) →
∪ ◡{𝑡} = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) |
| 150 | 148, 149 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) →
∪ ◡{𝑡} = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) |
| 151 | 144, 150 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) →
𝑧 = ∪ ◡{𝑡}) |
| 152 | | cnvf1olem 8135 |
. . . . . . . . . 10
⊢ ((Rel
(◡𝐹 ∖ ({ 0 } × V)) ∧ (𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V)) ∧ 𝑧 = ∪
◡{𝑡})) → (𝑧 ∈ ◡(◡𝐹 ∖ ({ 0 } × V)) ∧ 𝑡 = ∪
◡{𝑧})) |
| 153 | 152 | simprd 495 |
. . . . . . . . 9
⊢ ((Rel
(◡𝐹 ∖ ({ 0 } × V)) ∧ (𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V)) ∧ 𝑧 = ∪
◡{𝑡})) → 𝑡 = ∪ ◡{𝑧}) |
| 154 | 142, 143,
151, 153 | syl12anc 837 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) →
𝑡 = ∪ ◡{𝑧}) |
| 155 | 27 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑡 = ∪
◡{𝑧}) → Rel (𝐹 ∖ (V × { 0 }))) |
| 156 | 96 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑡 = ∪
◡{𝑧}) → 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) |
| 157 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑡 = ∪
◡{𝑧}) → 𝑡 = ∪ ◡{𝑧}) |
| 158 | | cnvf1olem 8135 |
. . . . . . . . . . 11
⊢ ((Rel
(𝐹 ∖ (V × {
0 }))
∧ (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ∧
𝑡 = ∪ ◡{𝑧})) → (𝑡 ∈ ◡(𝐹 ∖ (V × { 0 })) ∧ 𝑧 = ∪
◡{𝑡})) |
| 159 | 158 | simprd 495 |
. . . . . . . . . 10
⊢ ((Rel
(𝐹 ∖ (V × {
0 }))
∧ (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ∧
𝑡 = ∪ ◡{𝑧})) → 𝑧 = ∪ ◡{𝑡}) |
| 160 | 155, 156,
157, 159 | syl12anc 837 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑡 = ∪
◡{𝑧}) → 𝑧 = ∪ ◡{𝑡}) |
| 161 | 146 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑡 = ∪
◡{𝑧}) → (◡𝐹 ∖ ({ 0 } × V)) ⊆ (V
× V)) |
| 162 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑡 = ∪
◡{𝑧}) → 𝑡 ∈ (◡𝐹 ∖ ({ 0 } ×
V))) |
| 163 | 161, 162 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑡 = ∪
◡{𝑧}) → 𝑡 ∈ (V × V)) |
| 164 | 163, 149 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑡 = ∪
◡{𝑧}) → ∪ ◡{𝑡} = 〈(2nd ‘𝑡), (1st ‘𝑡)〉) |
| 165 | 160, 164 | eqtrd 2777 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) ∧ 𝑡 = ∪
◡{𝑧}) → 𝑧 = 〈(2nd ‘𝑡), (1st ‘𝑡)〉) |
| 166 | 154, 165 | impbida 801 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) ∧ 𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))) →
(𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉 ↔
𝑡 = ∪ ◡{𝑧})) |
| 167 | 166 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → ∀𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))(𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉 ↔
𝑡 = ∪ ◡{𝑧})) |
| 168 | 137, 141,
167 | rspcedvd 3624 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → ∃𝑢 ∈ (◡𝐹 ∖ ({ 0 } × V))∀𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))(𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉 ↔
𝑡 = 𝑢)) |
| 169 | | reu6 3732 |
. . . . 5
⊢
(∃!𝑡 ∈
(◡𝐹 ∖ ({ 0 } × V))𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉 ↔
∃𝑢 ∈ (◡𝐹 ∖ ({ 0 } × V))∀𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))(𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉 ↔
𝑡 = 𝑢)) |
| 170 | 168, 169 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐹 ∖ (V × { 0 }))) → ∃!𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V))𝑧 = 〈(2nd
‘𝑡), (1st
‘𝑡)〉) |
| 171 | 103, 6, 7, 106, 8, 109, 114, 116, 131, 170 | gsummptf1o 19981 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑧 ∈ (𝐹 ∖ (V × { 0 })) ↦
(2nd ‘𝑧)))
= (𝐺
Σg (𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V)) ↦
(1st ‘𝑡)))) |
| 172 | | fveq2 6906 |
. . . . . 6
⊢ (𝑡 = 𝑧 → (1st ‘𝑡) = (1st ‘𝑧)) |
| 173 | 172 | cbvmptv 5255 |
. . . . 5
⊢ (𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V)) ↦
(1st ‘𝑡))
= (𝑧 ∈ (◡𝐹 ∖ ({ 0 } × V)) ↦
(1st ‘𝑧)) |
| 174 | 33 | cnveqd 5886 |
. . . . . . 7
⊢ (𝜑 → ◡(𝐹 ↾ (𝐹 supp 0 )) = ◡(𝐹 ∖ (V × { 0 }))) |
| 175 | 174, 125 | eqtr2di 2794 |
. . . . . 6
⊢ (𝜑 → (◡𝐹 ∖ ({ 0 } × V)) = ◡(𝐹 ↾ (𝐹 supp 0 ))) |
| 176 | 175 | mpteq1d 5237 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ (◡𝐹 ∖ ({ 0 } × V)) ↦
(1st ‘𝑧))
= (𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 )) ↦ (1st
‘𝑧))) |
| 177 | 173, 176 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V)) ↦
(1st ‘𝑡))
= (𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 )) ↦ (1st
‘𝑧))) |
| 178 | 177 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑡 ∈ (◡𝐹 ∖ ({ 0 } × V)) ↦
(1st ‘𝑡)))
= (𝐺
Σg (𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 )) ↦ (1st
‘𝑧)))) |
| 179 | 102, 171,
178 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 )) ↦ (1st
‘𝑧)))) |
| 180 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑦(1st ‘𝑧) |
| 181 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑥𝜑 |
| 182 | | vex 3484 |
. . . 4
⊢ 𝑦 ∈ V |
| 183 | 74, 182 | op1std 8024 |
. . 3
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
| 184 | | relcnv 6122 |
. . . 4
⊢ Rel ◡(𝐹 ↾ (𝐹 supp 0 )) |
| 185 | 184 | a1i 11 |
. . 3
⊢ (𝜑 → Rel ◡(𝐹 ↾ (𝐹 supp 0 ))) |
| 186 | | cnvfi 9216 |
. . . 4
⊢ ((𝐹 ↾ (𝐹 supp 0 )) ∈ Fin → ◡(𝐹 ↾ (𝐹 supp 0 )) ∈
Fin) |
| 187 | 108, 186 | syl 17 |
. . 3
⊢ (𝜑 → ◡(𝐹 ↾ (𝐹 supp 0 )) ∈
Fin) |
| 188 | 112 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 ))) → ran 𝐹 ⊆ 𝐵) |
| 189 | 184 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 ))) → Rel ◡(𝐹 ↾ (𝐹 supp 0 ))) |
| 190 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 ))) → 𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 ))) |
| 191 | | 1stdm 8065 |
. . . . . . 7
⊢ ((Rel
◡(𝐹 ↾ (𝐹 supp 0 )) ∧ 𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 ))) → (1st
‘𝑧) ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) |
| 192 | 189, 190,
191 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 ))) → (1st
‘𝑧) ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) |
| 193 | | df-rn 5696 |
. . . . . 6
⊢ ran
(𝐹 ↾ (𝐹 supp 0 )) = dom ◡(𝐹 ↾ (𝐹 supp 0 )) |
| 194 | 192, 193 | eleqtrrdi 2852 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 ))) → (1st
‘𝑧) ∈ ran (𝐹 ↾ (𝐹 supp 0 ))) |
| 195 | 111, 194 | sselid 3981 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 ))) → (1st
‘𝑧) ∈ ran 𝐹) |
| 196 | 188, 195 | sseldd 3984 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 ))) → (1st
‘𝑧) ∈ 𝐵) |
| 197 | 180, 181,
6, 183, 185, 187, 8, 196 | gsummpt2d 33052 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑧 ∈ ◡(𝐹 ↾ (𝐹 supp 0 )) ↦ (1st
‘𝑧))) = (𝐺 Σg
(𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 )) ↦ (𝐺 Σg
(𝑦 ∈ (◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}) ↦ 𝑥))))) |
| 198 | | df-ima 5698 |
. . . . . . 7
⊢ (𝐹 “ (𝐹 supp 0 )) = ran (𝐹 ↾ (𝐹 supp 0 )) |
| 199 | | supppreima 32700 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ V ∧ 0 ∈ V) → (𝐹 supp 0 ) = (◡𝐹 “ (ran 𝐹 ∖ { 0 }))) |
| 200 | 24, 12, 31, 199 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp 0 ) = (◡𝐹 “ (ran 𝐹 ∖ { 0 }))) |
| 201 | 200 | imaeq2d 6078 |
. . . . . . 7
⊢ (𝜑 → (𝐹 “ (𝐹 supp 0 )) = (𝐹 “ (◡𝐹 “ (ran 𝐹 ∖ { 0 })))) |
| 202 | 198, 201 | eqtr3id 2791 |
. . . . . 6
⊢ (𝜑 → ran (𝐹 ↾ (𝐹 supp 0 )) = (𝐹 “ (◡𝐹 “ (ran 𝐹 ∖ { 0 })))) |
| 203 | | funimacnv 6647 |
. . . . . . 7
⊢ (Fun
𝐹 → (𝐹 “ (◡𝐹 “ (ran 𝐹 ∖ { 0 }))) = ((ran 𝐹 ∖ { 0 }) ∩ ran 𝐹)) |
| 204 | 24, 203 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 “ (◡𝐹 “ (ran 𝐹 ∖ { 0 }))) = ((ran 𝐹 ∖ { 0 }) ∩ ran 𝐹)) |
| 205 | | difssd 4137 |
. . . . . . 7
⊢ (𝜑 → (ran 𝐹 ∖ { 0 }) ⊆ ran 𝐹) |
| 206 | | dfss2 3969 |
. . . . . . 7
⊢ ((ran
𝐹 ∖ { 0 }) ⊆
ran 𝐹 ↔ ((ran 𝐹 ∖ { 0 }) ∩ ran 𝐹) = (ran 𝐹 ∖ { 0 })) |
| 207 | 205, 206 | sylib 218 |
. . . . . 6
⊢ (𝜑 → ((ran 𝐹 ∖ { 0 }) ∩ ran 𝐹) = (ran 𝐹 ∖ { 0 })) |
| 208 | 202, 204,
207 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 })) |
| 209 | 193, 208 | eqtr3id 2791 |
. . . 4
⊢ (𝜑 → dom ◡(𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 })) |
| 210 | 8 | cmnmndd 19822 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Mnd) |
| 211 | 210 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → 𝐺 ∈ Mnd) |
| 212 | 108 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → (𝐹 ↾ (𝐹 supp 0 )) ∈
Fin) |
| 213 | | imafi2 32723 |
. . . . . . 7
⊢ (◡(𝐹 ↾ (𝐹 supp 0 )) ∈ Fin →
(◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}) ∈ Fin) |
| 214 | 212, 186,
213 | 3syl 18 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → (◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}) ∈ Fin) |
| 215 | 193, 113 | eqsstrrid 4023 |
. . . . . . 7
⊢ (𝜑 → dom ◡(𝐹 ↾ (𝐹 supp 0 )) ⊆ 𝐵) |
| 216 | 215 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → 𝑥 ∈ 𝐵) |
| 217 | | gsumhashmul.x |
. . . . . . 7
⊢ · =
(.g‘𝐺) |
| 218 | 6, 217 | gsumconst 19952 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}) ∈ Fin ∧ 𝑥 ∈ 𝐵) → (𝐺 Σg (𝑦 ∈ (◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}) ↦ 𝑥)) = ((♯‘(◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥})) · 𝑥)) |
| 219 | 211, 214,
216, 218 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → (𝐺 Σg
(𝑦 ∈ (◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}) ↦ 𝑥)) = ((♯‘(◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥})) · 𝑥)) |
| 220 | | cnvresima 6250 |
. . . . . . . 8
⊢ (◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}) = ((◡𝐹 “ {𝑥}) ∩ (𝐹 supp 0 )) |
| 221 | 209 | eleq2d 2827 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 )) ↔ 𝑥 ∈ (ran 𝐹 ∖ { 0 }))) |
| 222 | 221 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → 𝑥 ∈ (ran 𝐹 ∖ { 0 })) |
| 223 | 222 | snssd 4809 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → {𝑥} ⊆ (ran 𝐹 ∖ { 0 })) |
| 224 | | sspreima 7088 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ {𝑥} ⊆ (ran 𝐹 ∖ { 0 })) → (◡𝐹 “ {𝑥}) ⊆ (◡𝐹 “ (ran 𝐹 ∖ { 0 }))) |
| 225 | 24, 223, 224 | syl2an2r 685 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → (◡𝐹 “ {𝑥}) ⊆ (◡𝐹 “ (ran 𝐹 ∖ { 0 }))) |
| 226 | 200 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → (𝐹 supp 0 ) = (◡𝐹 “ (ran 𝐹 ∖ { 0 }))) |
| 227 | 225, 226 | sseqtrrd 4021 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → (◡𝐹 “ {𝑥}) ⊆ (𝐹 supp 0 )) |
| 228 | | dfss2 3969 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {𝑥}) ⊆ (𝐹 supp 0 ) ↔ ((◡𝐹 “ {𝑥}) ∩ (𝐹 supp 0 )) = (◡𝐹 “ {𝑥})) |
| 229 | 227, 228 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → ((◡𝐹 “ {𝑥}) ∩ (𝐹 supp 0 )) = (◡𝐹 “ {𝑥})) |
| 230 | 220, 229 | eqtr2id 2790 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → (◡𝐹 “ {𝑥}) = (◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥})) |
| 231 | 230 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) →
(♯‘(◡𝐹 “ {𝑥})) = (♯‘(◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}))) |
| 232 | 231 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) →
((♯‘(◡𝐹 “ {𝑥})) · 𝑥) = ((♯‘(◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥})) · 𝑥)) |
| 233 | 219, 232 | eqtr4d 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 ))) → (𝐺 Σg
(𝑦 ∈ (◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}) ↦ 𝑥)) = ((♯‘(◡𝐹 “ {𝑥})) · 𝑥)) |
| 234 | 209, 233 | mpteq12dva 5231 |
. . 3
⊢ (𝜑 → (𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 )) ↦ (𝐺 Σg
(𝑦 ∈ (◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}) ↦ 𝑥))) = (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦
((♯‘(◡𝐹 “ {𝑥})) · 𝑥))) |
| 235 | 234 | oveq2d 7447 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ dom ◡(𝐹 ↾ (𝐹 supp 0 )) ↦ (𝐺 Σg
(𝑦 ∈ (◡(𝐹 ↾ (𝐹 supp 0 )) “ {𝑥}) ↦ 𝑥)))) = (𝐺 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦
((♯‘(◡𝐹 “ {𝑥})) · 𝑥)))) |
| 236 | 179, 197,
235 | 3eqtrd 2781 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦
((♯‘(◡𝐹 “ {𝑥})) · 𝑥)))) |