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	⊢ ( 𝜑 → 𝐶 = ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) )
Assertion	eleesubd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )

Proof

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