Metamath Proof Explorer

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 
|- ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( ( A ` 1 ) e. RR /\ ( A ` 2 ) e. RR /\ ( A ` 3 ) e. RR ) )

Proof

Step Hyp Ref Expression
1 elmapi 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> A : ( 1 ... 3 ) --> RR )
2 1elfz13 
 |-  1 e. ( 1 ... 3 )
3 2 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> 1 e. ( 1 ... 3 ) )
4 1 3 ffvelcdmd 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( A ` 1 ) e. RR )
5 2elfz13 
 |-  2 e. ( 1 ... 3 )
6 5 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> 2 e. ( 1 ... 3 ) )
7 1 6 ffvelcdmd 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( A ` 2 ) e. RR )
8 3elfz13 
 |-  3 e. ( 1 ... 3 )
9 8 a1i 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> 3 e. ( 1 ... 3 ) )
10 1 9 ffvelcdmd 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( A ` 3 ) e. RR )
11 4 7 10 3jca 
 |-  ( A e. ( RR ^m ( 1 ... 3 ) ) -> ( ( A ` 1 ) e. RR /\ ( A ` 2 ) e. RR /\ ( A ` 3 ) e. RR ) )