Metamath Proof Explorer

Theorem crosspdotd

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

Ref Expression
Hypotheses crosspdotd.1 
|- ( ph -> A e. ( RR ^m ( 1 ... 3 ) ) )
crosspdotd.2 
|- ( ph -> B e. ( RR ^m ( 1 ... 3 ) ) )
crosspdotd.3 
|- ( ph -> C e. ( RR ^m ( 1 ... 3 ) ) )
Assertion crosspdotd 
|- ( ph -> ( 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 crosspdotd.1 
 |-  ( ph -> A e. ( RR ^m ( 1 ... 3 ) ) )
2 crosspdotd.2 
 |-  ( ph -> B e. ( RR ^m ( 1 ... 3 ) ) )
3 crosspdotd.3 
 |-  ( ph -> C e. ( RR ^m ( 1 ... 3 ) ) )
4 1 2 3 crosspdot0lem 
 |-  ( ph -> ( B ( tripp ` A ) C ) = ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( A ` k ) x. ( ( B crossp C ) ` k ) ) ) ) )
5 1 2 3 crosspdotsumlem 
 |-  ( ph -> ( 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 crosspv1d 
 |-  ( ph -> ( ( B crossp C ) ` 1 ) = ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) )
7 6 oveq2d 
 |-  ( ph -> ( ( A ` 1 ) x. ( ( B crossp C ) ` 1 ) ) = ( ( A ` 1 ) x. ( ( ( B ` 2 ) x. ( C ` 3 ) ) - ( ( B ` 3 ) x. ( C ` 2 ) ) ) ) )
8 2 3 crosspv2d 
 |-  ( ph -> ( ( B crossp C ) ` 2 ) = ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) )
9 8 oveq2d 
 |-  ( ph -> ( ( A ` 2 ) x. ( ( B crossp C ) ` 2 ) ) = ( ( A ` 2 ) x. ( ( ( B ` 3 ) x. ( C ` 1 ) ) - ( ( B ` 1 ) x. ( C ` 3 ) ) ) ) )
10 2 3 crosspv3d 
 |-  ( ph -> ( ( B crossp C ) ` 3 ) = ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) )
11 10 oveq2d 
 |-  ( ph -> ( ( A ` 3 ) x. ( ( B crossp C ) ` 3 ) ) = ( ( A ` 3 ) x. ( ( ( B ` 1 ) x. ( C ` 2 ) ) - ( ( B ` 2 ) x. ( C ` 1 ) ) ) ) )
12 9 11 oveq12d 
 |-  ( ph -> ( ( ( 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 oveq12d 
 |-  ( ph -> ( ( ( 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 rr3fv1cld 
 |-  ( ph -> ( A ` 1 ) e. RR )
15 14 recnd 
 |-  ( ph -> ( A ` 1 ) e. CC )
16 2 rr3fv2cld 
 |-  ( ph -> ( B ` 2 ) e. RR )
17 3 rr3fv3cld 
 |-  ( ph -> ( C ` 3 ) e. RR )
18 16 17 remulcld 
 |-  ( ph -> ( ( B ` 2 ) x. ( C ` 3 ) ) e. RR )
19 18 recnd 
 |-  ( ph -> ( ( B ` 2 ) x. ( C ` 3 ) ) e. CC )
20 2 rr3fv3cld 
 |-  ( ph -> ( B ` 3 ) e. RR )
21 3 rr3fv2cld 
 |-  ( ph -> ( C ` 2 ) e. RR )
22 20 21 remulcld 
 |-  ( ph -> ( ( B ` 3 ) x. ( C ` 2 ) ) e. RR )
23 22 recnd 
 |-  ( ph -> ( ( B ` 3 ) x. ( C ` 2 ) ) e. CC )
24 15 19 23 subdid 
 |-  ( ph -> ( ( 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 recnd 
 |-  ( ph -> ( B ` 2 ) e. CC )
26 17 recnd 
 |-  ( ph -> ( C ` 3 ) e. CC )
27 15 25 26 mulassd 
 |-  ( ph -> ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) = ( ( A ` 1 ) x. ( ( B ` 2 ) x. ( C ` 3 ) ) ) )
28 27 eqcomd 
 |-  ( ph -> ( ( A ` 1 ) x. ( ( B ` 2 ) x. ( C ` 3 ) ) ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) x. ( C ` 3 ) ) )
29 20 recnd 
 |-  ( ph -> ( B ` 3 ) e. CC )
30 21 recnd 
 |-  ( ph -> ( C ` 2 ) e. CC )
31 15 29 30 mulassd 
 |-  ( ph -> ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) = ( ( A ` 1 ) x. ( ( B ` 3 ) x. ( C ` 2 ) ) ) )
32 31 eqcomd 
 |-  ( ph -> ( ( A ` 1 ) x. ( ( B ` 3 ) x. ( C ` 2 ) ) ) = ( ( ( A ` 1 ) x. ( B ` 3 ) ) x. ( C ` 2 ) ) )
33 28 32 oveq12d 
 |-  ( ph -> ( ( ( 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 eqtrd 
 |-  ( ph -> ( ( 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 rr3fv2cld 
 |-  ( ph -> ( A ` 2 ) e. RR )
36 35 recnd 
 |-  ( ph -> ( A ` 2 ) e. CC )
37 3 rr3fv1cld 
 |-  ( ph -> ( C ` 1 ) e. RR )
38 20 37 remulcld 
 |-  ( ph -> ( ( B ` 3 ) x. ( C ` 1 ) ) e. RR )
39 38 recnd 
 |-  ( ph -> ( ( B ` 3 ) x. ( C ` 1 ) ) e. CC )
40 2 rr3fv1cld 
 |-  ( ph -> ( B ` 1 ) e. RR )
41 40 17 remulcld 
 |-  ( ph -> ( ( B ` 1 ) x. ( C ` 3 ) ) e. RR )
42 41 recnd 
 |-  ( ph -> ( ( B ` 1 ) x. ( C ` 3 ) ) e. CC )
43 36 39 42 subdid 
 |-  ( ph -> ( ( 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 recnd 
 |-  ( ph -> ( C ` 1 ) e. CC )
45 36 29 44 mulassd 
 |-  ( ph -> ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) = ( ( A ` 2 ) x. ( ( B ` 3 ) x. ( C ` 1 ) ) ) )
46 45 eqcomd 
 |-  ( ph -> ( ( A ` 2 ) x. ( ( B ` 3 ) x. ( C ` 1 ) ) ) = ( ( ( A ` 2 ) x. ( B ` 3 ) ) x. ( C ` 1 ) ) )
47 40 recnd 
 |-  ( ph -> ( B ` 1 ) e. CC )
48 36 47 26 mulassd 
 |-  ( ph -> ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) = ( ( A ` 2 ) x. ( ( B ` 1 ) x. ( C ` 3 ) ) ) )
49 48 eqcomd 
 |-  ( ph -> ( ( A ` 2 ) x. ( ( B ` 1 ) x. ( C ` 3 ) ) ) = ( ( ( A ` 2 ) x. ( B ` 1 ) ) x. ( C ` 3 ) ) )
50 46 49 oveq12d 
 |-  ( ph -> ( ( ( 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 eqtrd 
 |-  ( ph -> ( ( 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 rr3fv3cld 
 |-  ( ph -> ( A ` 3 ) e. RR )
53 52 recnd 
 |-  ( ph -> ( A ` 3 ) e. CC )
54 40 21 remulcld 
 |-  ( ph -> ( ( B ` 1 ) x. ( C ` 2 ) ) e. RR )
55 54 recnd 
 |-  ( ph -> ( ( B ` 1 ) x. ( C ` 2 ) ) e. CC )
56 16 37 remulcld 
 |-  ( ph -> ( ( B ` 2 ) x. ( C ` 1 ) ) e. RR )
57 56 recnd 
 |-  ( ph -> ( ( B ` 2 ) x. ( C ` 1 ) ) e. CC )
58 53 55 57 subdid 
 |-  ( ph -> ( ( 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 mulassd 
 |-  ( ph -> ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) = ( ( A ` 3 ) x. ( ( B ` 1 ) x. ( C ` 2 ) ) ) )
60 59 eqcomd 
 |-  ( ph -> ( ( A ` 3 ) x. ( ( B ` 1 ) x. ( C ` 2 ) ) ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) x. ( C ` 2 ) ) )
61 53 25 44 mulassd 
 |-  ( ph -> ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) = ( ( A ` 3 ) x. ( ( B ` 2 ) x. ( C ` 1 ) ) ) )
62 61 eqcomd 
 |-  ( ph -> ( ( A ` 3 ) x. ( ( B ` 2 ) x. ( C ` 1 ) ) ) = ( ( ( A ` 3 ) x. ( B ` 2 ) ) x. ( C ` 1 ) ) )
63 60 62 oveq12d 
 |-  ( ph -> ( ( ( 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 eqtrd 
 |-  ( ph -> ( ( 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 oveq12d 
 |-  ( ph -> ( ( ( 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 oveq12d 
 |-  ( ph -> ( ( ( 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 eqtrd 
 |-  ( ph -> ( ( ( 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 eqtrd 
 |-  ( ph -> ( 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 eqtrd 
 |-  ( ph -> ( 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 ) ) ) ) ) )