Metamath Proof Explorer

Theorem gsumval2a

Description: Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses gsumval2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumval2.p ⊢ + = ( +g ‘ 𝐺 )
gsumval2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
gsumval2.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
gsumval2.f ⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
gsumval2a.o ⊢ 𝑂 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
gsumval2a.f ⊢ ( 𝜑 → ¬ ran 𝐹 ⊆ 𝑂 )
Assertion gsumval2a ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 gsumval2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumval2.p ⊢ + = ( +g ‘ 𝐺 )
3 gsumval2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4 gsumval2.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 gsumval2.f ⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
6 gsumval2a.o ⊢ 𝑂 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
7 gsumval2a.f ⊢ ( 𝜑 → ¬ ran 𝐹 ⊆ 𝑂 )
8 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
9 eqidd ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) = ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) )
10 ovexd ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ V )
11 1 8 2 6 9 3 10 5 gsumval ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ 𝑂 , ( 0g ‘ 𝐺 ) , if ( ( 𝑀 ... 𝑁 ) ∈ ran ... , ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) ) ) ) ) )
12 7 iffalsed ⊢ ( 𝜑 → if ( ran 𝐹 ⊆ 𝑂 , ( 0g ‘ 𝐺 ) , if ( ( 𝑀 ... 𝑁 ) ∈ ran ... , ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) ) ) ) ) = if ( ( 𝑀 ... 𝑁 ) ∈ ran ... , ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) ) ) ) )
13 fzf ⊢ ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ
14 ffn ⊢ ( ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ → ... Fn ( ℤ × ℤ ) )
15 13 14 ax-mp ⊢ ... Fn ( ℤ × ℤ )
16 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
17 4 16 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
18 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
19 4 18 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
20 fnovrn ⊢ ( ( ... Fn ( ℤ × ℤ ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) ∈ ran ... )
21 15 17 19 20 mp3an2i ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ ran ... )
22 21 iftrued ⊢ ( 𝜑 → if ( ( 𝑀 ... 𝑁 ) ∈ ran ... , ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) ) ) ) = ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
23 12 22 eqtrd ⊢ ( 𝜑 → if ( ran 𝐹 ⊆ 𝑂 , ( 0g ‘ 𝐺 ) , if ( ( 𝑀 ... 𝑁 ) ∈ ran ... , ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) ) ) ) ) = ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
24 11 23 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
25 fvex ⊢ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V
26 fzopth ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ↔ ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) ) )
27 4 26 syl ⊢ ( 𝜑 → ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ↔ ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) ) )
28 simpl ⊢ ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) → 𝑀 = 𝑚 )
29 28 seqeq1d ⊢ ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) → seq 𝑀 ( + , 𝐹 ) = seq 𝑚 ( + , 𝐹 ) )
30 simpr ⊢ ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) → 𝑁 = 𝑛 )
31 29 30 fveq12d ⊢ ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) )
32 31 eqcomd ⊢ ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) → ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
33 eqeq1 ⊢ ( 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) → ( 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ↔ ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
34 32 33 syl5ibrcom ⊢ ( ( 𝑀 = 𝑚 ∧ 𝑁 = 𝑛 ) → ( 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) → 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
35 27 34 syl6bi ⊢ ( 𝜑 → ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) → ( 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) → 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
36 35 impd ⊢ ( 𝜑 → ( ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) → 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
37 36 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) → 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
38 37 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) → 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
39 17 adantr ⊢ ( ( 𝜑 ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) → 𝑀 ∈ ℤ )
40 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑁 ) )
41 40 eqcomd ⊢ ( 𝑛 = 𝑁 → ( 𝑀 ... 𝑁 ) = ( 𝑀 ... 𝑛 ) )
42 41 biantrurd ⊢ ( 𝑛 = 𝑁 → ( 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ↔ ( ( 𝑀 ... 𝑁 ) = ( 𝑀 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
43 fveq2 ⊢ ( 𝑛 = 𝑁 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
44 43 eqeq2d ⊢ ( 𝑛 = 𝑁 → ( 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ↔ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
45 42 44 bitr3d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑀 ... 𝑁 ) = ( 𝑀 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ↔ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
46 45 rspcev ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑀 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) )
47 4 46 sylan ⊢ ( ( 𝜑 ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) → ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑀 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) )
48 fveq2 ⊢ ( 𝑚 = 𝑀 → ( ℤ≥ ‘ 𝑚 ) = ( ℤ≥ ‘ 𝑀 ) )
49 oveq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 ... 𝑛 ) = ( 𝑀 ... 𝑛 ) )
50 49 eqeq2d ⊢ ( 𝑚 = 𝑀 → ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ↔ ( 𝑀 ... 𝑁 ) = ( 𝑀 ... 𝑛 ) ) )
51 seqeq1 ⊢ ( 𝑚 = 𝑀 → seq 𝑚 ( + , 𝐹 ) = seq 𝑀 ( + , 𝐹 ) )
52 51 fveq1d ⊢ ( 𝑚 = 𝑀 → ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) )
53 52 eqeq2d ⊢ ( 𝑚 = 𝑀 → ( 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ↔ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) )
54 50 53 anbi12d ⊢ ( 𝑚 = 𝑀 → ( ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ↔ ( ( 𝑀 ... 𝑁 ) = ( 𝑀 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
55 48 54 rexeqbidv ⊢ ( 𝑚 = 𝑀 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ↔ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑀 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
56 55 spcegv ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑀 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) → ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
57 39 47 56 sylc ⊢ ( ( 𝜑 ∧ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) → ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) )
58 57 ex ⊢ ( 𝜑 → ( 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) → ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
59 38 58 impbid ⊢ ( 𝜑 → ( ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ↔ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
60 59 adantr ⊢ ( ( 𝜑 ∧ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V ) → ( ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ↔ 𝑧 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
61 60 iota5 ⊢ ( ( 𝜑 ∧ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V ) → ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
62 25 61 mpan2 ⊢ ( 𝜑 → ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( ( 𝑀 ... 𝑁 ) = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
63 24 62 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )