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

Proof

Step	Hyp	Ref	Expression
1		hoidifhspf.d	⊢ 𝐷 = ( 𝑥 ∈ ℝ ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑥 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) )
2		hoidifhspf.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3		hoidifhspf.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4		hoidifhspf.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
5	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑌 ∈ ℝ )
7	5 6	ifcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) ∈ ℝ )
8	7 5	ifcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
9	8	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ )
10	1 2 3 4	hoidifhspval2	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑌 ) ‘ 𝐴 ) = ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) ) )
11	10	feq1d	⊢ ( 𝜑 → ( ( ( 𝐷 ‘ 𝑌 ) ‘ 𝐴 ) : 𝑋 ⟶ ℝ ↔ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) ) : 𝑋 ⟶ ℝ ) )
12	9 11	mpbird	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑌 ) ‘ 𝐴 ) : 𝑋 ⟶ ℝ )