Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Andrew Salmon
Geometry
subrfn
Next ⟩
mulvfn
Metamath Proof Explorer
Ascii
Unicode
Theorem
subrfn
Description:
Vector subtraction produces a function.
(Contributed by
Andrew Salmon
, 27-Jan-2012)
Ref
Expression
Assertion
subrfn
⊢
A
∈
C
∧
B
∈
D
→
A
-
r
B
Fn
ℝ
Proof
Step
Hyp
Ref
Expression
1
ovex
⊢
A
⁡
x
−
B
⁡
x
∈
V
2
eqid
⊢
x
∈
ℝ
⟼
A
⁡
x
−
B
⁡
x
=
x
∈
ℝ
⟼
A
⁡
x
−
B
⁡
x
3
1
2
fnmpti
⊢
x
∈
ℝ
⟼
A
⁡
x
−
B
⁡
x
Fn
ℝ
4
subrval
⊢
A
∈
C
∧
B
∈
D
→
A
-
r
B
=
x
∈
ℝ
⟼
A
⁡
x
−
B
⁡
x
5
4
fneq1d
⊢
A
∈
C
∧
B
∈
D
→
A
-
r
B
Fn
ℝ
↔
x
∈
ℝ
⟼
A
⁡
x
−
B
⁡
x
Fn
ℝ
6
3
5
mpbiri
⊢
A
∈
C
∧
B
∈
D
→
A
-
r
B
Fn
ℝ