Description: Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | addrfn | |- ( ( A e. C /\ B e. D ) -> ( A +r B ) Fn RR ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovex | |- ( ( A ` x ) + ( B ` x ) ) e. _V |
|
2 | eqid | |- ( x e. RR |-> ( ( A ` x ) + ( B ` x ) ) ) = ( x e. RR |-> ( ( A ` x ) + ( B ` x ) ) ) |
|
3 | 1 2 | fnmpti | |- ( x e. RR |-> ( ( A ` x ) + ( B ` x ) ) ) Fn RR |
4 | addrval | |- ( ( A e. C /\ B e. D ) -> ( A +r B ) = ( x e. RR |-> ( ( A ` x ) + ( B ` x ) ) ) ) |
|
5 | 4 | fneq1d | |- ( ( A e. C /\ B e. D ) -> ( ( A +r B ) Fn RR <-> ( x e. RR |-> ( ( A ` x ) + ( B ` x ) ) ) Fn RR ) ) |
6 | 3 5 | mpbiri | |- ( ( A e. C /\ B e. D ) -> ( A +r B ) Fn RR ) |