Metamath Proof Explorer


Theorem itgeq12dv

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

Ref Expression
Hypotheses itgeq12dv.2 φ A = B
itgeq12dv.1 φ x A C = D
Assertion itgeq12dv φ A C dx = B D dx

Proof

Step Hyp Ref Expression
1 itgeq12dv.2 φ A = B
2 itgeq12dv.1 φ x A C = D
3 2 fvoveq1d φ x A C i k = D i k
4 3 breq2d φ x A 0 C i k 0 D i k
5 4 pm5.32da φ x A 0 C i k x A 0 D i k
6 1 eleq2d φ x A x B
7 6 anbi1d φ x A 0 D i k x B 0 D i k
8 5 7 bitrd φ x A 0 C i k x B 0 D i k
9 3 adantrr φ x A 0 C i k C i k = D i k
10 eqidd φ ¬ x A 0 C i k 0 = 0
11 8 9 10 ifbieq12d2 φ if x A 0 C i k C i k 0 = if x B 0 D i k D i k 0
12 11 mpteq2dv φ x if x A 0 C i k C i k 0 = x if x B 0 D i k D i k 0
13 12 fveq2d φ 2 x if x A 0 C i k C i k 0 = 2 x if x B 0 D i k D i k 0
14 13 oveq2d φ i k 2 x if x A 0 C i k C i k 0 = i k 2 x if x B 0 D i k D i k 0
15 14 sumeq2sdv φ k = 0 3 i k 2 x if x A 0 C i k C i k 0 = k = 0 3 i k 2 x if x B 0 D i k D i k 0
16 eqid C i k = C i k
17 16 dfitg A C dx = k = 0 3 i k 2 x if x A 0 C i k C i k 0
18 eqid D i k = D i k
19 18 dfitg B D dx = k = 0 3 i k 2 x if x B 0 D i k D i k 0
20 15 17 19 3eqtr4g φ A C dx = B D dx