ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  iseqeq3 Unicode version
Theorem iseqeq3 9436
Description: Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
Assertion
Ref Expression
iseqeq3 |- ( F = G -> seq M ( .+ , F , S ) = seq M ( .+ , G , S ) )
Proof of Theorem iseqeq3
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 938 . . . . . . . 8 |- ( ( F = G /\ x e. ( ZZ>= ` M ) /\ y e. S ) -> F = G )
21fveq1d 5200 . . . . . . 7 |- ( ( F = G /\ x e. ( ZZ>= ` M ) /\ y e. S ) -> ( F ` ( x + 1 ) ) = ( G ` ( x + 1 ) ) )
32oveq2d 5548 . . . . . 6 |- ( ( F = G /\ x e. ( ZZ>= ` M ) /\ y e. S ) -> ( y .+ ( F ` ( x + 1 ) ) ) = ( y .+ ( G ` ( x + 1 ) ) ) )
43opeq2d 3577 . . . . 5 |- ( ( F = G /\ x e. ( ZZ>= ` M ) /\ y e. S ) -> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. = <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. )
54mpt2eq3dva 5589 . . . 4 |- ( F = G -> ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) = ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) )
6 fveq1 5197 . . . . 5 |- ( F = G -> ( F ` M ) = ( G ` M ) )
76opeq2d 3577 . . . 4 |- ( F = G -> <. M , ( F ` M ) >. = <. M , ( G ` M ) >. )
8 freceq1 6002 . . . . 5 |- ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) = ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) -> frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) = frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) )
9 freceq2 6003 . . . . 5 |- ( <. M , ( F ` M ) >. = <. M , ( G ` M ) >. -> frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) = frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) )
108, 9sylan9eq 2133 . . . 4 |- ( ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) = ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) /\ <. M , ( F ` M ) >. = <. M , ( G ` M ) >. ) -> frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) = frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) )
115, 7, 10syl2anc 403 . . 3 |- ( F = G -> frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) = frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) )
1211rneqd 4581 . 2 |- ( F = G -> ran frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) )
13 df-iseq 9432 . 2 |- seq M ( .+ , F , S ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
14 df-iseq 9432 . 2 |- seq M ( .+ , G , S ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. )
1512, 13, 143eqtr4g 2138 1 |- ( F = G -> seq M ( .+ , F , S ) = seq M ( .+ , G , S ) )
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ w3a 919   = wceq 1284   e. wcel 1433   <.cop 3401   ran crn 4364   ` cfv 4922  (class class class)co 5532   |-> cmpt2 5534  freccfrec 6000   1c1 6982   + caddc 6984   ZZ>=cuz 8619   seqcseq 9431
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063
This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-opab 3840  df-mpt 3841  df-cnv 4371  df-dm 4373  df-rn 4374  df-res 4375  df-iota 4887  df-fv 4930  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-recs 5943  df-frec 6001  df-iseq 9432
This theorem is referenced by:  expival  9478  sumeq1  10192
  Copyright terms: Public domain W3C validator