Step | Hyp | Ref
| Expression |
1 | | gsumzcl.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumzcl.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | gsumzcl.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
4 | 3 | gsumz 17727 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
5 | 1, 2, 4 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
6 | | gsumzf1o.h |
. . . . . . . . 9
⊢ (𝜑 → 𝐻:𝐶–1-1-onto→𝐴) |
7 | | f1of1 6377 |
. . . . . . . . 9
⊢ (𝐻:𝐶–1-1-onto→𝐴 → 𝐻:𝐶–1-1→𝐴) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐻:𝐶–1-1→𝐴) |
9 | | f1dmex 7398 |
. . . . . . . 8
⊢ ((𝐻:𝐶–1-1→𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V) |
10 | 8, 2, 9 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ V) |
11 | 3 | gsumz 17727 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝐶 ∈ V) → (𝐺 Σg
(𝑥 ∈ 𝐶 ↦ 0 )) = 0 ) |
12 | 1, 10, 11 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐶 ↦ 0 )) = 0 ) |
13 | 5, 12 | eqtr4d 2864 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = (𝐺 Σg (𝑥 ∈ 𝐶 ↦ 0 ))) |
14 | 13 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σg
(𝑘 ∈ 𝐴 ↦ 0 )) = (𝐺 Σg (𝑥 ∈ 𝐶 ↦ 0 ))) |
15 | | gsumzcl.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
16 | 3 | fvexi 6447 |
. . . . . . 7
⊢ 0 ∈
V |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈ V) |
18 | | ssidd 3849 |
. . . . . 6
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
19 | 15, 2, 17, 18 | gsumcllem 18662 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → 𝐹 = (𝑘 ∈ 𝐴 ↦ 0 )) |
20 | 19 | oveq2d 6921 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
21 | | f1of 6378 |
. . . . . . . . 9
⊢ (𝐻:𝐶–1-1-onto→𝐴 → 𝐻:𝐶⟶𝐴) |
22 | 6, 21 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐻:𝐶⟶𝐴) |
23 | 22 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → 𝐻:𝐶⟶𝐴) |
24 | 23 | ffvelrnda 6608 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹 supp 0 ) = ∅) ∧ 𝑥 ∈ 𝐶) → (𝐻‘𝑥) ∈ 𝐴) |
25 | 23 | feqmptd 6496 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → 𝐻 = (𝑥 ∈ 𝐶 ↦ (𝐻‘𝑥))) |
26 | | eqidd 2826 |
. . . . . 6
⊢ (𝑘 = (𝐻‘𝑥) → 0 = 0 ) |
27 | 24, 25, 19, 26 | fmptco 6646 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐹 ∘ 𝐻) = (𝑥 ∈ 𝐶 ↦ 0 )) |
28 | 27 | oveq2d 6921 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σg
(𝐹 ∘ 𝐻)) = (𝐺 Σg (𝑥 ∈ 𝐶 ↦ 0 ))) |
29 | 14, 20, 28 | 3eqtr4d 2871 |
. . 3
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻))) |
30 | 29 | ex 403 |
. 2
⊢ (𝜑 → ((𝐹 supp 0 ) = ∅ → (𝐺 Σg
𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻)))) |
31 | | coass 5895 |
. . . . . . . . . . 11
⊢ ((𝐻 ∘ ◡𝐻) ∘ 𝑓) = (𝐻 ∘ (◡𝐻 ∘ 𝑓)) |
32 | 6 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐻:𝐶–1-1-onto→𝐴) |
33 | | f1ococnv2 6404 |
. . . . . . . . . . . . . 14
⊢ (𝐻:𝐶–1-1-onto→𝐴 → (𝐻 ∘ ◡𝐻) = ( I ↾ 𝐴)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐻 ∘ ◡𝐻) = ( I ↾ 𝐴)) |
35 | 34 | coeq1d 5516 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ((𝐻 ∘ ◡𝐻) ∘ 𝑓) = (( I ↾ 𝐴) ∘ 𝑓)) |
36 | | f1of1 6377 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 )) |
37 | 36 | ad2antll 720 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 )) |
38 | | suppssdm 7572 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
39 | 38, 15 | fssdm 6294 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴) |
40 | 39 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ 𝐴) |
41 | | f1ss 6343 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 ) ∧ (𝐹 supp 0 ) ⊆ 𝐴) → 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→𝐴) |
42 | 37, 40, 41 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→𝐴) |
43 | | f1f 6338 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→𝐴 → 𝑓:(1...(♯‘(𝐹 supp 0 )))⟶𝐴) |
44 | | fcoi2 6316 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))⟶𝐴 → (( I ↾ 𝐴) ∘ 𝑓) = 𝑓) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (( I ↾
𝐴) ∘ 𝑓) = 𝑓) |
46 | 35, 45 | eqtrd 2861 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ((𝐻 ∘ ◡𝐻) ∘ 𝑓) = 𝑓) |
47 | 31, 46 | syl5reqr 2876 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓 = (𝐻 ∘ (◡𝐻 ∘ 𝑓))) |
48 | 47 | coeq2d 5517 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 ∘ 𝑓) = (𝐹 ∘ (𝐻 ∘ (◡𝐻 ∘ 𝑓)))) |
49 | | coass 5895 |
. . . . . . . . 9
⊢ ((𝐹 ∘ 𝐻) ∘ (◡𝐻 ∘ 𝑓)) = (𝐹 ∘ (𝐻 ∘ (◡𝐻 ∘ 𝑓))) |
50 | 48, 49 | syl6eqr 2879 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 ∘ 𝑓) = ((𝐹 ∘ 𝐻) ∘ (◡𝐻 ∘ 𝑓))) |
51 | 50 | seqeq3d 13103 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) →
seq1((+g‘𝐺), (𝐹 ∘ 𝑓)) = seq1((+g‘𝐺), ((𝐹 ∘ 𝐻) ∘ (◡𝐻 ∘ 𝑓)))) |
52 | 51 | fveq1d 6435 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) →
(seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(𝐹 supp 0 ))) =
(seq1((+g‘𝐺), ((𝐹 ∘ 𝐻) ∘ (◡𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 )))) |
53 | | gsumzcl.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
54 | | eqid 2825 |
. . . . . . 7
⊢
(+g‘𝐺) = (+g‘𝐺) |
55 | | gsumzcl.z |
. . . . . . 7
⊢ 𝑍 = (Cntz‘𝐺) |
56 | 1 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐺 ∈ Mnd) |
57 | 2 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐴 ∈ 𝑉) |
58 | 15 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐹:𝐴⟶𝐵) |
59 | | gsumzcl.c |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
60 | 59 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
61 | | simprl 787 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) →
(♯‘(𝐹 supp
0 ))
∈ ℕ) |
62 | | ssid 3848 |
. . . . . . . 8
⊢ (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ) |
63 | | f1ofo 6385 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → 𝑓:(1...(♯‘(𝐹 supp 0 )))–onto→(𝐹 supp 0 )) |
64 | | forn 6356 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))–onto→(𝐹 supp 0 ) → ran 𝑓 = (𝐹 supp 0 )) |
65 | 63, 64 | syl 17 |
. . . . . . . . 9
⊢ (𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → ran 𝑓 = (𝐹 supp 0 )) |
66 | 65 | ad2antll 720 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran 𝑓 = (𝐹 supp 0 )) |
67 | 62, 66 | syl5sseqr 3879 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ ran 𝑓) |
68 | | eqid 2825 |
. . . . . . 7
⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 ) |
69 | 53, 3, 54, 55, 56, 57, 58, 60, 61, 42, 67, 68 | gsumval3 18661 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σg
𝐹) =
(seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(♯‘(𝐹 supp 0 )))) |
70 | 10 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐶 ∈ V) |
71 | | fco 6295 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐻:𝐶⟶𝐴) → (𝐹 ∘ 𝐻):𝐶⟶𝐵) |
72 | 15, 22, 71 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ 𝐻):𝐶⟶𝐵) |
73 | 72 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 ∘ 𝐻):𝐶⟶𝐵) |
74 | | rncoss 5619 |
. . . . . . . . 9
⊢ ran
(𝐹 ∘ 𝐻) ⊆ ran 𝐹 |
75 | 55 | cntzidss 18120 |
. . . . . . . . 9
⊢ ((ran
𝐹 ⊆ (𝑍‘ran 𝐹) ∧ ran (𝐹 ∘ 𝐻) ⊆ ran 𝐹) → ran (𝐹 ∘ 𝐻) ⊆ (𝑍‘ran (𝐹 ∘ 𝐻))) |
76 | 59, 74, 75 | sylancl 580 |
. . . . . . . 8
⊢ (𝜑 → ran (𝐹 ∘ 𝐻) ⊆ (𝑍‘ran (𝐹 ∘ 𝐻))) |
77 | 76 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran (𝐹 ∘ 𝐻) ⊆ (𝑍‘ran (𝐹 ∘ 𝐻))) |
78 | | f1ocnv 6390 |
. . . . . . . . . 10
⊢ (𝐻:𝐶–1-1-onto→𝐴 → ◡𝐻:𝐴–1-1-onto→𝐶) |
79 | | f1of1 6377 |
. . . . . . . . . 10
⊢ (◡𝐻:𝐴–1-1-onto→𝐶 → ◡𝐻:𝐴–1-1→𝐶) |
80 | 6, 78, 79 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ◡𝐻:𝐴–1-1→𝐶) |
81 | 80 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ◡𝐻:𝐴–1-1→𝐶) |
82 | | f1co 6348 |
. . . . . . . 8
⊢ ((◡𝐻:𝐴–1-1→𝐶 ∧ 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1→𝐴) → (◡𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1→𝐶) |
83 | 81, 42, 82 | syl2anc 579 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (◡𝐻 ∘ 𝑓):(1...(♯‘(𝐹 supp 0 )))–1-1→𝐶) |
84 | | ssidd 3849 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
85 | | fex 6745 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
86 | 15, 2, 85 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ V) |
87 | | suppimacnv 7570 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ (𝐹 supp 0 ) = (◡𝐹 “ (V ∖ { 0 }))) |
88 | 86, 16, 87 | sylancl 580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 supp 0 ) = (◡𝐹 “ (V ∖ { 0 }))) |
89 | 88 | eqcomd 2831 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ (V ∖ { 0 })) = (𝐹 supp 0 )) |
90 | 89 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (◡𝐹 “ (V ∖ { 0 })) = (𝐹 supp 0 )) |
91 | 84, 90, 66 | 3sstr4d 3873 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (◡𝐹 “ (V ∖ { 0 })) ⊆ ran 𝑓) |
92 | | imass2 5742 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ (V ∖ { 0 })) ⊆ ran 𝑓 → (◡𝐻 “ (◡𝐹 “ (V ∖ { 0 }))) ⊆ (◡𝐻 “ ran 𝑓)) |
93 | 91, 92 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (◡𝐻 “ (◡𝐹 “ (V ∖ { 0 }))) ⊆ (◡𝐻 “ ran 𝑓)) |
94 | | cnvco 5540 |
. . . . . . . . . . 11
⊢ ◡(𝐹 ∘ 𝐻) = (◡𝐻 ∘ ◡𝐹) |
95 | 94 | imaeq1i 5704 |
. . . . . . . . . 10
⊢ (◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })) = ((◡𝐻 ∘ ◡𝐹) “ (V ∖ { 0 })) |
96 | | imaco 5881 |
. . . . . . . . . 10
⊢ ((◡𝐻 ∘ ◡𝐹) “ (V ∖ { 0 })) = (◡𝐻 “ (◡𝐹 “ (V ∖ { 0 }))) |
97 | 95, 96 | eqtri 2849 |
. . . . . . . . 9
⊢ (◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })) = (◡𝐻 “ (◡𝐹 “ (V ∖ { 0 }))) |
98 | | rnco2 5883 |
. . . . . . . . 9
⊢ ran
(◡𝐻 ∘ 𝑓) = (◡𝐻 “ ran 𝑓) |
99 | 93, 97, 98 | 3sstr4g 3871 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })) ⊆ ran (◡𝐻 ∘ 𝑓)) |
100 | | f1oexrnex 7377 |
. . . . . . . . . . . . 13
⊢ ((𝐻:𝐶–1-1-onto→𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐻 ∈ V) |
101 | 6, 2, 100 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ V) |
102 | | coexg 7379 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → (𝐹 ∘ 𝐻) ∈ V) |
103 | 86, 101, 102 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ V) |
104 | | suppimacnv 7570 |
. . . . . . . . . . 11
⊢ (((𝐹 ∘ 𝐻) ∈ V ∧ 0 ∈ V) → ((𝐹 ∘ 𝐻) supp 0 ) = (◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 }))) |
105 | 103, 16, 104 | sylancl 580 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐹 ∘ 𝐻) supp 0 ) = (◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 }))) |
106 | 105 | sseq1d 3857 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐹 ∘ 𝐻) supp 0 ) ⊆ ran (◡𝐻 ∘ 𝑓) ↔ (◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })) ⊆ ran (◡𝐻 ∘ 𝑓))) |
107 | 106 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (((𝐹 ∘ 𝐻) supp 0 ) ⊆ ran (◡𝐻 ∘ 𝑓) ↔ (◡(𝐹 ∘ 𝐻) “ (V ∖ { 0 })) ⊆ ran (◡𝐻 ∘ 𝑓))) |
108 | 99, 107 | mpbird 249 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ((𝐹 ∘ 𝐻) supp 0 ) ⊆ ran (◡𝐻 ∘ 𝑓)) |
109 | | eqid 2825 |
. . . . . . 7
⊢ (((𝐹 ∘ 𝐻) ∘ (◡𝐻 ∘ 𝑓)) supp 0 ) = (((𝐹 ∘ 𝐻) ∘ (◡𝐻 ∘ 𝑓)) supp 0 ) |
110 | 53, 3, 54, 55, 56, 70, 73, 77, 61, 83, 108, 109 | gsumval3 18661 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σg
(𝐹 ∘ 𝐻)) =
(seq1((+g‘𝐺), ((𝐹 ∘ 𝐻) ∘ (◡𝐻 ∘ 𝑓)))‘(♯‘(𝐹 supp 0 )))) |
111 | 52, 69, 110 | 3eqtr4d 2871 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻))) |
112 | 111 | expr 450 |
. . . 4
⊢ ((𝜑 ∧ (♯‘(𝐹 supp 0 )) ∈ ℕ) →
(𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻)))) |
113 | 112 | exlimdv 2032 |
. . 3
⊢ ((𝜑 ∧ (♯‘(𝐹 supp 0 )) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻)))) |
114 | 113 | expimpd 447 |
. 2
⊢ (𝜑 → (((♯‘(𝐹 supp 0 )) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻)))) |
115 | | gsumzcl.w |
. . 3
⊢ (𝜑 → 𝐹 finSupp 0 ) |
116 | | fsuppimp 8550 |
. . . 4
⊢ (𝐹 finSupp 0 → (Fun 𝐹 ∧ (𝐹 supp 0 ) ∈
Fin)) |
117 | 116 | simprd 491 |
. . 3
⊢ (𝐹 finSupp 0 → (𝐹 supp 0 ) ∈
Fin) |
118 | | fz1f1o 14818 |
. . 3
⊢ ((𝐹 supp 0 ) ∈ Fin →
((𝐹 supp 0 ) = ∅ ∨
((♯‘(𝐹 supp
0 ))
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )))) |
119 | 115, 117,
118 | 3syl 18 |
. 2
⊢ (𝜑 → ((𝐹 supp 0 ) = ∅ ∨
((♯‘(𝐹 supp
0 ))
∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )))) |
120 | 30, 114, 119 | mpjaod 891 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻))) |