Theorem rr3fv1cli

Description: First component of a 3-dimensional real coordinate vector is real. (Contributed by Jiamin Zhao, 31-Jul-2026)

	Ref	Expression
Hypothesis	rr3fv.1	⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) )
Assertion	rr3fv1cli	⊢ ( 𝐴 ‘ 1 ) ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		rr3fv.1	⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) )
2		rr3fvcl	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( ( 𝐴 ‘ 1 ) ∈ ℝ ∧ ( 𝐴 ‘ 2 ) ∈ ℝ ∧ ( 𝐴 ‘ 3 ) ∈ ℝ ) )
3	1 2	ax-mp	⊢ ( ( 𝐴 ‘ 1 ) ∈ ℝ ∧ ( 𝐴 ‘ 2 ) ∈ ℝ ∧ ( 𝐴 ‘ 3 ) ∈ ℝ )
4	3	simp1i	⊢ ( 𝐴 ‘ 1 ) ∈ ℝ