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 e. ( RR ^m ( 1 ... 3 ) )
	crossp.2	|- B e. ( RR ^m ( 1 ... 3 ) )
Assertion	crosspclifi	|- if ( k = 1 , ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) , if ( k = 2 , ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) ) e. RR

Proof

Step	Hyp	Ref	Expression
1		crossp.1	|- A e. ( RR ^m ( 1 ... 3 ) )
2		crossp.2	|- B e. ( RR ^m ( 1 ... 3 ) )
3	1 2	crosspcle1i	|- ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) e. RR
4	1 2	crosspcle2i	|- ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) e. RR
5	1 2	crosspcle3i	|- ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) e. RR
6	4 5	ifcli	|- if ( k = 2 , ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) e. RR
7	3 6	ifcli	|- if ( k = 1 , ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) , if ( k = 2 , ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) ) e. RR