Metamath Proof Explorer

Theorem crosspv3i

Description: Value of the third component of the cross product. (Contributed by Jiamin Zhao, 31-Jul-2026)

Ref Expression
Hypotheses crossp.1 
|- A e. ( RR ^m ( 1 ... 3 ) )
crossp.2 
|- B e. ( RR ^m ( 1 ... 3 ) )
Assertion crosspv3i 
|- ( ( A crossp B ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) )

Proof

Step Hyp Ref Expression
1 crossp.1 
 |-  A e. ( RR ^m ( 1 ... 3 ) )
2 crossp.2 
 |-  B e. ( RR ^m ( 1 ... 3 ) )
3 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 ) ) ) ) ) ) )
4 1 2 3 mp2an 
 |-  ( 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 ) ) ) ) ) )
5 4 fveq1i 
 |-  ( ( A crossp B ) ` 3 ) = ( ( 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 ) ) ) ) ) ) ` 3 )
6 3elfz13 
 |-  3 e. ( 1 ... 3 )
7 1 2 crosspcle3i 
 |-  ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) e. RR
8 id 
 |-  ( k = 1 -> k = 1 )
9 1ne3 
 |-  1 =/= 3
10 9 a1i 
 |-  ( k = 1 -> 1 =/= 3 )
11 8 10 eqnetrd 
 |-  ( k = 1 -> k =/= 3 )
12 11 necon2bi 
 |-  ( k = 3 -> -. k = 1 )
13 12 iffalsed 
 |-  ( k = 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 ) ) ) ) ) = if ( k = 2 , ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) )
14 id 
 |-  ( k = 2 -> k = 2 )
15 2ne3 
 |-  2 =/= 3
16 15 a1i 
 |-  ( k = 2 -> 2 =/= 3 )
17 14 16 eqnetrd 
 |-  ( k = 2 -> k =/= 3 )
18 17 necon2bi 
 |-  ( k = 3 -> -. k = 2 )
19 18 iffalsed 
 |-  ( k = 3 -> if ( k = 2 , ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) )
20 13 19 eqtrd 
 |-  ( k = 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 ) ) ) ) ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) )
21 eqid 
 |-  ( 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 ) ) ) ) ) ) = ( 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 ) ) ) ) ) )
22 20 21 fvmptg 
 |-  ( ( 3 e. ( 1 ... 3 ) /\ ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) e. RR ) -> ( ( 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 ) ) ) ) ) ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) )
23 6 7 22 mp2an 
 |-  ( ( 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 ) ) ) ) ) ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) )
24 5 23 eqtri 
 |-  ( ( A crossp B ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) )