Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccrossp 
 |-  crossp
1 vu 
 |-  u
2 cr 
 |-  RR
3 cmap 
 |-  ^m
4 c1 
 |-  1
5 cfz 
 |-  ...
6 c3 
 |-  3
7 4 6 5 co 
 |-  ( 1 ... 3 )
8 2 7 3 co 
 |-  ( RR ^m ( 1 ... 3 ) )
9 vv 
 |-  v
10 vk 
 |-  k
11 10 cv 
 |-  k
12 11 4 wceq 
 |-  k = 1
13 1 cv 
 |-  u
14 c2 
 |-  2
15 14 13 cfv 
 |-  ( u ` 2 )
16 cmul 
 |-  x.
17 9 cv 
 |-  v
18 6 17 cfv 
 |-  ( v ` 3 )
19 15 18 16 co 
 |-  ( ( u ` 2 ) x. ( v ` 3 ) )
20 cmin 
 |-  -
21 6 13 cfv 
 |-  ( u ` 3 )
22 14 17 cfv 
 |-  ( v ` 2 )
23 21 22 16 co 
 |-  ( ( u ` 3 ) x. ( v ` 2 ) )
24 19 23 20 co 
 |-  ( ( ( u ` 2 ) x. ( v ` 3 ) ) - ( ( u ` 3 ) x. ( v ` 2 ) ) )
25 11 14 wceq 
 |-  k = 2
26 4 17 cfv 
 |-  ( v ` 1 )
27 21 26 16 co 
 |-  ( ( u ` 3 ) x. ( v ` 1 ) )
28 4 13 cfv 
 |-  ( u ` 1 )
29 28 18 16 co 
 |-  ( ( u ` 1 ) x. ( v ` 3 ) )
30 27 29 20 co 
 |-  ( ( ( u ` 3 ) x. ( v ` 1 ) ) - ( ( u ` 1 ) x. ( v ` 3 ) ) )
31 28 22 16 co 
 |-  ( ( u ` 1 ) x. ( v ` 2 ) )
32 15 26 16 co 
 |-  ( ( u ` 2 ) x. ( v ` 1 ) )
33 31 32 20 co 
 |-  ( ( ( u ` 1 ) x. ( v ` 2 ) ) - ( ( u ` 2 ) x. ( v ` 1 ) ) )
34 25 30 33 cif 
 |-  if ( k = 2 , ( ( ( u ` 3 ) x. ( v ` 1 ) ) - ( ( u ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( u ` 1 ) x. ( v ` 2 ) ) - ( ( u ` 2 ) x. ( v ` 1 ) ) ) )
35 12 24 34 cif 
 |-  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 ) ) ) ) )
36 10 7 35 cmpt 
 |-  ( 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 ) ) ) ) ) )
37 1 9 8 8 36 cmpo 
 |-  ( 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 ) ) ) ) ) ) )
38 0 37 wceq 
 |-  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 ) ) ) ) ) ) )