Definition df-tripp 50694

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 (𝑦 and 𝑧). Apply as (𝑦(tripp‘𝑥)𝑧). Vectors are represented as functions on (1...3). (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 50693	. 2 class tripp
2		vx	. . 3 setvar 𝑥
3		cr 11116	. . . 4 class ℝ
4		c1 11118	. . . . 5 class 1
5		c3 12313	. . . . 5 class 3
6		cfz 13553	. . . . 5 class ...
7	4, 5, 6	co 7419	. . . 4 class (1...3)
8		cmap 8830	. . . 4 class ↑m
9	3, 7, 8	co 7419	. . 3 class (ℝ ↑m (1...3))
10		vy	. . . 4 setvar 𝑦
11		vz	. . . 4 setvar 𝑧
12		crefld 21806	. . . . 5 class ℝfld
13		vk	. . . . . 6 setvar 𝑘
14	13	cv 1569	. . . . . . . 8 class 𝑘
15	2	cv 1569	. . . . . . . 8 class 𝑥
16	14, 15	cfv 6540	. . . . . . 7 class (𝑥‘𝑘)
17	10	cv 1569	. . . . . . . . 9 class 𝑦
18	11	cv 1569	. . . . . . . . 9 class 𝑧
19		ccrossp 50691	. . . . . . . . 9 class ⊠
20	17, 18, 19	co 7419	. . . . . . . 8 class (𝑦⊠𝑧)
21	14, 20	cfv 6540	. . . . . . 7 class ((𝑦⊠𝑧)‘𝑘)
22		cmul 11122	. . . . . . 7 class ·
23	16, 21, 22	co 7419	. . . . . 6 class ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘))
24	13, 7, 23	cmpt 5194	. . . . 5 class (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘)))
25		cgsu 17517	. . . . 5 class Σg
26	12, 24, 25	co 7419	. . . 4 class (ℝfld Σg (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘))))
27	10, 11, 9, 9, 26	cmpo 7421	. . 3 class (𝑦 ∈ (ℝ ↑m (1...3)), 𝑧 ∈ (ℝ ↑m (1...3)) ↦ (ℝfld Σg (𝑘 ∈ (1...3) ↦ ((𝑥‘𝑘) · ((𝑦⊠𝑧)‘𝑘)))))
28	2, 9, 27	cmpt 5194	. 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:  crosspdot0lem  50704