Metamath Proof Explorer

Definition df-tripp

Description: Define the scalar triple product of three 3-dimensional real coordinate vectors as the dot product of the first vector with the cross product of the other two. Vectors are represented as functions on ( 1 ... 3 ) . Apply as ( y ( trippx ) z ) . (Contributed by Jiamin Zhao, 31-Jul-2026)

Ref Expression
Assertion df-tripp 
|- tripp = ( x e. ( RR ^m ( 1 ... 3 ) ) |-> ( y e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctripp 
 |-  tripp
1 vx 
 |-  x
2 cr 
 |-  RR
3 cmap 
 |-  ^m
4 c1 
 |-  1
5 cfz 
 |-  ...
6 c3 
 |-  3
7 4 6 5 co 
 |-  ( 1 ... 3 )
8 2 7 3 co 
 |-  ( RR ^m ( 1 ... 3 ) )
9 vy 
 |-  y
10 vz 
 |-  z
11 crefld 
 |-  RRfld
12 cgsu 
 |-  gsum
13 vk 
 |-  k
14 1 cv 
 |-  x
15 13 cv 
 |-  k
16 15 14 cfv 
 |-  ( x ` k )
17 cmul 
 |-  x.
18 9 cv 
 |-  y
19 ccrossp 
 |-  crossp
20 10 cv 
 |-  z
21 18 20 19 co 
 |-  ( y crossp z )
22 15 21 cfv 
 |-  ( ( y crossp z ) ` k )
23 16 22 17 co 
 |-  ( ( x ` k ) x. ( ( y crossp z ) ` k ) )
24 13 7 23 cmpt 
 |-  ( k e. ( 1 ... 3 ) |-> ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) )
25 11 24 12 co 
 |-  ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) ) )
26 9 10 8 8 25 cmpo 
 |-  ( y e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) ) ) )
27 1 8 26 cmpt 
 |-  ( x e. ( RR ^m ( 1 ... 3 ) ) |-> ( y e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) ) ) ) )
28 0 27 wceq 
 |-  tripp = ( x e. ( RR ^m ( 1 ... 3 ) ) |-> ( y e. ( RR ^m ( 1 ... 3 ) ) , z e. ( RR ^m ( 1 ... 3 ) ) |-> ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) ) ) ) )