Metamath Proof Explorer

Theorem crosspv3d

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

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

Proof

Step Hyp Ref Expression
1 crosspd.1 
 |-  ( ph -> A e. ( RR ^m ( 1 ... 3 ) ) )
2 crosspd.2 
 |-  ( ph -> B e. ( RR ^m ( 1 ... 3 ) ) )
3 id 
 |-  ( k = 1 -> k = 1 )
4 1ne3 
 |-  1 =/= 3
5 4 a1i 
 |-  ( k = 1 -> 1 =/= 3 )
6 3 5 eqnetrd 
 |-  ( k = 1 -> k =/= 3 )
7 6 necon2bi 
 |-  ( k = 3 -> -. k = 1 )
8 7 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 ) ) ) ) )
9 id 
 |-  ( k = 2 -> k = 2 )
10 2ne3 
 |-  2 =/= 3
11 10 a1i 
 |-  ( k = 2 -> 2 =/= 3 )
12 9 11 eqnetrd 
 |-  ( k = 2 -> k =/= 3 )
13 12 necon2bi 
 |-  ( k = 3 -> -. k = 2 )
14 13 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 ) ) ) )
15 8 14 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 ) ) ) )
16 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 ) ) ) ) ) ) )
17 1 2 16 syl2anc 
 |-  ( ph -> ( 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 ) ) ) ) ) ) )
18 3elfz13 
 |-  3 e. ( 1 ... 3 )
19 18 a1i 
 |-  ( ph -> 3 e. ( 1 ... 3 ) )
20 1 2 crosspcle3d 
 |-  ( ph -> ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) e. RR )
21 15 17 19 20 fvmptd4 
 |-  ( ph -> ( ( A crossp B ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) )