Theorem hoidifhspf

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	hoidifhspf.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 ) ) ) ) )
	hoidifhspf.y	|- ( ph -> Y e. RR )
	hoidifhspf.x	|- ( ph -> X e. V )
	hoidifhspf.a	|- ( ph -> A : X --> RR )
Assertion	hoidifhspf	|- ( ph -> ( ( D ` Y ) ` A ) : X --> RR )

Proof

Step	Hyp	Ref	Expression
1		hoidifhspf.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		hoidifhspf.y	|- ( ph -> Y e. RR )
3		hoidifhspf.x	|- ( ph -> X e. V )
4		hoidifhspf.a	|- ( ph -> A : X --> RR )
5	4	ffvelrnda	|- ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
6	2	adantr	|- ( ( ph /\ k e. X ) -> Y e. RR )
7	5 6	ifcld	|- ( ( ph /\ k e. X ) -> if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) e. RR )
8	7 5	ifcld	|- ( ( ph /\ k e. X ) -> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) e. RR )
9	8	fmpttd	|- ( ph -> ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) : X --> RR )
10	1 2 3 4	hoidifhspval2	|- ( ph -> ( ( D ` Y ) ` A ) = ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) )
11	10	feq1d	|- ( ph -> ( ( ( D ` Y ) ` A ) : X --> RR <-> ( k e. X |-> if ( k = K , if ( Y <_ ( A ` k ) , ( A ` k ) , Y ) , ( A ` k ) ) ) : X --> RR ) )
12	9 11	mpbird	|- ( ph -> ( ( D ` Y ) ` A ) : X --> RR )