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

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 𝑀 ( 𝑄 , 𝐹 ) ‘ 𝑁 ) )