Theorem seqeq3 13941

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.

Step	Hyp	Ref	Expression
1		fveq1 6841	. . . . . . 7 ⊢ (𝐹 = 𝐺 → (𝐹‘(𝑥 + 1)) = (𝐺‘(𝑥 + 1)))
2	1	oveq2d 7384	. . . . . 6 ⊢ (𝐹 = 𝐺 → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐺‘(𝑥 + 1))))
3	2	opeq2d 4838	. . . . 5 ⊢ (𝐹 = 𝐺 → ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩ = ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩)
4	3	mpoeq3dv 7447	. . . 4 ⊢ (𝐹 = 𝐺 → (𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩))
5		fveq1 6841	. . . . 5 ⊢ (𝐹 = 𝐺 → (𝐹‘𝑀) = (𝐺‘𝑀))
6	5	opeq2d 4838	. . . 4 ⊢ (𝐹 = 𝐺 → ⟨𝑀, (𝐹‘𝑀)⟩ = ⟨𝑀, (𝐺‘𝑀)⟩)
7		rdgeq12 8354	. . . 4 ⊢ (((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩) = (𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩) ∧ ⟨𝑀, (𝐹‘𝑀)⟩ = ⟨𝑀, (𝐺‘𝑀)⟩) → rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) = rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐺‘𝑀)⟩))
8	4, 6, 7	syl2anc 585	. . 3 ⊢ (𝐹 = 𝐺 → rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) = rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐺‘𝑀)⟩))
9	8	imaeq1d 6026	. 2 ⊢ (𝐹 = 𝐺 → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐺‘𝑀)⟩) “ ω))
10		df-seq 13937	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
11		df-seq 13937	. 2 ⊢ seq𝑀( + , 𝐺) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐺‘𝑀)⟩) “ ω)
12	9, 10, 11	3eqtr4g 2797	1 ⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺))

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3442  ⟨cop 4588   “ cima 5635  ‘cfv 6500  (class class class)co 7368   ∈ cmpo 7370  ωcom 7818  reccrdg 8350  1c1 11039   + caddc 11041  seqcseq 13936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-xp 5638  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-iota 6456  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-seq 13937

This theorem is referenced by:  seqeq3d  13944  cbvprod  15848  cbvprodv  15849  prodeq1i  15851  iprodmul  15938  geolim3  26315  leibpilem2  26919  basel  27068  faclim  35959  sumeq2si  36415  prodeq2si  36417  cbvprodvw2  36460  ovoliunnfl  37910  voliunnfl  37912  heiborlem10  38068  binomcxplemnn0  44702  binomcxplemdvsum  44708  binomcxp  44710  fourierdlem112  46573  fouriersw  46586  voliunsge0lem  46827