Theorem crosspcle2d

Description: Closure of the second 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	crosspcle2d	$$⊢\phi \to A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\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	rr3fv3cld	$$⊢\phi \to A\left(3\right)\in ℝ$$
4	2	rr3fv1cld	$$⊢\phi \to B\left(1\right)\in ℝ$$
5	3 4	remulcld	$$⊢\phi \to A\left(3\right)B\left(1\right)\in ℝ$$
6	1	rr3fv1cld	$$⊢\phi \to A\left(1\right)\in ℝ$$
7	2	rr3fv3cld	$$⊢\phi \to B\left(3\right)\in ℝ$$
8	6 7	remulcld	$$⊢\phi \to A\left(1\right)B\left(3\right)\in ℝ$$
9	5 8	resubcld	$$⊢\phi \to A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right)\in ℝ$$