Theorem hoidifhspval2

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	hoidifhspval2.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 ) ) ) ) )
	hoidifhspval2.y	|- ( ph -> Y e. RR )
	hoidifhspval2.x	|- ( ph -> X e. V )
	hoidifhspval2.a	|- ( ph -> A : X --> RR )
Assertion	hoidifhspval2	|- ( ph -> ( ( D ` Y ) ` A ) = ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hoidifhspval2.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		hoidifhspval2.y	|- ( ph -> Y e. RR )
3		hoidifhspval2.x	|- ( ph -> X e. V )
4		hoidifhspval2.a	|- ( ph -> A : X --> RR )
5	1 2	hoidifhspval	|- ( ph -> ( D ` Y ) = ( a e. ( RR ^m X ) |-> ( k e. X |-> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) ) ) )
6		fveq1	|- ( a = A -> ( a ` k ) = ( A ` k ) )
7	6	breq2d	|- ( a = A -> ( Y <_ ( a ` k ) <-> Y <_ ( A ` k ) ) )
8	7 6	ifbieq1d	|- ( a = A -> if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) = if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) )
9	8 6	ifeq12d	|- ( a = A -> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) = if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) )
10	9	mpteq2dv	|- ( a = A -> ( k e. X |-> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) ) = ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) )
11	10	adantl	|- ( ( ph /\ a = A ) -> ( k e. X |-> if ( k = K , if ( Y <_ ( a ` k ) , ( a ` k ) , Y ) , ( a ` k ) ) ) = ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) )
12		reex	|- RR e. _V
13	12	a1i	|- ( ph -> RR e. _V )
14	13 3	jca	|- ( ph -> ( RR e. _V /\ X e. V ) )
15		elmapg	|- ( ( RR e. _V /\ X e. V ) -> ( A e. ( RR ^m X ) <-> A : X --> RR ) )
16	14 15	syl	|- ( ph -> ( A e. ( RR ^m X ) <-> A : X --> RR ) )
17	4 16	mpbird	|- ( ph -> A e. ( RR ^m X ) )
18		mptexg	|- ( X e. V -> ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) e. _V )
19	3 18	syl	|- ( ph -> ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) e. _V )
20	5 11 17 19	fvmptd	|- ( ph -> ( ( D ` Y ) ` A ) = ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) )