Theorem crosspcle1d

Description: Closure of the first component of the cross product's coordinate formula. (Contributed by Jiamin Zhao, 11-Aug-2026)

	Ref	Expression
Hypotheses	crosspcled.1	$$⊢\phi \to A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crosspcled.2	$$⊢\phi \to B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	crosspcle1d	$$⊢\phi \to A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		crosspcled.1	$$⊢\phi \to A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crosspcled.2	$$⊢\phi \to B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3	1	rr3fv2cld	$$⊢\phi \to A\left(2\right)\in ℝ$$
4	2	rr3fv3cld	$$⊢\phi \to B\left(3\right)\in ℝ$$
5	3 4	remulcld	$$⊢\phi \to A\left(2\right)B\left(3\right)\in ℝ$$
6	1	rr3fv3cld	$$⊢\phi \to A\left(3\right)\in ℝ$$
7	2	rr3fv2cld	$$⊢\phi \to B\left(2\right)\in ℝ$$
8	6 7	remulcld	$$⊢\phi \to A\left(3\right)B\left(2\right)\in ℝ$$
9	5 8	resubcld	$$⊢\phi \to A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right)\in ℝ$$