Metamath Proof Explorer

Theorem crosspval

Description: Value of the cross product of two 3-dimensional real coordinate vectors as a function on ( 1 ... 3 ) . (Contributed by Jiamin Zhao, 31-Jul-2026)

Ref Expression
Assertion crosspval 
|- ( ( 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 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( u = A -> ( u ` 2 ) = ( A ` 2 ) )
2 1 oveq1d 
 |-  ( u = A -> ( ( u ` 2 ) x. ( v ` 3 ) ) = ( ( A ` 2 ) x. ( v ` 3 ) ) )
3 fveq1 
 |-  ( u = A -> ( u ` 3 ) = ( A ` 3 ) )
4 3 oveq1d 
 |-  ( u = A -> ( ( u ` 3 ) x. ( v ` 2 ) ) = ( ( A ` 3 ) x. ( v ` 2 ) ) )
5 2 4 oveq12d 
 |-  ( u = A -> ( ( ( u ` 2 ) x. ( v ` 3 ) ) - ( ( u ` 3 ) x. ( v ` 2 ) ) ) = ( ( ( A ` 2 ) x. ( v ` 3 ) ) - ( ( A ` 3 ) x. ( v ` 2 ) ) ) )
6 3 oveq1d 
 |-  ( u = A -> ( ( u ` 3 ) x. ( v ` 1 ) ) = ( ( A ` 3 ) x. ( v ` 1 ) ) )
7 fveq1 
 |-  ( u = A -> ( u ` 1 ) = ( A ` 1 ) )
8 7 oveq1d 
 |-  ( u = A -> ( ( u ` 1 ) x. ( v ` 3 ) ) = ( ( A ` 1 ) x. ( v ` 3 ) ) )
9 6 8 oveq12d 
 |-  ( u = A -> ( ( ( u ` 3 ) x. ( v ` 1 ) ) - ( ( u ` 1 ) x. ( v ` 3 ) ) ) = ( ( ( A ` 3 ) x. ( v ` 1 ) ) - ( ( A ` 1 ) x. ( v ` 3 ) ) ) )
10 7 oveq1d 
 |-  ( u = A -> ( ( u ` 1 ) x. ( v ` 2 ) ) = ( ( A ` 1 ) x. ( v ` 2 ) ) )
11 1 oveq1d 
 |-  ( u = A -> ( ( u ` 2 ) x. ( v ` 1 ) ) = ( ( A ` 2 ) x. ( v ` 1 ) ) )
12 10 11 oveq12d 
 |-  ( u = A -> ( ( ( u ` 1 ) x. ( v ` 2 ) ) - ( ( u ` 2 ) x. ( v ` 1 ) ) ) = ( ( ( A ` 1 ) x. ( v ` 2 ) ) - ( ( A ` 2 ) x. ( v ` 1 ) ) ) )
13 9 12 ifeq12d 
 |-  ( u = A -> if ( k = 2 , ( ( ( u ` 3 ) x. ( v ` 1 ) ) - ( ( u ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( u ` 1 ) x. ( v ` 2 ) ) - ( ( u ` 2 ) x. ( v ` 1 ) ) ) ) = if ( k = 2 , ( ( ( A ` 3 ) x. ( v ` 1 ) ) - ( ( A ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( v ` 2 ) ) - ( ( A ` 2 ) x. ( v ` 1 ) ) ) ) )
14 5 13 ifeq12d 
 |-  ( u = A -> 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 ) ) ) ) ) = if ( k = 1 , ( ( ( A ` 2 ) x. ( v ` 3 ) ) - ( ( A ` 3 ) x. ( v ` 2 ) ) ) , if ( k = 2 , ( ( ( A ` 3 ) x. ( v ` 1 ) ) - ( ( A ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( v ` 2 ) ) - ( ( A ` 2 ) x. ( v ` 1 ) ) ) ) ) )
15 14 mpteq2dv 
 |-  ( u = A -> ( 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 ) ) ) ) ) ) = ( k e. ( 1 ... 3 ) |-> if ( k = 1 , ( ( ( A ` 2 ) x. ( v ` 3 ) ) - ( ( A ` 3 ) x. ( v ` 2 ) ) ) , if ( k = 2 , ( ( ( A ` 3 ) x. ( v ` 1 ) ) - ( ( A ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( v ` 2 ) ) - ( ( A ` 2 ) x. ( v ` 1 ) ) ) ) ) ) )
16 fveq1 
 |-  ( v = B -> ( v ` 3 ) = ( B ` 3 ) )
17 16 oveq2d 
 |-  ( v = B -> ( ( A ` 2 ) x. ( v ` 3 ) ) = ( ( A ` 2 ) x. ( B ` 3 ) ) )
18 fveq1 
 |-  ( v = B -> ( v ` 2 ) = ( B ` 2 ) )
19 18 oveq2d 
 |-  ( v = B -> ( ( A ` 3 ) x. ( v ` 2 ) ) = ( ( A ` 3 ) x. ( B ` 2 ) ) )
20 17 19 oveq12d 
 |-  ( v = B -> ( ( ( A ` 2 ) x. ( v ` 3 ) ) - ( ( A ` 3 ) x. ( v ` 2 ) ) ) = ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) )
21 fveq1 
 |-  ( v = B -> ( v ` 1 ) = ( B ` 1 ) )
22 21 oveq2d 
 |-  ( v = B -> ( ( A ` 3 ) x. ( v ` 1 ) ) = ( ( A ` 3 ) x. ( B ` 1 ) ) )
23 16 oveq2d 
 |-  ( v = B -> ( ( A ` 1 ) x. ( v ` 3 ) ) = ( ( A ` 1 ) x. ( B ` 3 ) ) )
24 22 23 oveq12d 
 |-  ( v = B -> ( ( ( A ` 3 ) x. ( v ` 1 ) ) - ( ( A ` 1 ) x. ( v ` 3 ) ) ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) )
25 18 oveq2d 
 |-  ( v = B -> ( ( A ` 1 ) x. ( v ` 2 ) ) = ( ( A ` 1 ) x. ( B ` 2 ) ) )
26 21 oveq2d 
 |-  ( v = B -> ( ( A ` 2 ) x. ( v ` 1 ) ) = ( ( A ` 2 ) x. ( B ` 1 ) ) )
27 25 26 oveq12d 
 |-  ( v = B -> ( ( ( A ` 1 ) x. ( v ` 2 ) ) - ( ( A ` 2 ) x. ( v ` 1 ) ) ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) )
28 24 27 ifeq12d 
 |-  ( v = B -> if ( k = 2 , ( ( ( A ` 3 ) x. ( v ` 1 ) ) - ( ( A ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( v ` 2 ) ) - ( ( A ` 2 ) x. ( v ` 1 ) ) ) ) = if ( k = 2 , ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) )
29 20 28 ifeq12d 
 |-  ( v = B -> if ( k = 1 , ( ( ( A ` 2 ) x. ( v ` 3 ) ) - ( ( A ` 3 ) x. ( v ` 2 ) ) ) , if ( k = 2 , ( ( ( A ` 3 ) x. ( v ` 1 ) ) - ( ( A ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( v ` 2 ) ) - ( ( A ` 2 ) x. ( v ` 1 ) ) ) ) ) = 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 ) ) ) ) ) )
30 29 mpteq2dv 
 |-  ( v = B -> ( k e. ( 1 ... 3 ) |-> if ( k = 1 , ( ( ( A ` 2 ) x. ( v ` 3 ) ) - ( ( A ` 3 ) x. ( v ` 2 ) ) ) , if ( k = 2 , ( ( ( A ` 3 ) x. ( v ` 1 ) ) - ( ( A ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( v ` 2 ) ) - ( ( A ` 2 ) x. ( v ` 1 ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) )
31 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 ) ) ) ) ) ) )
32 ovex 
 |-  ( 1 ... 3 ) e. _V
33 32 mptex 
 |-  ( 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 ) ) ) ) ) ) e. _V
34 15 30 31 33 ovmpo 
 |-  ( ( 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 ) ) ) ) ) ) )