Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqeq3 Structured version   Visualization version   GIF version

Theorem seqeq3 13358
 Description: Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
Assertion
Ref Expression
seqeq3 (𝐹 = 𝐺 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺))

Proof of Theorem seqeq3
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq1 6645 . . . . . . 7 (𝐹 = 𝐺 → (𝐹‘(𝑥 + 1)) = (𝐺‘(𝑥 + 1)))
21oveq2d 7149 . . . . . 6 (𝐹 = 𝐺 → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐺‘(𝑥 + 1))))
32opeq2d 4786 . . . . 5 (𝐹 = 𝐺 → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩)
43mpoeq3dv 7210 . . . 4 (𝐹 = 𝐺 → (𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩))
5 fveq1 6645 . . . . 5 (𝐹 = 𝐺 → (𝐹𝑀) = (𝐺𝑀))
65opeq2d 4786 . . . 4 (𝐹 = 𝐺 → ⟨𝑀, (𝐹𝑀)⟩ = ⟨𝑀, (𝐺𝑀)⟩)
7 rdgeq12 8027 . . . 4 (((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩) ∧ ⟨𝑀, (𝐹𝑀)⟩ = ⟨𝑀, (𝐺𝑀)⟩) → rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹𝑀)⟩) = rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐺𝑀)⟩))
84, 6, 7syl2anc 586 . . 3 (𝐹 = 𝐺 → rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹𝑀)⟩) = rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐺𝑀)⟩))
98imaeq1d 5904 . 2 (𝐹 = 𝐺 → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹𝑀)⟩) “ ω) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐺𝑀)⟩) “ ω))
10 df-seq 13354 . 2 seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹𝑀)⟩) “ ω)
11 df-seq 13354 . 2 seq𝑀( + , 𝐺) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐺𝑀)⟩) “ ω)
129, 10, 113eqtr4g 2880 1 (𝐹 = 𝐺 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1537  Vcvv 3473  ⟨cop 4549   “ cima 5534  ‘cfv 6331  (class class class)co 7133   ∈ cmpo 7135  ωcom 7558  reccrdg 8023  1c1 10516   + caddc 10518  seqcseq 13353 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-opab 5105  df-mpt 5123  df-xp 5537  df-cnv 5539  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-iota 6290  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-seq 13354 This theorem is referenced by:  seqeq3d  13361  cbvprod  15249  iprodmul  15337  geolim3  24914  leibpilem2  25506  basel  25654  faclim  32986  ovoliunnfl  34975  voliunnfl  34977  heiborlem10  35134  binomcxplemnn0  40836  binomcxplemdvsum  40842  binomcxp  40844  fourierdlem112  42651  fouriersw  42664  voliunsge0lem  42902
 Copyright terms: Public domain W3C validator