Metamath Proof Explorer


Theorem seqfeq4

Description: Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses seqfeq4.m ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
seqfeq4.f ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑥 ) ∈ 𝑆 )
seqfeq4.cl ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
seqfeq4.id ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 𝑄 𝑦 ) )
Assertion seqfeq4 ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑀 ( 𝑄 , 𝐹 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 seqfeq4.m ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
2 seqfeq4.f ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑥 ) ∈ 𝑆 )
3 seqfeq4.cl ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
4 seqfeq4.id ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 𝑄 𝑦 ) )
5 fvex ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V
6 fvi ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V → ( I ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
7 5 6 ax-mp ( I ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 )
8 ovex ( 𝑥 + 𝑦 ) ∈ V
9 fvi ( ( 𝑥 + 𝑦 ) ∈ V → ( I ‘ ( 𝑥 + 𝑦 ) ) = ( 𝑥 + 𝑦 ) )
10 8 9 ax-mp ( I ‘ ( 𝑥 + 𝑦 ) ) = ( 𝑥 + 𝑦 )
11 fvi ( 𝑥 ∈ V → ( I ‘ 𝑥 ) = 𝑥 )
12 11 elv ( I ‘ 𝑥 ) = 𝑥
13 fvi ( 𝑦 ∈ V → ( I ‘ 𝑦 ) = 𝑦 )
14 13 elv ( I ‘ 𝑦 ) = 𝑦
15 12 14 oveq12i ( ( I ‘ 𝑥 ) 𝑄 ( I ‘ 𝑦 ) ) = ( 𝑥 𝑄 𝑦 )
16 4 10 15 3eqtr4g ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( I ‘ ( 𝑥 + 𝑦 ) ) = ( ( I ‘ 𝑥 ) 𝑄 ( I ‘ 𝑦 ) ) )
17 fvex ( 𝐹𝑥 ) ∈ V
18 fvi ( ( 𝐹𝑥 ) ∈ V → ( I ‘ ( 𝐹𝑥 ) ) = ( 𝐹𝑥 ) )
19 17 18 mp1i ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( I ‘ ( 𝐹𝑥 ) ) = ( 𝐹𝑥 ) )
20 3 2 1 16 19 seqhomo ( 𝜑 → ( I ‘ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq 𝑀 ( 𝑄 , 𝐹 ) ‘ 𝑁 ) )
21 7 20 eqtr3id ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑀 ( 𝑄 , 𝐹 ) ‘ 𝑁 ) )