Definition df-tripp 50654

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 (𝑦(tripp‘𝑥)𝑧). (Contributed by Jiamin Zhao, 31-Jul-2026.)

Assertion

Ref	Expression
df-tripp	⊢ tripp = (𝑥 ∈ (ℝ ↑m (1...3)) ↦ (𝑦 ∈ (ℝ ↑m (1...3)), 𝑧 ∈ (ℝ ↑m (1...3)) ↦ (ℝfld Σg (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘))))))

Distinct variable group:   𝑥,𝑘,𝑦,𝑧

Detailed syntax breakdown of Definition df-tripp

Step	Hyp	Ref	Expression
1		ctripp 50653	. 2 class tripp
2		vx	. . 3 setvar 𝑥
3		cr 11094	. . . 4 class ℝ
4		c1 11096	. . . . 5 class 1
5		c3 12291	. . . . 5 class 3
6		cfz 13530	. . . . 5 class ...
7	4, 5, 6	co 7410	. . . 4 class (1...3)
8		cmap 8820	. . . 4 class ↑m
9	3, 7, 8	co 7410	. . 3 class (ℝ ↑m (1...3))
10		vy	. . . 4 setvar 𝑦
11		vz	. . . 4 setvar 𝑧
12		crefld 21754	. . . . 5 class ℝfld
13		vk	. . . . . 6 setvar 𝑘
14	13	cv 1569	. . . . . . . 8 class 𝑘
15	2	cv 1569	. . . . . . . 8 class 𝑥
16	14, 15	cfv 6536	. . . . . . 7 class (𝑥‘𝑘)
17	10	cv 1569	. . . . . . . . 9 class 𝑦
18	11	cv 1569	. . . . . . . . 9 class 𝑧
19		ccrossp 50651	. . . . . . . . 9 class ⊠
20	17, 18, 19	co 7410	. . . . . . . 8 class (𝑦⊠𝑧)
21	14, 20	cfv 6536	. . . . . . 7 class ((𝑦⊠𝑧)‘𝑘)
22		cmul 11100	. . . . . . 7 class ·
23	16, 21, 22	co 7410	. . . . . 6 class ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘))
24	13, 7, 23	cmpt 5192	. . . . 5 class (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘)))
25		cgsu 17488	. . . . 5 class Σg
26	12, 24, 25	co 7410	. . . 4 class (ℝfld Σg (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘))))
27	10, 11, 9, 9, 26	cmpo 7412	. . 3 class (𝑦 ∈ (ℝ ↑m (1...3)), 𝑧 ∈ (ℝ ↑m (1...3)) ↦ (ℝfld Σg (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘)))))
28	2, 9, 27	cmpt 5192	. 2 class (𝑥 ∈ (ℝ ↑m (1...3)) ↦ (𝑦 ∈ (ℝ ↑m (1...3)), 𝑧 ∈ (ℝ ↑m (1...3)) ↦ (ℝfld Σg (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘))))))
29	1, 28	wceq 1570	1 wff tripp = (𝑥 ∈ (ℝ ↑m (1...3)) ↦ (𝑦 ∈ (ℝ ↑m (1...3)), 𝑧 ∈ (ℝ ↑m (1...3)) ↦ (ℝfld Σg (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘))))))

This definition is referenced by:  crosspdot0i  50664