Theorem itgeq12dv

Description: Equality theorem for an integral. (Contributed by Thierry Arnoux, 14-Feb-2017)

	Ref	Expression
Hypotheses	itgeq12dv.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	itgeq12dv.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 = 𝐷 )
Assertion	itgeq12dv	⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		itgeq12dv.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		itgeq12dv.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 = 𝐷 )
3	2	fvoveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) )
4	3	breq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ↔ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) )
5	4	pm5.32da	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) ) )
6	1	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
7	6	anbi1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) ) )
8	5 7	bitrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) ) )
9	3	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) )
10		eqidd	⊢ ( ( 𝜑 ∧ ¬ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) ) → 0 = 0 )
11	8 9 10	ifbieq12d2	⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) )
12	11	mpteq2dv	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
13	12	fveq2d	⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
14	13	oveq2d	⊢ ( 𝜑 → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
15	14	sumeq2sdv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
16		eqid	⊢ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) )
17	16	dfitg	⊢ ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
18		eqid	⊢ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) )
19	18	dfitg	⊢ ∫ 𝐵 𝐷 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
20	15 17 19	3eqtr4g	⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥 )