Step |
Hyp |
Ref |
Expression |
1 |
|
subrval |
⊢ ( ( 𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 -𝑟 𝐵 ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑥 ) − ( 𝐵 ‘ 𝑥 ) ) ) ) |
2 |
1
|
fveq1d |
⊢ ( ( 𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ) → ( ( 𝐴 -𝑟 𝐵 ) ‘ 𝐶 ) = ( ( 𝑥 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑥 ) − ( 𝐵 ‘ 𝑥 ) ) ) ‘ 𝐶 ) ) |
3 |
|
fveq2 |
⊢ ( 𝑥 = 𝐶 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝐶 ) ) |
4 |
|
fveq2 |
⊢ ( 𝑥 = 𝐶 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝐶 ) ) |
5 |
3 4
|
oveq12d |
⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ‘ 𝑥 ) − ( 𝐵 ‘ 𝑥 ) ) = ( ( 𝐴 ‘ 𝐶 ) − ( 𝐵 ‘ 𝐶 ) ) ) |
6 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑥 ) − ( 𝐵 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑥 ) − ( 𝐵 ‘ 𝑥 ) ) ) |
7 |
|
ovex |
⊢ ( ( 𝐴 ‘ 𝐶 ) − ( 𝐵 ‘ 𝐶 ) ) ∈ V |
8 |
5 6 7
|
fvmpt |
⊢ ( 𝐶 ∈ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑥 ) − ( 𝐵 ‘ 𝑥 ) ) ) ‘ 𝐶 ) = ( ( 𝐴 ‘ 𝐶 ) − ( 𝐵 ‘ 𝐶 ) ) ) |
9 |
2 8
|
sylan9eq |
⊢ ( ( ( 𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 -𝑟 𝐵 ) ‘ 𝐶 ) = ( ( 𝐴 ‘ 𝐶 ) − ( 𝐵 ‘ 𝐶 ) ) ) |
10 |
9
|
3impa |
⊢ ( ( 𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 -𝑟 𝐵 ) ‘ 𝐶 ) = ( ( 𝐴 ‘ 𝐶 ) − ( 𝐵 ‘ 𝐶 ) ) ) |