Theorem hoidifhspval3

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

Proof

Step	Hyp	Ref	Expression
1		hoidifhspval3.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		hoidifhspval3.y	$$⊢\phi \to Y\in ℝ$$
3		hoidifhspval3.x	$$⊢\phi \to X\in V$$
4		hoidifhspval3.a	$$⊢\phi \to A:X⟶ℝ$$
5		hoidifhspval3.j	$$⊢\phi \to J\in X$$
6	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)$$
7		eqeq1	$$⊢k=J\to \left(k=K\leftrightarrow J=K\right)$$
8		fveq2	$$⊢k=J\to A\left(k\right)=A\left(J\right)$$
9	8	breq2d	$$⊢k=J\to \left(Y\le A\left(k\right)\leftrightarrow Y\le A\left(J\right)\right)$$
10	9 8	ifbieq1d	$$⊢k=J\to if\left(Y\le A\left(k\right),A\left(k\right),Y\right)=if\left(Y\le A\left(J\right),A\left(J\right),Y\right)$$
11	7 10 8	ifbieq12d	$$⊢k=J\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(J=K,if\left(Y\le A\left(J\right),A\left(J\right),Y\right),A\left(J\right)\right)$$
12	11	adantl	$$⊢\left(\phi \wedge k=J\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)=if\left(J=K,if\left(Y\le A\left(J\right),A\left(J\right),Y\right),A\left(J\right)\right)$$
13		fvexd	$$⊢\phi \to A\left(J\right)\in \mathrm{V}$$
14	2	elexd	$$⊢\phi \to Y\in \mathrm{V}$$
15	13 14	ifcld	$$⊢\phi \to if\left(Y\le A\left(J\right),A\left(J\right),Y\right)\in \mathrm{V}$$
16	15 13	ifcld	$$⊢\phi \to if\left(J=K,if\left(Y\le A\left(J\right),A\left(J\right),Y\right),A\left(J\right)\right)\in \mathrm{V}$$
17	6 12 5 16	fvmptd	$$⊢\phi \to D\left(Y\right)\left(A\right)\left(J\right)=if\left(J=K,if\left(Y\le A\left(J\right),A\left(J\right),Y\right),A\left(J\right)\right)$$