Step | Hyp | Ref
| Expression |
1 | | gsumval2.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
2 | | eqid 2610 |
. . . 4
⊢
(0g‘𝐺) = (0g‘𝐺) |
3 | | gsumval2.p |
. . . 4
⊢ + =
(+g‘𝐺) |
4 | | gsumval2a.o |
. . . 4
⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} |
5 | | eqidd 2611 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ (V ∖ 𝑂)) = (◡𝐹 “ (V ∖ 𝑂))) |
6 | | gsumval2.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
7 | | ovex 6577 |
. . . . 5
⊢ (𝑀...𝑁) ∈ V |
8 | 7 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑀...𝑁) ∈ V) |
9 | | gsumval2.f |
. . . 4
⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵) |
10 | 1, 2, 3, 4, 5, 6, 8, 9 | gsumval 17094 |
. . 3
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ 𝑂, (0g‘𝐺), if((𝑀...𝑁) ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ 𝑂))))–1-1-onto→(◡𝐹 “ (V ∖ 𝑂)) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ 𝑂))))))))) |
11 | | gsumval2a.f |
. . . . 5
⊢ (𝜑 → ¬ ran 𝐹 ⊆ 𝑂) |
12 | 11 | iffalsed 4047 |
. . . 4
⊢ (𝜑 → if(ran 𝐹 ⊆ 𝑂, (0g‘𝐺), if((𝑀...𝑁) ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ 𝑂))))–1-1-onto→(◡𝐹 “ (V ∖ 𝑂)) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ 𝑂)))))))) = if((𝑀...𝑁) ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ 𝑂))))–1-1-onto→(◡𝐹 “ (V ∖ 𝑂)) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ 𝑂)))))))) |
13 | | gsumval2.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
14 | | eluzel2 11568 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
16 | | eluzelz 11573 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
17 | 13, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
18 | | fzf 12201 |
. . . . . . . 8
⊢
...:(ℤ × ℤ)⟶𝒫 ℤ |
19 | | ffn 5958 |
. . . . . . . 8
⊢
(...:(ℤ × ℤ)⟶𝒫 ℤ → ... Fn
(ℤ × ℤ)) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢ ... Fn
(ℤ × ℤ) |
21 | | fnovrn 6707 |
. . . . . . 7
⊢ ((... Fn
(ℤ × ℤ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ ran ...) |
22 | 20, 21 | mp3an1 1403 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ ran ...) |
23 | 15, 17, 22 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑀...𝑁) ∈ ran ...) |
24 | 23 | iftrued 4044 |
. . . 4
⊢ (𝜑 → if((𝑀...𝑁) ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ 𝑂))))–1-1-onto→(◡𝐹 “ (V ∖ 𝑂)) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ 𝑂))))))) = (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)))) |
25 | 12, 24 | eqtrd 2644 |
. . 3
⊢ (𝜑 → if(ran 𝐹 ⊆ 𝑂, (0g‘𝐺), if((𝑀...𝑁) ∈ ran ..., (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑧∃𝑓(𝑓:(1...(#‘(◡𝐹 “ (V ∖ 𝑂))))–1-1-onto→(◡𝐹 “ (V ∖ 𝑂)) ∧ 𝑧 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘(◡𝐹 “ (V ∖ 𝑂)))))))) = (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)))) |
26 | 10, 25 | eqtrd 2644 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝐹) = (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)))) |
27 | | fvex 6113 |
. . 3
⊢ (seq𝑀( + , 𝐹)‘𝑁) ∈ V |
28 | | fzopth 12249 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝑚...𝑛) ↔ (𝑀 = 𝑚 ∧ 𝑁 = 𝑛))) |
29 | 13, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀...𝑁) = (𝑚...𝑛) ↔ (𝑀 = 𝑚 ∧ 𝑁 = 𝑛))) |
30 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 = 𝑚 ∧ 𝑁 = 𝑛) → 𝑀 = 𝑚) |
31 | 30 | seqeq1d 12669 |
. . . . . . . . . . . . 13
⊢ ((𝑀 = 𝑚 ∧ 𝑁 = 𝑛) → seq𝑀( + , 𝐹) = seq𝑚( + , 𝐹)) |
32 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑀 = 𝑚 ∧ 𝑁 = 𝑛) → 𝑁 = 𝑛) |
33 | 31, 32 | fveq12d 6109 |
. . . . . . . . . . . 12
⊢ ((𝑀 = 𝑚 ∧ 𝑁 = 𝑛) → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑚( + , 𝐹)‘𝑛)) |
34 | 33 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝑀 = 𝑚 ∧ 𝑁 = 𝑛) → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁)) |
35 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) → (𝑧 = (seq𝑀( + , 𝐹)‘𝑁) ↔ (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁))) |
36 | 34, 35 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((𝑀 = 𝑚 ∧ 𝑁 = 𝑛) → (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) → 𝑧 = (seq𝑀( + , 𝐹)‘𝑁))) |
37 | 29, 36 | syl6bi 242 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀...𝑁) = (𝑚...𝑛) → (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) → 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)))) |
38 | 37 | impd 446 |
. . . . . . . 8
⊢ (𝜑 → (((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) → 𝑧 = (seq𝑀( + , 𝐹)‘𝑁))) |
39 | 38 | rexlimdvw 3016 |
. . . . . . 7
⊢ (𝜑 → (∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) → 𝑧 = (seq𝑀( + , 𝐹)‘𝑁))) |
40 | 39 | exlimdv 1848 |
. . . . . 6
⊢ (𝜑 → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) → 𝑧 = (seq𝑀( + , 𝐹)‘𝑁))) |
41 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)) → 𝑀 ∈ ℤ) |
42 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑁 → (𝑀...𝑛) = (𝑀...𝑁)) |
43 | 42 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (𝑀...𝑁) = (𝑀...𝑛)) |
44 | 43 | biantrurd 528 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → (𝑧 = (seq𝑀( + , 𝐹)‘𝑛) ↔ ((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛)))) |
45 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁)) |
46 | 45 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → (𝑧 = (seq𝑀( + , 𝐹)‘𝑛) ↔ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁))) |
47 | 44, 46 | bitr3d 269 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛)) ↔ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁))) |
48 | 47 | rspcev 3282 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)) → ∃𝑛 ∈ (ℤ≥‘𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛))) |
49 | 13, 48 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)) → ∃𝑛 ∈ (ℤ≥‘𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛))) |
50 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (ℤ≥‘𝑚) =
(ℤ≥‘𝑀)) |
51 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑀 → (𝑚...𝑛) = (𝑀...𝑛)) |
52 | 51 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → ((𝑀...𝑁) = (𝑚...𝑛) ↔ (𝑀...𝑁) = (𝑀...𝑛))) |
53 | | seqeq1 12666 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑀 → seq𝑚( + , 𝐹) = seq𝑀( + , 𝐹)) |
54 | 53 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑀 → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑛)) |
55 | 54 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → (𝑧 = (seq𝑚( + , 𝐹)‘𝑛) ↔ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛))) |
56 | 52, 55 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛)))) |
57 | 50, 56 | rexeqbidv 3130 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛)))) |
58 | 57 | spcegv 3267 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ →
(∃𝑛 ∈
(ℤ≥‘𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑛)) → ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)))) |
59 | 41, 49, 58 | sylc 63 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁)) → ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))) |
60 | 59 | ex 449 |
. . . . . 6
⊢ (𝜑 → (𝑧 = (seq𝑀( + , 𝐹)‘𝑁) → ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)))) |
61 | 40, 60 | impbid 201 |
. . . . 5
⊢ (𝜑 → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁))) |
62 | 61 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (seq𝑀( + , 𝐹)‘𝑁) ∈ V) → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ 𝑧 = (seq𝑀( + , 𝐹)‘𝑁))) |
63 | 62 | iota5 5788 |
. . 3
⊢ ((𝜑 ∧ (seq𝑀( + , 𝐹)‘𝑁) ∈ V) → (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))) = (seq𝑀( + , 𝐹)‘𝑁)) |
64 | 27, 63 | mpan2 703 |
. 2
⊢ (𝜑 → (℩𝑧∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑧 = (seq𝑚( + , 𝐹)‘𝑛))) = (seq𝑀( + , 𝐹)‘𝑁)) |
65 | 26, 64 | eqtrd 2644 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁)) |