Metamath Proof Explorer


Theorem itgeq1f

Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014) Avoid axioms. (Revised by GG, 1-Sep-2025)

Ref Expression
Hypotheses itgeq1f.1
|- F/_ x A
itgeq1f.2
|- F/_ x B
Assertion itgeq1f
|- ( A = B -> S. A C _d x = S. B C _d x )

Proof

Step Hyp Ref Expression
1 itgeq1f.1
 |-  F/_ x A
2 itgeq1f.2
 |-  F/_ x B
3 1 2 nfeq
 |-  F/ x A = B
4 eleq2
 |-  ( A = B -> ( x e. A <-> x e. B ) )
5 4 anbi1d
 |-  ( A = B -> ( ( x e. A /\ 0 <_ y ) <-> ( x e. B /\ 0 <_ y ) ) )
6 5 ifbid
 |-  ( A = B -> if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
7 6 csbeq2dv
 |-  ( A = B -> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
8 7 adantr
 |-  ( ( A = B /\ x e. RR ) -> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) = [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) )
9 3 8 mpteq2da
 |-  ( A = B -> ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) = ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) )
10 9 fveq2d
 |-  ( A = B -> ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) = ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) )
11 10 oveq2d
 |-  ( A = B -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) ) = ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) ) )
12 11 sumeq2sdv
 |-  ( A = B -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) ) = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) ) )
13 df-itg
 |-  S. A C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) )
14 df-itg
 |-  S. B C _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( C / ( _i ^ k ) ) ) / y ]_ if ( ( x e. B /\ 0 <_ y ) , y , 0 ) ) ) )
15 12 13 14 3eqtr4g
 |-  ( A = B -> S. A C _d x = S. B C _d x )