Metamath Proof Explorer

Theorem hoidifhspval

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 hoidifhspval.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 ) ) ) ) )
hoidifhspval.y 
|- ( ph -> Y e. RR )
Assertion hoidifhspval 
|- ( ph -> ( D ` Y ) = ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoidifhspval.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 hoidifhspval.y 
 |-  ( ph -> Y e. RR )
3 breq1 
 |-  ( x = Y -> ( x <_ ( a ` k ) <-> Y <_ ( a ` k ) ) )
4 id 
 |-  ( x = Y -> x = Y )
5 3 4 ifbieq2d 
 |-  ( x = Y -> if ( x <_ ( a ` k ) , ( a ` k ) , x ) = if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) )
6 5 ifeq1d 
 |-  ( x = Y -> if ( k = K , if ( x <_ ( a ` k ) , ( a ` k ) , x ) , ( a ` k ) ) = if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) )
7 6 mpteq2dv 
 |-  ( x = Y -> ( k e. X |-> if ( k = K , if ( x <_ ( a ` k ) , ( a ` k ) , x ) , ( a ` k ) ) ) = ( k e. X |-> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) ) )
8 7 mpteq2dv 
 |-  ( x = Y -> ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( x <_ ( a ` k ) , ( a ` k ) , x ) , ( a ` k ) ) ) ) = ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) ) ) )
9 ovex 
 |-  ( RR ^m X ) e. _V
10 9 mptex 
 |-  ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) ) ) e. _V
11 10 a1i 
 |-  ( ph -> ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) ) ) e. _V )
12 1 8 2 11 fvmptd3 
 |-  ( ph -> ( D ` Y ) = ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) ) ) )