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=\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)$$
	hoidifhspval2.y	$$⊢\phi \to Y\in ℝ$$
	hoidifhspval2.x	$$⊢\phi \to X\in V$$
	hoidifhspval2.a	$$⊢\phi \to A:X⟶ℝ$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		hoidifhspval2.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		hoidifhspval2.y	$$⊢\phi \to Y\in ℝ$$
3		hoidifhspval2.x	$$⊢\phi \to X\in V$$
4		hoidifhspval2.a	$$⊢\phi \to A:X⟶ℝ$$
5	1 2	hoidifhspval	$$⊢\phi \to D\left(Y\right)=\left(a\in \left({ℝ}^X\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)\right)$$
6		fveq1	$$⊢a=A\to a\left(k\right)=A\left(k\right)$$
7	6	breq2d	$$⊢a=A\to \left(Y\le a\left(k\right)\leftrightarrow Y\le A\left(k\right)\right)$$
8	7 6	ifbieq1d	$$⊢a=A\to if\left(Y\le a\left(k\right),a\left(k\right),Y\right)=if\left(Y\le A\left(k\right),A\left(k\right),Y\right)$$
9	8 6	ifeq12d	$$⊢a=A\to if\left(k=K,if\left(Y\le a\left(k\right),a\left(k\right),Y\right),a\left(k\right)\right)=if\left(k=K,if\left(Y\le A\left(k\right),A\left(k\right),Y\right),A\left(k\right)\right)$$
10	9	mpteq2dv	$$⊢a=A\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)=\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	adantl	$$⊢\left(\phi \wedge a=A\right)\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)=\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)$$
12		reex	$$⊢ℝ\in \mathrm{V}$$
13	12	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
14	13 3	jca	$$⊢\phi \to \left(ℝ\in \mathrm{V}\wedge X\in V\right)$$
15		elmapg	$$⊢\left(ℝ\in \mathrm{V}\wedge X\in V\right)\to \left(A\in \left({ℝ}^X\right)\leftrightarrow A:X⟶ℝ\right)$$
16	14 15	syl	$$⊢\phi \to \left(A\in \left({ℝ}^X\right)\leftrightarrow A:X⟶ℝ\right)$$
17	4 16	mpbird	$$⊢\phi \to A\in \left({ℝ}^X\right)$$
18		mptexg	$$⊢X\in V\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)\in \mathrm{V}$$
19	3 18	syl	$$⊢\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)\in \mathrm{V}$$
20	5 11 17 19	fvmptd	$$⊢\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)$$