Metamath Proof Explorer

Theorem crosspclem

Description: Lemma for crosspcld . Closure of the three-way coordinate case split used in the cross product's mapping rule. (Contributed by Jiamin Zhao, 11-Aug-2026)

Ref Expression
Hypotheses crosspd.1 
|- ( ph -> A e. ( RR ^m ( 1 ... 3 ) ) )
crosspd.2 
|- ( ph -> B e. ( RR ^m ( 1 ... 3 ) ) )
Assertion crosspclem 
|- ( ph -> 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. RR )

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 1 2 crosspcle1d 
 |-  ( ph -> ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) e. RR )
4 1 2 crosspcle2d 
 |-  ( ph -> ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) e. RR )
5 1 2 crosspcle3d 
 |-  ( ph -> ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) e. RR )
6 4 5 ifcld 
 |-  ( ph -> if ( k = 2 , ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) e. RR )
7 3 6 ifcld 
 |-  ( ph -> 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. RR )