Metamath Proof Explorer

Theorem crosspdoti

Description: Value of the scalar triple product, expanded into the standard six-term Sarrus polynomial. (Contributed by Jiamin Zhao, 1-Aug-2026)

Ref Expression
Hypotheses crosspdoti.1 
|- A e. ( RR ^m ( 1 ... 3 ) )
crosspdoti.2 
|- B e. ( RR ^m ( 1 ... 3 ) )
crosspdoti.3 
|- C e. ( RR ^m ( 1 ... 3 ) )
Assertion crosspdoti 
|- ( B ( tripp ` A ) C ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 crosspdoti.1 
 |-  A e. ( RR ^m ( 1 ... 3 ) )
2 crosspdoti.2 
 |-  B e. ( RR ^m ( 1 ... 3 ) )
3 crosspdoti.3 
 |-  C e. ( RR ^m ( 1 ... 3 ) )
4 1 2 3 crosspdot0i 
 |-  ( B ( tripp ` A ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) )
5 1 2 3 crosspdotsumi 
 |-  ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) = ( ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) + ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) )
6 2 3 crosspv1i 
 |-  ( ( B crossp C ) ` 1 ) = ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) )
7 6 oveq2i 
 |-  ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) = ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) )
8 2 3 crosspv2i 
 |-  ( ( B crossp C ) ` 2 ) = ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) )
9 8 oveq2i 
 |-  ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) = ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) )
10 2 3 crosspv3i 
 |-  ( ( B crossp C ) ` 3 ) = ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) )
11 10 oveq2i 
 |-  ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) = ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) )
12 9 11 oveq12i 
 |-  ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) = ( ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) + ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) )
13 7 12 oveq12i 
 |-  ( ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) + ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) ) = ( ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) + ( ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) + ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) ) )
14 1 rr3fv1cli 
 |-  ( A ` 1 ) e. RR
15 14 recni 
 |-  ( A ` 1 ) e. CC
16 2 rr3fv2cli 
 |-  ( B ` 2 ) e. RR
17 3 rr3fv3cli 
 |-  ( C ` 3 ) e. RR
18 16 17 remulcli 
 |-  ( ( B ` 2 ) x. ( C ` 3 ) ) e. RR
19 18 recni 
 |-  ( ( B ` 2 ) x. ( C ` 3 ) ) e. CC
20 2 rr3fv3cli 
 |-  ( B ` 3 ) e. RR
21 3 rr3fv2cli 
 |-  ( C ` 2 ) e. RR
22 20 21 remulcli 
 |-  ( ( B ` 3 ) x. ( C ` 2 ) ) e. RR
23 22 recni 
 |-  ( ( B ` 3 ) x. ( C ` 2 ) ) e. CC
24 15 19 23 subdii 
 |-  ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) = ( ( ( A ` 1 ) x. ( ( B ` 2 ) x. ( C ` 3 ) ) ) - ( ( A ` 1 ) x. ( ( B ` 3 ) x. ( C ` 2 ) ) ) )
25 16 recni 
 |-  ( B ` 2 ) e. CC
26 17 recni 
 |-  ( C ` 3 ) e. CC
27 15 25 26 mulassi 
 |-  ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) = ( ( A ` 1 ) x. ( ( B ` 2 ) x. ( C ` 3 ) ) )
28 27 eqcomi 
 |-  ( ( A ` 1 ) x. ( ( B ` 2 ) x. ( C ` 3 ) ) ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) )
29 20 recni 
 |-  ( B ` 3 ) e. CC
30 21 recni 
 |-  ( C ` 2 ) e. CC
31 15 29 30 mulassi 
 |-  ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) = ( ( A ` 1 ) x. ( ( B ` 3 ) x. ( C ` 2 ) ) )
32 31 eqcomi 
 |-  ( ( A ` 1 ) x. ( ( B ` 3 ) x. ( C ` 2 ) ) ) = ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) )
33 28 32 oveq12i 
 |-  ( ( ( A ` 1 ) x. ( ( B ` 2 ) x. ( C ` 3 ) ) ) - ( ( A ` 1 ) x. ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) = ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) )
34 24 33 eqtri 
 |-  ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) = ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) )
35 1 rr3fv2cli 
 |-  ( A ` 2 ) e. RR
36 35 recni 
 |-  ( A ` 2 ) e. CC
37 3 rr3fv1cli 
 |-  ( C ` 1 ) e. RR
38 20 37 remulcli 
 |-  ( ( B ` 3 ) x. ( C ` 1 ) ) e. RR
39 38 recni 
 |-  ( ( B ` 3 ) x. ( C ` 1 ) ) e. CC
40 2 rr3fv1cli 
 |-  ( B ` 1 ) e. RR
41 40 17 remulcli 
 |-  ( ( B ` 1 ) x. ( C ` 3 ) ) e. RR
42 41 recni 
 |-  ( ( B ` 1 ) x. ( C ` 3 ) ) e. CC
43 36 39 42 subdii 
 |-  ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) = ( ( ( A ` 2 ) x. ( ( B ` 3 ) x. ( C ` 1 ) ) ) - ( ( A ` 2 ) x. ( ( B ` 1 ) x. ( C ` 3 ) ) ) )
44 37 recni 
 |-  ( C ` 1 ) e. CC
45 36 29 44 mulassi 
 |-  ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) = ( ( A ` 2 ) x. ( ( B ` 3 ) x. ( C ` 1 ) ) )
46 45 eqcomi 
 |-  ( ( A ` 2 ) x. ( ( B ` 3 ) x. ( C ` 1 ) ) ) = ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) )
47 40 recni 
 |-  ( B ` 1 ) e. CC
48 36 47 26 mulassi 
 |-  ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) = ( ( A ` 2 ) x. ( ( B ` 1 ) x. ( C ` 3 ) ) )
49 48 eqcomi 
 |-  ( ( A ` 2 ) x. ( ( B ` 1 ) x. ( C ` 3 ) ) ) = ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) )
50 46 49 oveq12i 
 |-  ( ( ( A ` 2 ) x. ( ( B ` 3 ) x. ( C ` 1 ) ) ) - ( ( A ` 2 ) x. ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) = ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) )
51 43 50 eqtri 
 |-  ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) = ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) )
52 1 rr3fv3cli 
 |-  ( A ` 3 ) e. RR
53 52 recni 
 |-  ( A ` 3 ) e. CC
54 40 21 remulcli 
 |-  ( ( B ` 1 ) x. ( C ` 2 ) ) e. RR
55 54 recni 
 |-  ( ( B ` 1 ) x. ( C ` 2 ) ) e. CC
56 16 37 remulcli 
 |-  ( ( B ` 2 ) x. ( C ` 1 ) ) e. RR
57 56 recni 
 |-  ( ( B ` 2 ) x. ( C ` 1 ) ) e. CC
58 53 55 57 subdii 
 |-  ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) = ( ( ( A ` 3 ) x. ( ( B ` 1 ) x. ( C ` 2 ) ) ) - ( ( A ` 3 ) x. ( ( B ` 2 ) x. ( C ` 1 ) ) ) )
59 53 47 30 mulassi 
 |-  ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) = ( ( A ` 3 ) x. ( ( B ` 1 ) x. ( C ` 2 ) ) )
60 59 eqcomi 
 |-  ( ( A ` 3 ) x. ( ( B ` 1 ) x. ( C ` 2 ) ) ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) )
61 53 25 44 mulassi 
 |-  ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) = ( ( A ` 3 ) x. ( ( B ` 2 ) x. ( C ` 1 ) ) )
62 61 eqcomi 
 |-  ( ( A ` 3 ) x. ( ( B ` 2 ) x. ( C ` 1 ) ) ) = ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) )
63 60 62 oveq12i 
 |-  ( ( ( A ` 3 ) x. ( ( B ` 1 ) x. ( C ` 2 ) ) ) - ( ( A ` 3 ) x. ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) = ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) )
64 58 63 eqtri 
 |-  ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) = ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) )
65 51 64 oveq12i 
 |-  ( ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) + ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) ) = ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) )
66 34 65 oveq12i 
 |-  ( ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) + ( ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) + ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) ) ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) )
67 13 66 eqtri 
 |-  ( ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) + ( ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) + ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) ) ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) )
68 5 67 eqtri 
 |-  ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) )
69 4 68 eqtri 
 |-  ( B ( tripp ` A ) C ) = ( ( ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) - ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) ) + ( ( ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) - ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) ) + ( ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) - ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) ) ) )