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 ) )