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	|- A e. ( RR ^m ( 1 ... 3 ) )
Assertion	rr3fv1cli	|- ( A ` 1 ) e. RR

Proof

Step	Hyp	Ref	Expression
1		rr3fv.1	|- A e. ( RR ^m ( 1 ... 3 ) )
2		rr3fvcl	|- ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( ( A ` 1 ) e. RR /\ ( A ` 2 ) e. RR /\ ( A ` 3 ) e. RR ) )
3	1 2	ax-mp	|- ( ( A ` 1 ) e. RR /\ ( A ` 2 ) e. RR /\ ( A ` 3 ) e. RR )
4	3	simp1i	|- ( A ` 1 ) e. RR