Metamath Proof Explorer


Theorem subrval

Description: Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012)

Ref Expression
Assertion subrval ( ( 𝐴𝐶𝐵𝐷 ) → ( 𝐴 -𝑟 𝐵 ) = ( 𝑣 ∈ ℝ ↦ ( ( 𝐴𝑣 ) − ( 𝐵𝑣 ) ) ) )

Proof

Step Hyp Ref Expression
1 elex ( 𝐴𝐶𝐴 ∈ V )
2 elex ( 𝐵𝐷𝐵 ∈ V )
3 fveq1 ( 𝑥 = 𝐴 → ( 𝑥𝑣 ) = ( 𝐴𝑣 ) )
4 fveq1 ( 𝑦 = 𝐵 → ( 𝑦𝑣 ) = ( 𝐵𝑣 ) )
5 3 4 oveqan12d ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ( 𝑥𝑣 ) − ( 𝑦𝑣 ) ) = ( ( 𝐴𝑣 ) − ( 𝐵𝑣 ) ) )
6 5 mpteq2dv ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝑣 ∈ ℝ ↦ ( ( 𝑥𝑣 ) − ( 𝑦𝑣 ) ) ) = ( 𝑣 ∈ ℝ ↦ ( ( 𝐴𝑣 ) − ( 𝐵𝑣 ) ) ) )
7 df-subr -𝑟 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑣 ∈ ℝ ↦ ( ( 𝑥𝑣 ) − ( 𝑦𝑣 ) ) ) )
8 reex ℝ ∈ V
9 8 mptex ( 𝑣 ∈ ℝ ↦ ( ( 𝐴𝑣 ) − ( 𝐵𝑣 ) ) ) ∈ V
10 6 7 9 ovmpoa ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 -𝑟 𝐵 ) = ( 𝑣 ∈ ℝ ↦ ( ( 𝐴𝑣 ) − ( 𝐵𝑣 ) ) ) )
11 1 2 10 syl2an ( ( 𝐴𝐶𝐵𝐷 ) → ( 𝐴 -𝑟 𝐵 ) = ( 𝑣 ∈ ℝ ↦ ( ( 𝐴𝑣 ) − ( 𝐵𝑣 ) ) ) )