Metamath Proof Explorer

Theorem hoidifhspval3

Description: D is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoidifhspval3.d 
|- D = ( x e. RR |-> ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( x <_ ( a ` k ) , ( a ` k ) , x ) , ( a ` k ) ) ) ) )
hoidifhspval3.y 
|- ( ph -> Y e. RR )
hoidifhspval3.x 
|- ( ph -> X e. V )
hoidifhspval3.a 
|- ( ph -> A : X --> RR )
hoidifhspval3.j 
|- ( ph -> J e. X )
Assertion hoidifhspval3 
|- ( ph -> ( ( ( D ` Y ) ` A ) ` J ) = if ( J = K , if ( Y <_ ( A ` J ) , ( A ` J ) , Y ) , ( A ` J ) ) )

Proof

Step Hyp Ref Expression
1 hoidifhspval3.d 
 |-  D = ( x e. RR |-> ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( x <_ ( a ` k ) , ( a ` k ) , x ) , ( a ` k ) ) ) ) )
2 hoidifhspval3.y 
 |-  ( ph -> Y e. RR )
3 hoidifhspval3.x 
 |-  ( ph -> X e. V )
4 hoidifhspval3.a 
 |-  ( ph -> A : X --> RR )
5 hoidifhspval3.j 
 |-  ( ph -> J e. X )
6 1 2 3 4 hoidifhspval2 
 |-  ( ph -> ( ( D ` Y ) ` A ) = ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) )
7 eqeq1 
 |-  ( k = J -> ( k = K <-> J = K ) )
8 fveq2 
 |-  ( k = J -> ( A ` k ) = ( A ` J ) )
9 8 breq2d 
 |-  ( k = J -> ( Y <_ ( A ` k ) <-> Y <_ ( A ` J ) ) )
10 9 8 ifbieq1d 
 |-  ( k = J -> if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) = if ( Y <_ ( A ` J ) , ( A ` J ) , Y ) )
11 7 10 8 ifbieq12d 
 |-  ( k = J -> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) = if ( J = K , if ( Y <_ ( A ` J ) , ( A ` J ) , Y ) , ( A ` J ) ) )
12 11 adantl 
 |-  ( ( ph /\ k = J ) -> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) = if ( J = K , if ( Y <_ ( A ` J ) , ( A ` J ) , Y ) , ( A ` J ) ) )
13 fvexd 
 |-  ( ph -> ( A ` J ) e. _V )
14 2 elexd 
 |-  ( ph -> Y e. _V )
15 13 14 ifcld 
 |-  ( ph -> if ( Y <_ ( A ` J ) , ( A ` J ) , Y ) e. _V )
16 15 13 ifcld 
 |-  ( ph -> if ( J = K , if ( Y <_ ( A ` J ) , ( A ` J ) , Y ) , ( A ` J ) ) e. _V )
17 6 12 5 16 fvmptd 
 |-  ( ph -> ( ( ( D ` Y ) ` A ) ` J ) = if ( J = K , if ( Y <_ ( A ` J ) , ( A ` J ) , Y ) , ( A ` J ) ) )