MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqeq1 Structured version   Unicode version

Theorem seqeq1 11805
Description: Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
Assertion
Ref Expression
seqeq1  |-  ( M  =  N  ->  seq M (  .+  ,  F )  =  seq N (  .+  ,  F ) )

Proof of Theorem seqeq1
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5688 . . . . 5  |-  ( M  =  N  ->  ( F `  M )  =  ( F `  N ) )
2 opeq12 4058 . . . . 5  |-  ( ( M  =  N  /\  ( F `  M )  =  ( F `  N ) )  ->  <. M ,  ( F `
 M ) >.  =  <. N ,  ( F `  N )
>. )
31, 2mpdan 663 . . . 4  |-  ( M  =  N  ->  <. M , 
( F `  M
) >.  =  <. N , 
( F `  N
) >. )
4 rdgeq2 6864 . . . 4  |-  ( <. M ,  ( F `  M ) >.  =  <. N ,  ( F `  N ) >.  ->  rec ( ( x  e. 
_V ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. )  =  rec ( ( x  e. 
_V ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. N , 
( F `  N
) >. ) )
53, 4syl 16 . . 3  |-  ( M  =  N  ->  rec ( ( x  e. 
_V ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. )  =  rec ( ( x  e. 
_V ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. N , 
( F `  N
) >. ) )
65imaeq1d 5165 . 2  |-  ( M  =  N  ->  ( rec ( ( x  e. 
_V ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) " om )  =  ( rec ( ( x  e. 
_V ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. N , 
( F `  N
) >. ) " om ) )
7 df-seq 11803 . 2  |-  seq M
(  .+  ,  F
)  =  ( rec ( ( x  e. 
_V ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) " om )
8 df-seq 11803 . 2  |-  seq N
(  .+  ,  F
)  =  ( rec ( ( x  e. 
_V ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. N , 
( F `  N
) >. ) " om )
96, 7, 83eqtr4g 2498 1  |-  ( M  =  N  ->  seq M (  .+  ,  F )  =  seq N (  .+  ,  F ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364   _Vcvv 2970   <.cop 3880   "cima 4839   ` cfv 5415  (class class class)co 6090    e. cmpt2 6092   omcom 6475   reccrdg 6861   1c1 9279    + caddc 9281    seqcseq 11802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-cnv 4844  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fv 5423  df-recs 6828  df-rdg 6862  df-seq 11803
This theorem is referenced by:  seqeq1d  11808  seqfn  11814  seq1  11815  seqp1  11817  seqf1olem2  11842  seqid  11847  seqz  11850  iserex  13130  summolem2  13189  summo  13190  zsum  13191  isumsplit  13299  ege2le3  13371  gsumval2a  15505  leibpi  22296  ntrivcvg  27341  ntrivcvgn0  27342  ntrivcvgtail  27344  ntrivcvgmullem  27345  prodmolem2  27377  prodmo  27378  zprod  27379  fprodntriv  27384  stirlinglem12  29805
  Copyright terms: Public domain W3C validator