Theorem eleesub

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

	Ref	Expression
Hypothesis	eleesub.1	⊢ 𝐶 = ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) )
Assertion	eleesub	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eleesub.1	⊢ 𝐶 = ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) )
2		fveere	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
3		fveere	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
4		resubcl	⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℝ ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
5	2 3 4	syl2an	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
6	5	anandirs	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
7	6	ralrimiva	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
8		eleenn	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )
9		mptelee	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ ) )
10	8 9	syl	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ ) )
11	10	adantr	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ ) )
12	7 11	mpbird	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
13	1 12	eqeltrid	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )