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 φ N M
seqfeq4.f φ x M N F x S
seqfeq4.cl φ x S y S x + ˙ y S
seqfeq4.id φ x S y S x + ˙ y = x Q y
Assertion seqfeq4 φ seq M + ˙ F N = seq M Q F N

Proof

Step Hyp Ref Expression
1 seqfeq4.m φ N M
2 seqfeq4.f φ x M N F x S
3 seqfeq4.cl φ x S y S x + ˙ y S
4 seqfeq4.id φ x S y S x + ˙ y = x Q y
5 fvex seq M + ˙ F N V
6 fvi seq M + ˙ F N V I seq M + ˙ F N = seq M + ˙ F N
7 5 6 ax-mp I seq M + ˙ F N = seq M + ˙ F N
8 ovex x + ˙ y V
9 fvi x + ˙ y V I x + ˙ y = x + ˙ y
10 8 9 ax-mp I x + ˙ y = x + ˙ y
11 fvi x V I x = x
12 11 elv I x = x
13 fvi y V I y = y
14 13 elv I y = y
15 12 14 oveq12i I x Q I y = x Q y
16 4 10 15 3eqtr4g φ x S y S I x + ˙ y = I x Q I y
17 fvex F x V
18 fvi F x V I F x = F x
19 17 18 mp1i φ x M N I F x = F x
20 3 2 1 16 19 seqhomo φ I seq M + ˙ F N = seq M Q F N
21 7 20 eqtr3id φ seq M + ˙ F N = seq M Q F N