Metamath Proof Explorer

Theorem seqeq1

Description: Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013)

Ref Expression
Assertion seqeq1 
|- ( M = N -> seq M ( .+ , F ) = seq N ( .+ , F ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( M = N -> ( F ` M ) = ( F ` N ) )
2 opeq12 
 |-  ( ( M = N /\ ( F ` M ) = ( F ` N ) ) -> <. M , ( F ` M ) >. = <. N , ( F ` N ) >. )
3 1 2 mpdan 
 |-  ( M = N -> <. M , ( F ` M ) >. = <. N , ( F ` N ) >. )
4 rdgeq2 
 |-  ( <. 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 ) >. ) )
5 3 4 syl 
 |-  ( 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 ) >. ) )
6 5 imaeq1d 
 |-  ( 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 
 |-  seq M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
8 df-seq 
 |-  seq N ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. N , ( F ` N ) >. ) " _om )
9 6 7 8 3eqtr4g 
 |-  ( M = N -> seq M ( .+ , F ) = seq N ( .+ , F ) )