Metamath Proof Explorer


Theorem eleesub

Description: Membership of a subtraction mapping in a Euclidean space. (Contributed by Scott Fenton, 17-Jul-2013)

Ref Expression
Hypothesis eleesub.1
|- C = ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) )
Assertion eleesub
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> C e. ( EE ` N ) )

Proof

Step Hyp Ref Expression
1 eleesub.1
 |-  C = ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) )
2 fveere
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
3 fveere
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
4 resubcl
 |-  ( ( ( A ` i ) e. RR /\ ( B ` i ) e. RR ) -> ( ( A ` i ) - ( B ` i ) ) e. RR )
5 2 3 4 syl2an
 |-  ( ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) /\ ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) ) -> ( ( A ` i ) - ( B ` i ) ) e. RR )
6 5 anandirs
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) - ( B ` i ) ) e. RR )
7 6 ralrimiva
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A. i e. ( 1 ... N ) ( ( A ` i ) - ( B ` i ) ) e. RR )
8 eleenn
 |-  ( A e. ( EE ` N ) -> N e. NN )
9 mptelee
 |-  ( N e. NN -> ( ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) e. ( EE ` N ) <-> A. i e. ( 1 ... N ) ( ( A ` i ) - ( B ` i ) ) e. RR ) )
10 8 9 syl
 |-  ( A e. ( EE ` N ) -> ( ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) e. ( EE ` N ) <-> A. i e. ( 1 ... N ) ( ( A ` i ) - ( B ` i ) ) e. RR ) )
11 10 adantr
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) e. ( EE ` N ) <-> A. i e. ( 1 ... N ) ( ( A ` i ) - ( B ` i ) ) e. RR ) )
12 7 11 mpbird
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) e. ( EE ` N ) )
13 1 12 eqeltrid
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> C e. ( EE ` N ) )