Metamath Proof Explorer


Theorem subrfv

Description: Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012)

Ref Expression
Assertion subrfv ( ( 𝐴𝐸𝐵𝐷𝐶 ∈ ℝ ) → ( ( 𝐴 -𝑟 𝐵 ) ‘ 𝐶 ) = ( ( 𝐴𝐶 ) − ( 𝐵𝐶 ) ) )

Proof

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 ( ( 𝐴𝐸𝐵𝐷𝐶 ∈ ℝ ) → ( ( 𝐴 -𝑟 𝐵 ) ‘ 𝐶 ) = ( ( 𝐴𝐶 ) − ( 𝐵𝐶 ) ) )