Theorem rr3fv1cld

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

	Ref	Expression
Hypothesis	rr3fvd.1	|- ( ph -> A e. ( RR ^m ( 1 ... 3 ) ) )
Assertion	rr3fv1cld	|- ( ph -> ( A ` 1 ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		rr3fvd.1	|- ( ph -> 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	syl	|- ( ph -> ( ( A ` 1 ) e. RR /\ ( A ` 2 ) e. RR /\ ( A ` 3 ) e. RR ) )
4	3	simp1d	|- ( ph -> ( A ` 1 ) e. RR )