Definition df-tripp 50662

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 50661	. 2 class tripp
2		vx	. . 3 setvar 𝑥
3		cr 11103	. . . 4 class ℝ
4		c1 11105	. . . . 5 class 1
5		c3 12300	. . . . 5 class 3
6		cfz 13539	. . . . 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 21763	. . . . 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 50659	. . . . . . . . 9 class ⊠
20	17, 18, 19	co 7410	. . . . . . . 8 class (𝑦⊠𝑧)
21	14, 20	cfv 6536	. . . . . . 7 class ((𝑦⊠𝑧)‘𝑘)
22		cmul 11109	. . . . . . 7 class ·
23	16, 21, 22	co 7410	. . . . . 6 class ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘))
24	13, 7, 23	cmpt 5192	. . . . 5 class (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘)))
25		cgsu 17497	. . . . 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 used by:  crosspdot0i  50672