Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 hoidifhspval2.d ⊢ 𝐷 = ( 𝑥 ∈ ℝ ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑥 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) )
2 hoidifhspval2.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3 hoidifhspval2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4 hoidifhspval2.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
5 1 2 hoidifhspval ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑌 ) = ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) )
6 fveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
7 6 breq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) ↔ 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) ) )
8 7 6 ifbieq1d ⊢ ( 𝑎 = 𝐴 → if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) = if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) )
9 8 6 ifeq12d ⊢ ( 𝑎 = 𝐴 → if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) = if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) )
10 9 mpteq2dv ⊢ ( 𝑎 = 𝐴 → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) ) )
12 reex ⊢ ℝ ∈ V
13 12 a1i ⊢ ( 𝜑 → ℝ ∈ V )
14 13 3 jca ⊢ ( 𝜑 → ( ℝ ∈ V ∧ 𝑋 ∈ 𝑉 ) )
15 elmapg ⊢ ( ( ℝ ∈ V ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 ∈ ( ℝ ↑m 𝑋 ) ↔ 𝐴 : 𝑋 ⟶ ℝ ) )
16 14 15 syl ⊢ ( 𝜑 → ( 𝐴 ∈ ( ℝ ↑m 𝑋 ) ↔ 𝐴 : 𝑋 ⟶ ℝ ) )
17 4 16 mpbird ⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m 𝑋 ) )
18 mptexg ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) ) ∈ V )
19 3 18 syl ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) ) ∈ V )
20 5 11 17 19 fvmptd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑌 ) ‘ 𝐴 ) = ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝐴 ‘ 𝑘 ) , ( 𝐴 ‘ 𝑘 ) , 𝑌 ) , ( 𝐴 ‘ 𝑘 ) ) ) )