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	⊢ ⊠ = ( 𝑢 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑣 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccrossp	⊢ ⊠
1		vu	⊢ 𝑢
2		cr	⊢ ℝ
3		cmap	⊢ ↑m
4		c1	⊢ 1
5		cfz	⊢ ...
6		c3	⊢ 3
7	4 6 5	co	⊢ ( 1 ... 3 )
8	2 7 3	co	⊢ ( ℝ ↑m ( 1 ... 3 ) )
9		vv	⊢ 𝑣
10		vk	⊢ 𝑘
11	10	cv	⊢ 𝑘
12	11 4	wceq	⊢ 𝑘 = 1
13	1	cv	⊢ 𝑢
14		c2	⊢ 2
15	14 13	cfv	⊢ ( 𝑢 ‘ 2 )
16		cmul	⊢ ·
17	9	cv	⊢ 𝑣
18	6 17	cfv	⊢ ( 𝑣 ‘ 3 )
19	15 18 16	co	⊢ ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) )
20		cmin	⊢ −
21	6 13	cfv	⊢ ( 𝑢 ‘ 3 )
22	14 17	cfv	⊢ ( 𝑣 ‘ 2 )
23	21 22 16	co	⊢ ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) )
24	19 23 20	co	⊢ ( ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) )
25	11 14	wceq	⊢ 𝑘 = 2
26	4 17	cfv	⊢ ( 𝑣 ‘ 1 )
27	21 26 16	co	⊢ ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) )
28	4 13	cfv	⊢ ( 𝑢 ‘ 1 )
29	28 18 16	co	⊢ ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) )
30	27 29 20	co	⊢ ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) )
31	28 22 16	co	⊢ ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) )
32	15 26 16	co	⊢ ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) )
33	31 32 20	co	⊢ ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) )
34	25 30 33	cif	⊢ if ( 𝑘 = 2 , ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) )
35	12 24 34	cif	⊢ if ( 𝑘 = 1 , ( ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) )
36	10 7 35	cmpt	⊢ ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) ) )
37	1 9 8 8 36	cmpo	⊢ ( 𝑢 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑣 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) ) ) )
38	0 37	wceq	⊢ ⊠ = ( 𝑢 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑣 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) ) ) )