Theorem rr3fvcl

Description: The components of a 3-dimensional real coordinate vector are real numbers. (Contributed by Jiamin Zhao, 31-Jul-2026)

	Ref	Expression
Assertion	rr3fvcl	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( ( 𝐴 ‘ 1 ) ∈ ℝ ∧ ( 𝐴 ‘ 2 ) ∈ ℝ ∧ ( 𝐴 ‘ 3 ) ∈ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		elmapi	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → 𝐴 : ( 1 ... 3 ) ⟶ ℝ )
2		1elfz13	⊢ 1 ∈ ( 1 ... 3 )
3	2	a1i	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → 1 ∈ ( 1 ... 3 ) )
4	1 3	ffvelcdmd	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝐴 ‘ 1 ) ∈ ℝ )
5		2elfz13	⊢ 2 ∈ ( 1 ... 3 )
6	5	a1i	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → 2 ∈ ( 1 ... 3 ) )
7	1 6	ffvelcdmd	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝐴 ‘ 2 ) ∈ ℝ )
8		3elfz13	⊢ 3 ∈ ( 1 ... 3 )
9	8	a1i	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → 3 ∈ ( 1 ... 3 ) )
10	1 9	ffvelcdmd	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝐴 ‘ 3 ) ∈ ℝ )
11	4 7 10	3jca	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( ( 𝐴 ‘ 1 ) ∈ ℝ ∧ ( 𝐴 ‘ 2 ) ∈ ℝ ∧ ( 𝐴 ‘ 3 ) ∈ ℝ ) )