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	⊢ 𝐷 = ( 𝑥 ∈ ℝ ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑥 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) )
	hoidifhspval3.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	hoidifhspval3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	hoidifhspval3.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
	hoidifhspval3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑋 )
Assertion	hoidifhspval3	⊢ ( 𝜑 → ( ( ( 𝐷 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐽 ) = if ( 𝐽 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝐽 ) , ( 𝐴 ‘ 𝐽 ) , 𝑌 ) , ( 𝐴 ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hoidifhspval3.d	⊢ 𝐷 = ( 𝑥 ∈ ℝ ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑥 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) )
2		hoidifhspval3.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3		hoidifhspval3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4		hoidifhspval3.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
5		hoidifhspval3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑋 )
6	1 2 3 4	hoidifhspval2	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑌 ) ‘ 𝐴 ) = ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) ) )
7		eqeq1	⊢ ( 𝑘 = 𝐽 → ( 𝑘 = 𝐾 ↔ 𝐽 = 𝐾 ) )
8		fveq2	⊢ ( 𝑘 = 𝐽 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝐽 ) )
9	8	breq2d	⊢ ( 𝑘 = 𝐽 → ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) ↔ 𝑌 ≤ ( 𝐴 ‘ 𝐽 ) ) )
10	9 8	ifbieq1d	⊢ ( 𝑘 = 𝐽 → if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) = if ( 𝑌 ≤ ( 𝐴 ‘ 𝐽 ) , ( 𝐴 ‘ 𝐽 ) , 𝑌 ) )
11	7 10 8	ifbieq12d	⊢ ( 𝑘 = 𝐽 → if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) = if ( 𝐽 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝐽 ) , ( 𝐴 ‘ 𝐽 ) , 𝑌 ) , ( 𝐴 ‘ 𝐽 ) ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐽 ) → if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) = if ( 𝐽 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝐽 ) , ( 𝐴 ‘ 𝐽 ) , 𝑌 ) , ( 𝐴 ‘ 𝐽 ) ) )
13		fvexd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐽 ) ∈ V )
14	2	elexd	⊢ ( 𝜑 → 𝑌 ∈ V )
15	13 14	ifcld	⊢ ( 𝜑 → if ( 𝑌 ≤ ( 𝐴 ‘ 𝐽 ) , ( 𝐴 ‘ 𝐽 ) , 𝑌 ) ∈ V )
16	15 13	ifcld	⊢ ( 𝜑 → if ( 𝐽 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝐽 ) , ( 𝐴 ‘ 𝐽 ) , 𝑌 ) , ( 𝐴 ‘ 𝐽 ) ) ∈ V )
17	6 12 5 16	fvmptd	⊢ ( 𝜑 → ( ( ( 𝐷 ‘ 𝑌 ) ‘ 𝐴 ) ‘ 𝐽 ) = if ( 𝐽 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝐽 ) , ( 𝐴 ‘ 𝐽 ) , 𝑌 ) , ( 𝐴 ‘ 𝐽 ) ) )