Step |
Hyp |
Ref |
Expression |
1 |
|
ovex |
⊢ ( 0 [,] 1 ) ∈ V |
2 |
|
ovex |
⊢ ( 𝐴 [,] 𝐵 ) ∈ V |
3 |
|
eqid |
⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ) |
4 |
3
|
iccf1o |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ) : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) ∧ ◡ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ) = ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) ) ) |
5 |
4
|
simpld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ) : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) ) |
6 |
|
f1oen2g |
⊢ ( ( ( 0 [,] 1 ) ∈ V ∧ ( 𝐴 [,] 𝐵 ) ∈ V ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ) : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) ) → ( 0 [,] 1 ) ≈ ( 𝐴 [,] 𝐵 ) ) |
7 |
1 2 5 6
|
mp3an12i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 0 [,] 1 ) ≈ ( 𝐴 [,] 𝐵 ) ) |