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=\left(x\in ℝ⟼\left(a\in \left({ℝ}^X\right)⟼\left(k\in X⟼if\left(k=K,if\left(x\le a\left(k\right),a\left(k\right),x\right),a\left(k\right)\right)\right)\right)\right)$$
	hoidifhspf.y	$$⊢\phi \to Y\in ℝ$$
	hoidifhspf.x	$$⊢\phi \to X\in V$$
	hoidifhspf.a	$$⊢\phi \to A:X⟶ℝ$$
Assertion	hoidifhspf	$$⊢\phi \to D\left(Y\right)\left(A\right):X⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		hoidifhspf.d	$$⊢D=\left(x\in ℝ⟼\left(a\in \left({ℝ}^X\right)⟼\left(k\in X⟼if\left(k=K,if\left(x\le a\left(k\right),a\left(k\right),x\right),a\left(k\right)\right)\right)\right)\right)$$
2		hoidifhspf.y	$$⊢\phi \to Y\in ℝ$$
3		hoidifhspf.x	$$⊢\phi \to X\in V$$
4		hoidifhspf.a	$$⊢\phi \to A:X⟶ℝ$$
5	4	ffvelrnda	$$⊢\left(\phi \wedge k\in X\right)\to A\left(k\right)\in ℝ$$
6	2	adantr	$$⊢\left(\phi \wedge k\in X\right)\to Y\in ℝ$$
7	5 6	ifcld	$$⊢\left(\phi \wedge k\in X\right)\to if\left(Y\le A\left(k\right),A\left(k\right),Y\right)\in ℝ$$
8	7 5	ifcld	$$⊢\left(\phi \wedge k\in X\right)\to if\left(k=K,if\left(Y\le A\left(k\right),A\left(k\right),Y\right),A\left(k\right)\right)\in ℝ$$
9	8	fmpttd	$$⊢\phi \to \left(k\in X⟼if\left(k=K,if\left(Y\le A\left(k\right),A\left(k\right),Y\right),A\left(k\right)\right)\right):X⟶ℝ$$
10	1 2 3 4	hoidifhspval2	$$⊢\phi \to D\left(Y\right)\left(A\right)=\left(k\in X⟼if\left(k=K,if\left(Y\le A\left(k\right),A\left(k\right),Y\right),A\left(k\right)\right)\right)$$
11	10	feq1d	$$⊢\phi \to \left(D\left(Y\right)\left(A\right):X⟶ℝ\leftrightarrow \left(k\in X⟼if\left(k=K,if\left(Y\le A\left(k\right),A\left(k\right),Y\right),A\left(k\right)\right)\right):X⟶ℝ\right)$$
12	9 11	mpbird	$$⊢\phi \to D\left(Y\right)\left(A\right):X⟶ℝ$$