Metamath Proof Explorer

Theorem eleesubd

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

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

Proof

Step Hyp Ref Expression
1 eleesubd.1 
 |-  ( ph -> C = ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) )
2 1 3ad2ant1 
 |-  ( ( ph /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> C = ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) )
3 fveere 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
4 fveere 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
5 resubcl 
 |-  ( ( ( A ` i ) e. RR /\ ( B ` i ) e. RR ) -> ( ( A ` i ) - ( B ` i ) ) e. RR )
6 3 4 5 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) /\ ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) ) -> ( ( A ` i ) - ( B ` i ) ) e. RR )
7 6 anandirs 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) - ( B ` i ) ) e. RR )
8 7 ralrimiva 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A. i e. ( 1 ... N ) ( ( A ` i ) - ( B ` i ) ) e. RR )
9 eleenn 
 |-  ( A e. ( EE ` N ) -> N e. NN )
10 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 ) )
11 9 10 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 ) )
12 11 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 ) )
13 8 12 mpbird 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) e. ( EE ` N ) )
14 13 3adant1 
 |-  ( ( ph /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) e. ( EE ` N ) )
15 2 14 eqeltrd 
 |-  ( ( ph /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> C e. ( EE ` N ) )