Theorem cbvitgvw2

Description: Change bound variable and domain in an integral, using implicit substitution. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypotheses	cbvitgvw2.1	⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
	cbvitgvw2.2	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
Assertion	cbvitgvw2	⊢ ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑦

Proof

Step	Hyp	Ref	Expression
1		cbvitgvw2.1	⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
2		cbvitgvw2.2	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
3	1	fvoveq1d	⊢ ( 𝑥 = 𝑦 → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑡 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑡 ) ) ) )
4		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
5	4 2	eleq12d	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
6	5	anbi1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣 ) ) )
7	6	ifbid	⊢ ( 𝑥 = 𝑦 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) = if ( ( 𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) )
8	3 7	csbeq12dv	⊢ ( 𝑥 = 𝑦 → ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) = ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) )
9	8	cbvmptv	⊢ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) = ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) )
10	9	fveq2i	⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) = ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) )
11	10	oveq2i	⊢ ( ( i ↑ 𝑡 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) = ( ( i ↑ 𝑡 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) )
12	11	sumeq2si	⊢ Σ 𝑡 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑡 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) = Σ 𝑡 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑡 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) )
13		df-itg	⊢ ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑡 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑡 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) )
14		df-itg	⊢ ∫ 𝐵 𝐷 d 𝑦 = Σ 𝑡 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑡 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑡 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐵 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) )
15	12 13 14	3eqtr4i	⊢ ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑦