This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumval2

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 ⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
Assertion gsumval2 ( 𝜑 → ( 𝐺 Σ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 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7 eqid ⊢ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
8 3 adantr ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → 𝐺 ∈ 𝑉 )
9 ovexd ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ( 𝑀 ... 𝑁 ) ∈ V )
10 5 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( 𝑀 ... 𝑁 ) )
11 10 adantr ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → 𝐹 Fn ( 𝑀 ... 𝑁 ) )
12 simpr ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } )
13 df-f ⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ↔ ( 𝐹 Fn ( 𝑀 ... 𝑁 ) ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) )
14 11 12 13 sylanbrc ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } )
15 1 6 2 7 8 9 14 gsumval1 ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ( 𝐺 Σg 𝐹 ) = ( 0g ‘ 𝐺 ) )
16 simpl ⊢ ( ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) → ( 𝑥 + 𝑦 ) = 𝑦 )
17 16 ralimi ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = 𝑦 )
18 17 a1i ⊢ ( 𝑥 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = 𝑦 ) )
19 18 ss2rabi ⊢ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = 𝑦 }
20 fvex ⊢ ( 0g ‘ 𝐺 ) ∈ V
21 20 snid ⊢ ( 0g ‘ 𝐺 ) ∈ { ( 0g ‘ 𝐺 ) }
22 5 fdmd ⊢ ( 𝜑 → dom 𝐹 = ( 𝑀 ... 𝑁 ) )
23 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
24 ne0i ⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... 𝑁 ) ≠ ∅ )
25 4 23 24 3syl ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ≠ ∅ )
26 22 25 eqnetrd ⊢ ( 𝜑 → dom 𝐹 ≠ ∅ )
27 dm0rn0 ⊢ ( dom 𝐹 = ∅ ↔ ran 𝐹 = ∅ )
28 27 necon3bii ⊢ ( dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅ )
29 26 28 sylib ⊢ ( 𝜑 → ran 𝐹 ≠ ∅ )
30 29 adantr ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ran 𝐹 ≠ ∅ )
31 ssn0 ⊢ ( ( ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ∧ ran 𝐹 ≠ ∅ ) → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ≠ ∅ )
32 12 30 31 syl2anc ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ≠ ∅ )
33 32 neneqd ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ¬ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } = ∅ )
34 1 6 2 7 mgmidsssn0 ⊢ ( 𝐺 ∈ 𝑉 → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ⊆ { ( 0g ‘ 𝐺 ) } )
35 3 34 syl ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ⊆ { ( 0g ‘ 𝐺 ) } )
36 sssn ⊢ ( { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ⊆ { ( 0g ‘ 𝐺 ) } ↔ ( { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } = ∅ ∨ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } = { ( 0g ‘ 𝐺 ) } ) )
37 35 36 sylib ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } = ∅ ∨ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } = { ( 0g ‘ 𝐺 ) } ) )
38 37 orcanai ⊢ ( ( 𝜑 ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } = ∅ ) → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } = { ( 0g ‘ 𝐺 ) } )
39 33 38 syldan ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } = { ( 0g ‘ 𝐺 ) } )
40 21 39 eleqtrrid ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ( 0g ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } )
41 19 40 sselid ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ( 0g ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = 𝑦 } )
42 oveq1 ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( 𝑥 + 𝑦 ) = ( ( 0g ‘ 𝐺 ) + 𝑦 ) )
43 42 eqeq1d ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( ( 𝑥 + 𝑦 ) = 𝑦 ↔ ( ( 0g ‘ 𝐺 ) + 𝑦 ) = 𝑦 ) )
44 43 ralbidv ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ( ( 0g ‘ 𝐺 ) + 𝑦 ) = 𝑦 ) )
45 44 elrab ⊢ ( ( 0g ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = 𝑦 } ↔ ( ( 0g ‘ 𝐺 ) ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 0g ‘ 𝐺 ) + 𝑦 ) = 𝑦 ) )
46 oveq2 ⊢ ( 𝑦 = ( 0g ‘ 𝐺 ) → ( ( 0g ‘ 𝐺 ) + 𝑦 ) = ( ( 0g ‘ 𝐺 ) + ( 0g ‘ 𝐺 ) ) )
47 id ⊢ ( 𝑦 = ( 0g ‘ 𝐺 ) → 𝑦 = ( 0g ‘ 𝐺 ) )
48 46 47 eqeq12d ⊢ ( 𝑦 = ( 0g ‘ 𝐺 ) → ( ( ( 0g ‘ 𝐺 ) + 𝑦 ) = 𝑦 ↔ ( ( 0g ‘ 𝐺 ) + ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) ) )
49 48 rspcva ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 0g ‘ 𝐺 ) + 𝑦 ) = 𝑦 ) → ( ( 0g ‘ 𝐺 ) + ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
50 45 49 sylbi ⊢ ( ( 0g ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = 𝑦 } → ( ( 0g ‘ 𝐺 ) + ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
51 41 50 syl ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ( ( 0g ‘ 𝐺 ) + ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
52 4 adantr ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
53 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) ∧ 𝑧 ∈ ( 𝑀 ... 𝑁 ) ) → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ⊆ { ( 0g ‘ 𝐺 ) } )
54 14 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) ∧ 𝑧 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } )
55 53 54 sseldd ⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) ∧ 𝑧 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ { ( 0g ‘ 𝐺 ) } )
56 elsni ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ { ( 0g ‘ 𝐺 ) } → ( 𝐹 ‘ 𝑧 ) = ( 0g ‘ 𝐺 ) )
57 55 56 syl ⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) ∧ 𝑧 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 0g ‘ 𝐺 ) )
58 51 52 57 seqid3 ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( 0g ‘ 𝐺 ) )
59 15 58 eqtr4d ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ( 𝐺 Σg 𝐹 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
60 3 adantr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → 𝐺 ∈ 𝑉 )
61 4 adantr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
62 5 adantr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
63 simpr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ¬ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } )
64 1 2 60 61 62 7 63 gsumval2a ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ) → ( 𝐺 Σg 𝐹 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
65 59 64 pm2.61dan ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )