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	Could not format assertion : No typesetting found for |- 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 ) ) ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctripp	Could not format tripp : No typesetting found for class tripp with typecode class
1		vx	$$setvarx$$
2		cr	$$classℝ$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4		c1	$$class1$$
5		cfz	$$class\dots$$
6		c3	$$class3$$
7	4 6 5	co	$$class\left(1\dots 3\right)$$
8	2 7 3	co	$$class\left({ℝ}^{\left(1\dots 3\right)}\right)$$
9		vy	$$setvary$$
10		vz	$$setvarz$$
11		crefld	$$class{ℝ}_{\mathrm{fld}}$$
12		cgsu	$$class{\Sigma }_{𝑔}$$
13		vk	$$setvark$$
14	1	cv	$$setvarx$$
15	13	cv	$$setvark$$
16	15 14	cfv	$$classx\left(k\right)$$
17		cmul	$$class\times$$
18	9	cv	$$setvary$$
19		ccrossp	Could not format crossp : No typesetting found for class crossp with typecode class
20	10	cv	$$setvarz$$
21	18 20 19	co	Could not format ( y crossp z ) : No typesetting found for class ( y crossp z ) with typecode class
22	15 21	cfv	Could not format ( ( y crossp z ) ` k ) : No typesetting found for class ( ( y crossp z ) ` k ) with typecode class
23	16 22 17	co	Could not format ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) : No typesetting found for class ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) with typecode class
24	13 7 23	cmpt	Could not format ( k e. ( 1 ... 3 ) |-> ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) ) : No typesetting found for class ( k e. ( 1 ... 3 ) |-> ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) ) with typecode class
25	11 24 12	co	Could not format ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) ) ) : No typesetting found for class ( RRfld gsum ( k e. ( 1 ... 3 ) |-> ( ( x ` k ) x. ( ( y crossp z ) ` k ) ) ) ) with typecode class
26	9 10 8 8 25	cmpo	Could not format ( 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 ) ) ) ) ) : No typesetting found for class ( 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 ) ) ) ) ) with typecode class
27	1 8 26	cmpt	Could not format ( 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 ) ) ) ) ) ) : No typesetting found for class ( 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 ) ) ) ) ) ) with typecode class
28	0 27	wceq	Could not format 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 ) ) ) ) ) ) : No typesetting found for wff 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 ) ) ) ) ) ) with typecode wff