Step | Hyp | Ref
| Expression |
1 | | gsumzcl.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Mnd) |
2 | | gsumzcl.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | inex1g 4729 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝑊) ∈ V) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∩ 𝑊) ∈ V) |
5 | | gsumzcl.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
6 | 5 | gsumz 17197 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝐴 ∩ 𝑊) ∈ V) → (𝐺 Σg (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) = 0 ) |
7 | 1, 4, 6 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) = 0 ) |
8 | 5 | gsumz 17197 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
9 | 1, 2, 8 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) |
10 | 7, 9 | eqtr4d 2647 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
11 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σg
(𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
12 | | resres 5329 |
. . . . . . . 8
⊢ ((𝐹 ↾ 𝐴) ↾ 𝑊) = (𝐹 ↾ (𝐴 ∩ 𝑊)) |
13 | | gsumzcl.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
14 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
15 | | fnresdm 5914 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
16 | 13, 14, 15 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ↾ 𝐴) = 𝐹) |
17 | 16 | reseq1d 5316 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑊) = (𝐹 ↾ 𝑊)) |
18 | 12, 17 | syl5eqr 2658 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑊)) = (𝐹 ↾ 𝑊)) |
19 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐹 ↾ (𝐴 ∩ 𝑊)) = (𝐹 ↾ 𝑊)) |
20 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(0g‘𝐺) ∈ V |
21 | 5, 20 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 0 ∈
V |
22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ V) |
23 | | ssid 3587 |
. . . . . . . . . 10
⊢ (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ) |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 )) |
25 | 13, 2, 22, 24 | gsumcllem 18132 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → 𝐹 = (𝑘 ∈ 𝐴 ↦ 0 )) |
26 | 25 | reseq1d 5316 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐹 ↾ (𝐴 ∩ 𝑊)) = ((𝑘 ∈ 𝐴 ↦ 0 ) ↾ (𝐴 ∩ 𝑊))) |
27 | | inss1 3795 |
. . . . . . . 8
⊢ (𝐴 ∩ 𝑊) ⊆ 𝐴 |
28 | | resmpt 5369 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝑊) ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ 0 ) ↾ (𝐴 ∩ 𝑊)) = (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) |
29 | 27, 28 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑘 ∈ 𝐴 ↦ 0 ) ↾ (𝐴 ∩ 𝑊)) = (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 ) |
30 | 26, 29 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐹 ↾ (𝐴 ∩ 𝑊)) = (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) |
31 | 19, 30 | eqtr3d 2646 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐹 ↾ 𝑊) = (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 )) |
32 | 31 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σg
(𝐹 ↾ 𝑊)) = (𝐺 Σg (𝑘 ∈ (𝐴 ∩ 𝑊) ↦ 0 ))) |
33 | 25 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 ))) |
34 | 11, 32, 33 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ (𝐹 supp 0 ) = ∅) → (𝐺 Σg
(𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹)) |
35 | 34 | ex 449 |
. 2
⊢ (𝜑 → ((𝐹 supp 0 ) = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹))) |
36 | | f1ofo 6057 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → 𝑓:(1...(#‘(𝐹 supp 0 )))–onto→(𝐹 supp 0 )) |
37 | | forn 6031 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(#‘(𝐹 supp 0 )))–onto→(𝐹 supp 0 ) → ran 𝑓 = (𝐹 supp 0 )) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → ran 𝑓 = (𝐹 supp 0 )) |
39 | 38 | ad2antll 761 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran 𝑓 = (𝐹 supp 0 )) |
40 | | gsumzres.s |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊) |
41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ 𝑊) |
42 | 39, 41 | eqsstrd 3602 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran 𝑓 ⊆ 𝑊) |
43 | | cores 5555 |
. . . . . . . . 9
⊢ (ran
𝑓 ⊆ 𝑊 → ((𝐹 ↾ 𝑊) ∘ 𝑓) = (𝐹 ∘ 𝑓)) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ((𝐹 ↾ 𝑊) ∘ 𝑓) = (𝐹 ∘ 𝑓)) |
45 | 44 | seqeq3d 12671 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) →
seq1((+g‘𝐺), ((𝐹 ↾ 𝑊) ∘ 𝑓)) = seq1((+g‘𝐺), (𝐹 ∘ 𝑓))) |
46 | 45 | fveq1d 6105 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) →
(seq1((+g‘𝐺), ((𝐹 ↾ 𝑊) ∘ 𝑓))‘(#‘(𝐹 supp 0 ))) =
(seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(#‘(𝐹 supp 0 )))) |
47 | | gsumzcl.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
48 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝐺) = (+g‘𝐺) |
49 | | gsumzcl.z |
. . . . . . 7
⊢ 𝑍 = (Cntz‘𝐺) |
50 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐺 ∈ Mnd) |
51 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐴 ∩ 𝑊) ∈ V) |
52 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐹:𝐴⟶𝐵) |
53 | | fssres 5983 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐴 ∩ 𝑊) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵) |
54 | 52, 27, 53 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵) |
55 | 18 | feq1d 5943 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵 ↔ (𝐹 ↾ 𝑊):(𝐴 ∩ 𝑊)⟶𝐵)) |
56 | 55 | biimpa 500 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵) → (𝐹 ↾ 𝑊):(𝐴 ∩ 𝑊)⟶𝐵) |
57 | 54, 56 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 ↾ 𝑊):(𝐴 ∩ 𝑊)⟶𝐵) |
58 | | gsumzcl.c |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
59 | | resss 5342 |
. . . . . . . . . 10
⊢ (𝐹 ↾ 𝑊) ⊆ 𝐹 |
60 | | rnss 5275 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ 𝑊) ⊆ 𝐹 → ran (𝐹 ↾ 𝑊) ⊆ ran 𝐹) |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . 9
⊢ ran
(𝐹 ↾ 𝑊) ⊆ ran 𝐹 |
62 | 49 | cntzidss 17593 |
. . . . . . . . 9
⊢ ((ran
𝐹 ⊆ (𝑍‘ran 𝐹) ∧ ran (𝐹 ↾ 𝑊) ⊆ ran 𝐹) → ran (𝐹 ↾ 𝑊) ⊆ (𝑍‘ran (𝐹 ↾ 𝑊))) |
63 | 58, 61, 62 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → ran (𝐹 ↾ 𝑊) ⊆ (𝑍‘ran (𝐹 ↾ 𝑊))) |
64 | 63 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran (𝐹 ↾ 𝑊) ⊆ (𝑍‘ran (𝐹 ↾ 𝑊))) |
65 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (#‘(𝐹 supp 0 )) ∈
ℕ) |
66 | | f1of1 6049 |
. . . . . . . . 9
⊢ (𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 )) |
67 | 66 | ad2antll 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 )) |
68 | | suppssdm 7195 |
. . . . . . . . . . 11
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
69 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
70 | 13, 69 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = 𝐴) |
71 | 68, 70 | syl5sseq 3616 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴) |
72 | 71, 40 | ssind 3799 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ (𝐴 ∩ 𝑊)) |
73 | 72 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ (𝐴 ∩ 𝑊)) |
74 | | f1ss 6019 |
. . . . . . . 8
⊢ ((𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 ) ∧ (𝐹 supp 0 ) ⊆ (𝐴 ∩ 𝑊)) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐴 ∩ 𝑊)) |
75 | 67, 73, 74 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐴 ∩ 𝑊)) |
76 | | fex 6394 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
77 | 13, 2, 76 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ V) |
78 | | ressuppss 7201 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ ((𝐹 ↾ 𝑊) supp 0 ) ⊆ (𝐹 supp 0 )) |
79 | 77, 21, 78 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ (𝐹 supp 0 )) |
80 | | sseq2 3590 |
. . . . . . . . . . 11
⊢ (ran
𝑓 = (𝐹 supp 0 ) → (((𝐹 ↾ 𝑊) supp 0 ) ⊆ ran 𝑓 ↔ ((𝐹 ↾ 𝑊) supp 0 ) ⊆ (𝐹 supp 0 ))) |
81 | 79, 80 | syl5ibr 235 |
. . . . . . . . . 10
⊢ (ran
𝑓 = (𝐹 supp 0 ) → (𝜑 → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ ran 𝑓)) |
82 | 36, 37, 81 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → (𝜑 → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ ran 𝑓)) |
83 | 82 | adantl 481 |
. . . . . . . 8
⊢
(((#‘(𝐹 supp
0 ))
∈ ℕ ∧ 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) → (𝜑 → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ ran 𝑓)) |
84 | 83 | impcom 445 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ((𝐹 ↾ 𝑊) supp 0 ) ⊆ ran 𝑓) |
85 | | eqid 2610 |
. . . . . . 7
⊢ (((𝐹 ↾ 𝑊) ∘ 𝑓) supp 0 ) = (((𝐹 ↾ 𝑊) ∘ 𝑓) supp 0 ) |
86 | 47, 5, 48, 49, 50, 51, 57, 64, 65, 75, 84, 85 | gsumval3 18131 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σg
(𝐹 ↾ 𝑊)) =
(seq1((+g‘𝐺), ((𝐹 ↾ 𝑊) ∘ 𝑓))‘(#‘(𝐹 supp 0 )))) |
87 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝐴 ∈ 𝑉) |
88 | 58 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
89 | 71 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ 𝐴) |
90 | | f1ss 6019 |
. . . . . . . 8
⊢ ((𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→(𝐹 supp 0 ) ∧ (𝐹 supp 0 ) ⊆ 𝐴) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→𝐴) |
91 | 67, 89, 90 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1→𝐴) |
92 | 23, 39 | syl5sseqr 3617 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐹 supp 0 ) ⊆ ran 𝑓) |
93 | | eqid 2610 |
. . . . . . 7
⊢ ((𝐹 ∘ 𝑓) supp 0 ) = ((𝐹 ∘ 𝑓) supp 0 ) |
94 | 47, 5, 48, 49, 50, 87, 52, 88, 65, 91, 92, 93 | gsumval3 18131 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σg
𝐹) =
(seq1((+g‘𝐺), (𝐹 ∘ 𝑓))‘(#‘(𝐹 supp 0 )))) |
95 | 46, 86, 94 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘(𝐹 supp 0 )) ∈ ℕ ∧
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ))) → (𝐺 Σg
(𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹)) |
96 | 95 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ (#‘(𝐹 supp 0 )) ∈ ℕ) →
(𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → (𝐺 Σg
(𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹))) |
97 | 96 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ (#‘(𝐹 supp 0 )) ∈ ℕ) →
(∃𝑓 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 ) → (𝐺 Σg
(𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹))) |
98 | 97 | expimpd 627 |
. 2
⊢ (𝜑 → (((#‘(𝐹 supp 0 )) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) → (𝐺 Σg
(𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹))) |
99 | | gsumzres.w |
. . 3
⊢ (𝜑 → 𝐹 finSupp 0 ) |
100 | | fsuppimp 8164 |
. . . 4
⊢ (𝐹 finSupp 0 → (Fun 𝐹 ∧ (𝐹 supp 0 ) ∈
Fin)) |
101 | 100 | simprd 478 |
. . 3
⊢ (𝐹 finSupp 0 → (𝐹 supp 0 ) ∈
Fin) |
102 | | fz1f1o 14288 |
. . 3
⊢ ((𝐹 supp 0 ) ∈ Fin →
((𝐹 supp 0 ) = ∅ ∨
((#‘(𝐹 supp 0 )) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )))) |
103 | 99, 101, 102 | 3syl 18 |
. 2
⊢ (𝜑 → ((𝐹 supp 0 ) = ∅ ∨
((#‘(𝐹 supp 0 )) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )))) |
104 | 35, 98, 103 | mpjaod 395 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹)) |