Theorem crosspcli

Description: Closure of the cross product: the cross product of two 3-dimensional real coordinate vectors is again such a vector. (Contributed by Jiamin Zhao, 31-Jul-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	crosspcli	Could not format assertion : No typesetting found for |- ( A crossp B ) e. ( RR ^m ( 1 ... 3 ) ) with typecode |-

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		crosspval	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ B e. ( RR ^m ( 1 ... 3 ) ) ) -> ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> 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 ) ) ) ) ) ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ B e. ( RR ^m ( 1 ... 3 ) ) ) -> ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> 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 ) ) ) ) ) ) ) with typecode |-
4	1 2 3	mp2an	Could not format ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> 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 ) ) ) ) ) ) : No typesetting found for |- ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> 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 ) ) ) ) ) ) with typecode |-
5	1 2	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 ℝ$$
6	5	a1i	$$⊢\left(A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge k\in \left(1\dots 3\right)\right)\to 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 ℝ$$
7	6	fmpttd	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)\to \left(k\in \left(1\dots 3\right)⟼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)\right):\left(1\dots 3\right)⟶ℝ$$
8	1 7	ax-mp	$$⊢\left(k\in \left(1\dots 3\right)⟼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)\right):\left(1\dots 3\right)⟶ℝ$$
9		reex	$$⊢ℝ\in \mathrm{V}$$
10		ovex	$$⊢\left(1\dots 3\right)\in \mathrm{V}$$
11	9 10	elmap	$$⊢\left(k\in \left(1\dots 3\right)⟼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)\right)\in \left({ℝ}^{\left(1\dots 3\right)}\right)\leftrightarrow \left(k\in \left(1\dots 3\right)⟼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)\right):\left(1\dots 3\right)⟶ℝ$$
12	8 11	mpbir	$$⊢\left(k\in \left(1\dots 3\right)⟼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)\right)\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
13	4 12	eqeltri	Could not format ( A crossp B ) e. ( RR ^m ( 1 ... 3 ) ) : No typesetting found for |- ( A crossp B ) e. ( RR ^m ( 1 ... 3 ) ) with typecode |-