This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ditgeq3d

Description: Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ditgeq3d.1 
|- ( ph -> A <_ B )
ditgeq3d.2 
|- ( ( ph /\ x e. ( A (,) B ) ) -> D = E )
Assertion ditgeq3d 
|- ( ph -> S_ [ A -> B ] D _d x = S_ [ A -> B ] E _d x )

Proof

Step Hyp Ref Expression
1 ditgeq3d.1 
 |-  ( ph -> A <_ B )
2 ditgeq3d.2 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> D = E )
3 df-ditg 
 |-  S_ [ A -> B ] D _d x = if ( A <_ B , S. ( A (,) B ) D _d x , -u S. ( B (,) A ) D _d x )
4 1 iftrued 
 |-  ( ph -> if ( A <_ B , S. ( A (,) B ) D _d x , -u S. ( B (,) A ) D _d x ) = S. ( A (,) B ) D _d x )
5 3 4 eqtrid 
 |-  ( ph -> S_ [ A -> B ] D _d x = S. ( A (,) B ) D _d x )
6 2 itgeq2dv 
 |-  ( ph -> S. ( A (,) B ) D _d x = S. ( A (,) B ) E _d x )
7 df-ditg 
 |-  S_ [ A -> B ] E _d x = if ( A <_ B , S. ( A (,) B ) E _d x , -u S. ( B (,) A ) E _d x )
8 1 iftrued 
 |-  ( ph -> if ( A <_ B , S. ( A (,) B ) E _d x , -u S. ( B (,) A ) E _d x ) = S. ( A (,) B ) E _d x )
9 7 8 eqtr2id 
 |-  ( ph -> S. ( A (,) B ) E _d x = S_ [ A -> B ] E _d x )
10 5 6 9 3eqtrd 
 |-  ( ph -> S_ [ A -> B ] D _d x = S_ [ A -> B ] E _d x )