Metamath Proof Explorer

Theorem cncfioobdlem

Description: G actually extends F . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfioobdlem.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
cncfioobdlem.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
cncfioobdlem.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ 𝑉 )
cncfioobdlem.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
cncfioobdlem.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
Assertion cncfioobdlem ( 𝜑 → ( 𝐺 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cncfioobdlem.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 cncfioobdlem.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 cncfioobdlem.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ 𝑉 )
4 cncfioobdlem.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
5 cncfioobdlem.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
6 4 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐴 ∈ ℝ )
8 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
9 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
10 elioo2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
11 8 9 10 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
12 5 11 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) )
13 12 simp2d ⊢ ( 𝜑 → 𝐴 < 𝐶 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐴 < 𝐶 )
15 eqcom ⊢ ( 𝑥 = 𝐶 ↔ 𝐶 = 𝑥 )
16 15 bilani ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐶 = 𝑥 )
17 14 16 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐴 < 𝑥 )
18 7 17 gtned ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 ≠ 𝐴 )
19 18 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → ¬ 𝑥 = 𝐴 )
20 19 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 = 𝐶 )
22 5 elioored ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐶 ∈ ℝ )
24 21 23 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 ∈ ℝ )
25 12 simp3d ⊢ ( 𝜑 → 𝐶 < 𝐵 )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐶 < 𝐵 )
27 21 26 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 < 𝐵 )
28 24 27 ltned ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 ≠ 𝐵 )
29 28 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → ¬ 𝑥 = 𝐵 )
30 29 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
31 21 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐶 ) )
32 20 30 31 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝐶 ) )
33 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
34 33 5 sselid ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
35 3 5 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ 𝑉 )
36 6 32 34 35 fvmptd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )