Definition df-crossp

Description: Define the cross product of two 3-dimensional real coordinate vectors. Vectors are represented as functions on ( 1 ... 3 ) . (Contributed by Jiamin Zhao, 31-Jul-2026)

	Ref	Expression
Assertion	df-crossp	Could not format assertion : No typesetting found for |- crossp = ( u e. ( RR ^m ( 1 ... 3 ) ) , v e. ( RR ^m ( 1 ... 3 ) ) |-> ( k e. ( 1 ... 3 ) |-> if ( k = 1 , ( ( ( u ` 2 ) x. ( v ` 3 ) ) - ( ( u ` 3 ) x. ( v ` 2 ) ) ) , if ( k = 2 , ( ( ( u ` 3 ) x. ( v ` 1 ) ) - ( ( u ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( u ` 1 ) x. ( v ` 2 ) ) - ( ( u ` 2 ) x. ( v ` 1 ) ) ) ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccrossp	Could not format crossp : No typesetting found for class crossp with typecode class
1		vu	$$setvaru$$
2		cr	$$classℝ$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4		c1	$$class1$$
5		cfz	$$class\dots$$
6		c3	$$class3$$
7	4 6 5	co	$$class\left(1\dots 3\right)$$
8	2 7 3	co	$$class\left({ℝ}^{\left(1\dots 3\right)}\right)$$
9		vv	$$setvarv$$
10		vk	$$setvark$$
11	10	cv	$$setvark$$
12	11 4	wceq	$$wffk=1$$
13	1	cv	$$setvaru$$
14		c2	$$class2$$
15	14 13	cfv	$$classu\left(2\right)$$
16		cmul	$$class\times$$
17	9	cv	$$setvarv$$
18	6 17	cfv	$$classv\left(3\right)$$
19	15 18 16	co	$$classu\left(2\right)v\left(3\right)$$
20		cmin	$$class-$$
21	6 13	cfv	$$classu\left(3\right)$$
22	14 17	cfv	$$classv\left(2\right)$$
23	21 22 16	co	$$classu\left(3\right)v\left(2\right)$$
24	19 23 20	co	$$class\left(u\left(2\right)v\left(3\right)-u\left(3\right)v\left(2\right)\right)$$
25	11 14	wceq	$$wffk=2$$
26	4 17	cfv	$$classv\left(1\right)$$
27	21 26 16	co	$$classu\left(3\right)v\left(1\right)$$
28	4 13	cfv	$$classu\left(1\right)$$
29	28 18 16	co	$$classu\left(1\right)v\left(3\right)$$
30	27 29 20	co	$$class\left(u\left(3\right)v\left(1\right)-u\left(1\right)v\left(3\right)\right)$$
31	28 22 16	co	$$classu\left(1\right)v\left(2\right)$$
32	15 26 16	co	$$classu\left(2\right)v\left(1\right)$$
33	31 32 20	co	$$class\left(u\left(1\right)v\left(2\right)-u\left(2\right)v\left(1\right)\right)$$
34	25 30 33	cif	$$classif\left(k=2,u\left(3\right)v\left(1\right)-u\left(1\right)v\left(3\right),u\left(1\right)v\left(2\right)-u\left(2\right)v\left(1\right)\right)$$
35	12 24 34	cif	$$classif\left(k=1,u\left(2\right)v\left(3\right)-u\left(3\right)v\left(2\right),if\left(k=2,u\left(3\right)v\left(1\right)-u\left(1\right)v\left(3\right),u\left(1\right)v\left(2\right)-u\left(2\right)v\left(1\right)\right)\right)$$
36	10 7 35	cmpt	$$class\left(k\in \left(1\dots 3\right)⟼if\left(k=1,u\left(2\right)v\left(3\right)-u\left(3\right)v\left(2\right),if\left(k=2,u\left(3\right)v\left(1\right)-u\left(1\right)v\left(3\right),u\left(1\right)v\left(2\right)-u\left(2\right)v\left(1\right)\right)\right)\right)$$
37	1 9 8 8 36	cmpo	$$class\left(u\in \left({ℝ}^{\left(1\dots 3\right)}\right),v\in \left({ℝ}^{\left(1\dots 3\right)}\right)⟼\left(k\in \left(1\dots 3\right)⟼if\left(k=1,u\left(2\right)v\left(3\right)-u\left(3\right)v\left(2\right),if\left(k=2,u\left(3\right)v\left(1\right)-u\left(1\right)v\left(3\right),u\left(1\right)v\left(2\right)-u\left(2\right)v\left(1\right)\right)\right)\right)\right)$$
38	0 37	wceq	Could not format crossp = ( u e. ( RR ^m ( 1 ... 3 ) ) , v e. ( RR ^m ( 1 ... 3 ) ) |-> ( k e. ( 1 ... 3 ) |-> if ( k = 1 , ( ( ( u ` 2 ) x. ( v ` 3 ) ) - ( ( u ` 3 ) x. ( v ` 2 ) ) ) , if ( k = 2 , ( ( ( u ` 3 ) x. ( v ` 1 ) ) - ( ( u ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( u ` 1 ) x. ( v ` 2 ) ) - ( ( u ` 2 ) x. ( v ` 1 ) ) ) ) ) ) ) : No typesetting found for wff crossp = ( u e. ( RR ^m ( 1 ... 3 ) ) , v e. ( RR ^m ( 1 ... 3 ) ) |-> ( k e. ( 1 ... 3 ) |-> if ( k = 1 , ( ( ( u ` 2 ) x. ( v ` 3 ) ) - ( ( u ` 3 ) x. ( v ` 2 ) ) ) , if ( k = 2 , ( ( ( u ` 3 ) x. ( v ` 1 ) ) - ( ( u ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( u ` 1 ) x. ( v ` 2 ) ) - ( ( u ` 2 ) x. ( v ` 1 ) ) ) ) ) ) ) with typecode wff