Theorem crosspcle1i

Description: Closure of the first component of the cross product's Sarrus expansion. (A helper for crosspclifi and crosspv1i .) (Contributed by Jiamin Zhao, 31-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		crosspcle.1	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crosspcle.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3	1	rr3fv2cli	$$⊢A\left(2\right)\in ℝ$$
4	2	rr3fv3cli	$$⊢B\left(3\right)\in ℝ$$
5	3 4	remulcli	$$⊢A\left(2\right)B\left(3\right)\in ℝ$$
6	1	rr3fv3cli	$$⊢A\left(3\right)\in ℝ$$
7	2	rr3fv2cli	$$⊢B\left(2\right)\in ℝ$$
8	6 7	remulcli	$$⊢A\left(3\right)B\left(2\right)\in ℝ$$
9	5 8	resubcli	$$⊢A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right)\in ℝ$$