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

Metamath Proof Explorer

Theorem seqeq3

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

Ref Expression
Assertion seqeq3 
|- ( F = G -> seq M ( .+ , F ) = seq M ( .+ , G ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( F = G -> ( F ` ( x + 1 ) ) = ( G ` ( x + 1 ) ) )
2 1 oveq2d 
 |-  ( F = G -> ( y .+ ( F ` ( x + 1 ) ) ) = ( y .+ ( G ` ( x + 1 ) ) ) )
3 2 opeq2d 
 |-  ( F = G -> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. = <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. )
4 3 mpoeq3dv 
 |-  ( F = G -> ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) = ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) )
5 fveq1 
 |-  ( F = G -> ( F ` M ) = ( G ` M ) )
6 5 opeq2d 
 |-  ( F = G -> <. M , ( F ` M ) >. = <. M , ( G ` M ) >. )
7 rdgeq12 
 |-  ( ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) = ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) /\ <. M , ( F ` M ) >. = <. M , ( G ` M ) >. ) -> 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 .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) )
8 4 6 7 syl2anc 
 |-  ( F = G -> 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 .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) )
9 8 imaeq1d 
 |-  ( F = G -> ( 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 .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) " _om ) )
10 df-seq 
 |-  seq M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
11 df-seq 
 |-  seq M ( .+ , G ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) " _om )
12 9 10 11 3eqtr4g 
 |-  ( F = G -> seq M ( .+ , F ) = seq M ( .+ , G ) )