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 biimpi ⊢ ( 𝑥 = 𝐶 → 𝐶 = 𝑥 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐶 = 𝑥 )
18 14 17 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐴 < 𝑥 )
19 7 18 gtned ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 ≠ 𝐴 )
20 19 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → ¬ 𝑥 = 𝐴 )
21 20 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 = 𝐶 )
23 5 elioored ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐶 ∈ ℝ )
25 22 24 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 ∈ ℝ )
26 12 simp3d ⊢ ( 𝜑 → 𝐶 < 𝐵 )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐶 < 𝐵 )
28 22 27 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 < 𝐵 )
29 25 28 ltned ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝑥 ≠ 𝐵 )
30 29 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → ¬ 𝑥 = 𝐵 )
31 30 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
32 22 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐶 ) )
33 21 31 32 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝐶 ) )
34 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
35 34 5 sseldi ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
36 3 5 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ 𝑉 )
37 6 33 35 36 fvmptd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )