Theorem crosspclifi

Description: Closure of the three-way Sarrus case split used in the cross product's mapping rule. (A helper for crosspcli .) (Contributed by Jiamin Zhao, 1-Aug-2026)

	Ref	Expression
Hypotheses	crossp.1	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crossp.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	crosspclifi	$$⊢if\left(k=1,A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right),if\left(k=2,A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right),A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)\right)\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		crossp.1	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crossp.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3	1 2	crosspcle1i	$$⊢A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right)\in ℝ$$
4	1 2	crosspcle2i	$$⊢A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right)\in ℝ$$
5	1 2	crosspcle3i	$$⊢A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)\in ℝ$$
6	4 5	ifcli	$$⊢if\left(k=2,A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right),A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)\right)\in ℝ$$
7	3 6	ifcli	$$⊢if\left(k=1,A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right),if\left(k=2,A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right),A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)\right)\right)\in ℝ$$