Definition df-crossp 50652

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.)

Assertion

Ref	Expression
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)))))))

Distinct variable group:   𝑢,𝑘,𝑣

Detailed syntax breakdown of Definition df-crossp

Step	Hyp	Ref	Expression
1		ccrossp 50651	. 2 class ⊠
2		vu	. . 3 setvar 𝑢
3		vv	. . 3 setvar 𝑣
4		cr 11094	. . . 4 class ℝ
5		c1 11096	. . . . 5 class 1
6		c3 12291	. . . . 5 class 3
7		cfz 13530	. . . . 5 class ...
8	5, 6, 7	co 7410	. . . 4 class (1...3)
9		cmap 8820	. . . 4 class ↑m
10	4, 8, 9	co 7410	. . 3 class (ℝ ↑m (1...3))
11		vk	. . . 4 setvar 𝑘
12	11	cv 1569	. . . . . 6 class 𝑘
13	12, 5	wceq 1570	. . . . 5 wff 𝑘 = 1
14		c2 12290	. . . . . . . 8 class 2
15	2	cv 1569	. . . . . . . 8 class 𝑢
16	14, 15	cfv 6536	. . . . . . 7 class (𝑢‘2)
17	3	cv 1569	. . . . . . . 8 class 𝑣
18	6, 17	cfv 6536	. . . . . . 7 class (𝑣‘3)
19		cmul 11100	. . . . . . 7 class ·
20	16, 18, 19	co 7410	. . . . . 6 class ((𝑢‘2) · (𝑣‘3))
21	6, 15	cfv 6536	. . . . . . 7 class (𝑢‘3)
22	14, 17	cfv 6536	. . . . . . 7 class (𝑣‘2)
23	21, 22, 19	co 7410	. . . . . 6 class ((𝑢‘3) · (𝑣‘2))
24		cmin 11436	. . . . . 6 class −
25	20, 23, 24	co 7410	. . . . 5 class (((𝑢‘2) · (𝑣‘3)) − ((𝑢‘3) · (𝑣‘2)))
26	12, 14	wceq 1570	. . . . . 6 wff 𝑘 = 2
27	5, 17	cfv 6536	. . . . . . . 8 class (𝑣‘1)
28	21, 27, 19	co 7410	. . . . . . 7 class ((𝑢‘3) · (𝑣‘1))
29	5, 15	cfv 6536	. . . . . . . 8 class (𝑢‘1)
30	29, 18, 19	co 7410	. . . . . . 7 class ((𝑢‘1) · (𝑣‘3))
31	28, 30, 24	co 7410	. . . . . 6 class (((𝑢‘3) · (𝑣‘1)) − ((𝑢‘1) · (𝑣‘3)))
32	29, 22, 19	co 7410	. . . . . . 7 class ((𝑢‘1) · (𝑣‘2))
33	16, 27, 19	co 7410	. . . . . . 7 class ((𝑢‘2) · (𝑣‘1))
34	32, 33, 24	co 7410	. . . . . 6 class (((𝑢‘1) · (𝑣‘2)) − ((𝑢‘2) · (𝑣‘1)))
35	26, 31, 34	cif 4487	. . . . 5 class if(𝑘 = 2, (((𝑢‘3) · (𝑣‘1)) − ((𝑢‘1) · (𝑣‘3))), (((𝑢‘1) · (𝑣‘2)) − ((𝑢‘2) · (𝑣‘1))))
36	13, 25, 35	cif 4487	. . . 4 class if(𝑘 = 1, (((𝑢‘2) · (𝑣‘3)) − ((𝑢‘3) · (𝑣‘2))), if(𝑘 = 2, (((𝑢‘3) · (𝑣‘1)) − ((𝑢‘1) · (𝑣‘3))), (((𝑢‘1) · (𝑣‘2)) − ((𝑢‘2) · (𝑣‘1)))))
37	11, 8, 36	cmpt 5192	. . 3 class (𝑘 ∈ (1...3) ↦ if(𝑘 = 1, (((𝑢‘2) · (𝑣‘3)) − ((𝑢‘3) · (𝑣‘2))), if(𝑘 = 2, (((𝑢‘3) · (𝑣‘1)) − ((𝑢‘1) · (𝑣‘3))), (((𝑢‘1) · (𝑣‘2)) − ((𝑢‘2) · (𝑣‘1))))))
38	2, 3, 10, 10, 37	cmpo 7412	. 2 class (𝑢 ∈ (ℝ ↑m (1...3)), 𝑣 ∈ (ℝ ↑m (1...3)) ↦ (𝑘 ∈ (1...3) ↦ if(𝑘 = 1, (((𝑢‘2) · (𝑣‘3)) − ((𝑢‘3) · (𝑣‘2))), if(𝑘 = 2, (((𝑢‘3) · (𝑣‘1)) − ((𝑢‘1) · (𝑣‘3))), (((𝑢‘1) · (𝑣‘2)) − ((𝑢‘2) · (𝑣‘1)))))))
39	1, 38	wceq 1570	1 wff ⊠ = (𝑢 ∈ (ℝ ↑m (1...3)), 𝑣 ∈ (ℝ ↑m (1...3)) ↦ (𝑘 ∈ (1...3) ↦ if(𝑘 = 1, (((𝑢‘2) · (𝑣‘3)) − ((𝑢‘3) · (𝑣‘2))), if(𝑘 = 2, (((𝑢‘3) · (𝑣‘1)) − ((𝑢‘1) · (𝑣‘3))), (((𝑢‘1) · (𝑣‘2)) − ((𝑢‘2) · (𝑣‘1)))))))

This definition is referenced by:  crosspval  50655