Metamath Proof Explorer

Theorem cbvsumdavw2

Description: Change bound variable and the set of integers in a sum. Deduction form. (Contributed by GG, 14-Aug-2025)

Ref Expression
Hypotheses cbvsumdavw2.1 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
cbvsumdavw2.2 ⊢ ( ( 𝜑 ∧ 𝑗 = 𝑘 ) → 𝐶 = 𝐷 )
Assertion cbvsumdavw2 ( 𝜑 → Σ 𝑗 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐷 )

Proof

Step Hyp Ref Expression
1 cbvsumdavw2.1 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
2 cbvsumdavw2.2 ⊢ ( ( 𝜑 ∧ 𝑗 = 𝑘 ) → 𝐶 = 𝐷 )
3 1 sseq1d ⊢ ( 𝜑 → ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ↔ 𝐵 ⊆ ( ℤ≥ ‘ 𝑚 ) ) )
4 1 eleq2d ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵 ) )
5 2 cbvcsbdavw ⊢ ( 𝜑 → ⦋ 𝑛 / 𝑗 ⦌ 𝐶 = ⦋ 𝑛 / 𝑘 ⦌ 𝐷 )
6 4 5 ifbieq1d ⊢ ( 𝜑 → if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑗 ⦌ 𝐶 , 0 ) = if ( 𝑛 ∈ 𝐵 , ⦋ 𝑛 / 𝑘 ⦌ 𝐷 , 0 ) )
7 6 mpteq2dv ⊢ ( 𝜑 → ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑗 ⦌ 𝐶 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐵 , ⦋ 𝑛 / 𝑘 ⦌ 𝐷 , 0 ) ) )
8 7 seqeq3d ⊢ ( 𝜑 → seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑗 ⦌ 𝐶 , 0 ) ) ) = seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐵 , ⦋ 𝑛 / 𝑘 ⦌ 𝐷 , 0 ) ) ) )
9 8 breq1d ⊢ ( 𝜑 → ( seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑗 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐵 , ⦋ 𝑛 / 𝑘 ⦌ 𝐷 , 0 ) ) ) ⇝ 𝑥 ) )
10 3 9 anbi12d ⊢ ( 𝜑 → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑗 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐵 , ⦋ 𝑛 / 𝑘 ⦌ 𝐷 , 0 ) ) ) ⇝ 𝑥 ) ) )
11 10 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑗 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐵 , ⦋ 𝑛 / 𝑘 ⦌ 𝐷 , 0 ) ) ) ⇝ 𝑥 ) ) )
12 1 f1oeq3d ⊢ ( 𝜑 → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ↔ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐵 ) )
13 2 cbvcsbdavw ⊢ ( 𝜑 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 = ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 )
14 13 mpteq2dv ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 ) )
15 14 seqeq3d ⊢ ( 𝜑 → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 ) ) )
16 15 fveq1d ⊢ ( 𝜑 → ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 ) ) ‘ 𝑚 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 ) ) ‘ 𝑚 ) )
17 16 eqeq2d ⊢ ( 𝜑 → ( 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 ) ) ‘ 𝑚 ) ↔ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 ) ) ‘ 𝑚 ) ) )
18 12 17 anbi12d ⊢ ( 𝜑 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 ) ) ‘ 𝑚 ) ) ) )
19 18 exbidv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 ) ) ‘ 𝑚 ) ) ) )
20 19 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 ) ) ‘ 𝑚 ) ) ) )
21 11 20 orbi12d ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑗 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐵 , ⦋ 𝑛 / 𝑘 ⦌ 𝐷 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 ) ) ‘ 𝑚 ) ) ) ) )
22 21 iotabidv ⊢ ( 𝜑 → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑗 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐵 , ⦋ 𝑛 / 𝑘 ⦌ 𝐷 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 ) ) ‘ 𝑚 ) ) ) ) )
23 df-sum ⊢ Σ 𝑗 ∈ 𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑗 ⦌ 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑗 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
24 df-sum ⊢ Σ 𝑘 ∈ 𝐵 𝐷 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐵 , ⦋ 𝑛 / 𝑘 ⦌ 𝐷 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐵 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐷 ) ) ‘ 𝑚 ) ) ) )
25 22 23 24 3eqtr4g ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐷 )