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 \in (ℝ^{(1 \dots 3)}) \to (A (1) \in ℝ \land A (2) \in ℝ \land A (3) \in ℝ)$

Step	Hyp	Ref	Expression
1		elmapi	$⊢ A \in (ℝ^{(1 \dots 3)}) \to A : (1 \dots 3) ⟶ ℝ$
2		1elfz13	$⊢ 1 \in (1 \dots 3)$
3	2	a1i	$⊢ A \in (ℝ^{(1 \dots 3)}) \to 1 \in (1 \dots 3)$
4	1 3	ffvelcdmd	$⊢ A \in (ℝ^{(1 \dots 3)}) \to A (1) \in ℝ$
5		2elfz13	$⊢ 2 \in (1 \dots 3)$
6	5	a1i	$⊢ A \in (ℝ^{(1 \dots 3)}) \to 2 \in (1 \dots 3)$
7	1 6	ffvelcdmd	$⊢ A \in (ℝ^{(1 \dots 3)}) \to A (2) \in ℝ$
8		3elfz13	$⊢ 3 \in (1 \dots 3)$
9	8	a1i	$⊢ A \in (ℝ^{(1 \dots 3)}) \to 3 \in (1 \dots 3)$
10	1 9	ffvelcdmd	$⊢ A \in (ℝ^{(1 \dots 3)}) \to A (3) \in ℝ$
11	4 7 10	3jca	$⊢ A \in (ℝ^{(1 \dots 3)}) \to (A (1) \in ℝ \land A (2) \in ℝ \land A (3) \in ℝ)$

Metamath Proof Explorer