Definition df-tripp

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctripp	⊢ tripp
1		vx	⊢ 𝑥
2		cr	⊢ ℝ
3		cmap	⊢ ↑m
4		c1	⊢ 1
5		cfz	⊢ ...
6		c3	⊢ 3
7	4 6 5	co	⊢ ( 1 ... 3 )
8	2 7 3	co	⊢ ( ℝ ↑m ( 1 ... 3 ) )
9		vy	⊢ 𝑦
10		vz	⊢ 𝑧
11		crefld	⊢ ℝfld
12		cgsu	⊢ Σg
13		vk	⊢ 𝑘
14	1	cv	⊢ 𝑥
15	13	cv	⊢ 𝑘
16	15 14	cfv	⊢ ( 𝑥 ‘ 𝑘 )
17		cmul	⊢ ·
18	9	cv	⊢ 𝑦
19		ccrossp	⊢ ⊠
20	10	cv	⊢ 𝑧
21	18 20 19	co	⊢ ( 𝑦 ⊠ 𝑧 )
22	15 21	cfv	⊢ ( ( 𝑦 ⊠ 𝑧 ) ‘ 𝑘 )
23	16 22 17	co	⊢ ( ( 𝑥 ‘ 𝑘 ) · ( ( 𝑦 ⊠ 𝑧 ) ‘ 𝑘 ) )
24	13 7 23	cmpt	⊢ ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑥 ‘ 𝑘 ) · ( ( 𝑦 ⊠ 𝑧 ) ‘ 𝑘 ) ) )
25	11 24 12	co	⊢ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑥 ‘ 𝑘 ) · ( ( 𝑦 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) )
26	9 10 8 8 25	cmpo	⊢ ( 𝑦 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑥 ‘ 𝑘 ) · ( ( 𝑦 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) )
27	1 8 26	cmpt	⊢ ( 𝑥 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( 𝑦 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑥 ‘ 𝑘 ) · ( ( 𝑦 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) )
28	0 27	wceq	⊢ tripp = ( 𝑥 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( 𝑦 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑧 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( ℝfld Σg ( 𝑘 ∈ ( 1 ... 3 ) ↦ ( ( 𝑥 ‘ 𝑘 ) · ( ( 𝑦 ⊠ 𝑧 ) ‘ 𝑘 ) ) ) ) ) )