Definition df-veronese 50784

Description: Define the quadratic Veronese map on real 3-vectors, with coordinates ordered as ( x^2 , y^2 , z^2 , x y , y z , z x ). (Contributed by Jiamin Zhao, 14-Aug-2026.)

Assertion

Ref	Expression
df-veronese	⊢ veronese = (𝑞 ∈ (ℝ ↑m (1...3)) ↦ (𝑘 ∈ (1...6) ↦ (((if(𝑘 = 1, ((𝑞‘1)↑2), 0) + if(𝑘 = 2, ((𝑞‘2)↑2), 0)) + if(𝑘 = 3, ((𝑞‘3)↑2), 0)) + ((if(𝑘 = 4, ((𝑞‘1) · (𝑞‘2)), 0) + if(𝑘 = 5, ((𝑞‘2) · (𝑞‘3)), 0)) + if(𝑘 = 6, ((𝑞‘3) · (𝑞‘1)), 0)))))

Distinct variable group:   𝑘,𝑞

Detailed syntax breakdown of Definition df-veronese

Step	Hyp	Ref	Expression
1		cveronese 50783	. 2 class veronese
2		vq	. . 3 setvar 𝑞
3		cr 11124	. . . 4 class ℝ
4		c1 11126	. . . . 5 class 1
5		c3 12321	. . . . 5 class 3
6		cfz 13561	. . . . 5 class ...
7	4, 5, 6	co 7416	. . . 4 class (1...3)
8		cmap 8829	. . . 4 class ↑m
9	3, 7, 8	co 7416	. . 3 class (ℝ ↑m (1...3))
10		vk	. . . 4 setvar 𝑘
11		c6 12324	. . . . 5 class 6
12	4, 11, 6	co 7416	. . . 4 class (1...6)
13	10	cv 1569	. . . . . . . . 9 class 𝑘
14	13, 4	wceq 1570	. . . . . . . 8 wff 𝑘 = 1
15	2	cv 1569	. . . . . . . . . 10 class 𝑞
16	4, 15	cfv 6537	. . . . . . . . 9 class (𝑞‘1)
17		c2 12320	. . . . . . . . 9 class 2
18		cexp 14125	. . . . . . . . 9 class ↑
19	16, 17, 18	co 7416	. . . . . . . 8 class ((𝑞‘1)↑2)
20		cc0 11125	. . . . . . . 8 class 0
21	14, 19, 20	cif 4485	. . . . . . 7 class if(𝑘 = 1, ((𝑞‘1)↑2), 0)
22	13, 17	wceq 1570	. . . . . . . 8 wff 𝑘 = 2
23	17, 15	cfv 6537	. . . . . . . . 9 class (𝑞‘2)
24	23, 17, 18	co 7416	. . . . . . . 8 class ((𝑞‘2)↑2)
25	22, 24, 20	cif 4485	. . . . . . 7 class if(𝑘 = 2, ((𝑞‘2)↑2), 0)
26		caddc 11128	. . . . . . 7 class +
27	21, 25, 26	co 7416	. . . . . 6 class (if(𝑘 = 1, ((𝑞‘1)↑2), 0) + if(𝑘 = 2, ((𝑞‘2)↑2), 0))
28	13, 5	wceq 1570	. . . . . . 7 wff 𝑘 = 3
29	5, 15	cfv 6537	. . . . . . . 8 class (𝑞‘3)
30	29, 17, 18	co 7416	. . . . . . 7 class ((𝑞‘3)↑2)
31	28, 30, 20	cif 4485	. . . . . 6 class if(𝑘 = 3, ((𝑞‘3)↑2), 0)
32	27, 31, 26	co 7416	. . . . 5 class ((if(𝑘 = 1, ((𝑞‘1)↑2), 0) + if(𝑘 = 2, ((𝑞‘2)↑2), 0)) + if(𝑘 = 3, ((𝑞‘3)↑2), 0))
33		c4 12322	. . . . . . . . 9 class 4
34	13, 33	wceq 1570	. . . . . . . 8 wff 𝑘 = 4
35		cmul 11130	. . . . . . . . 9 class ·
36	16, 23, 35	co 7416	. . . . . . . 8 class ((𝑞‘1) · (𝑞‘2))
37	34, 36, 20	cif 4485	. . . . . . 7 class if(𝑘 = 4, ((𝑞‘1) · (𝑞‘2)), 0)
38		c5 12323	. . . . . . . . 9 class 5
39	13, 38	wceq 1570	. . . . . . . 8 wff 𝑘 = 5
40	23, 29, 35	co 7416	. . . . . . . 8 class ((𝑞‘2) · (𝑞‘3))
41	39, 40, 20	cif 4485	. . . . . . 7 class if(𝑘 = 5, ((𝑞‘2) · (𝑞‘3)), 0)
42	37, 41, 26	co 7416	. . . . . 6 class (if(𝑘 = 4, ((𝑞‘1) · (𝑞‘2)), 0) + if(𝑘 = 5, ((𝑞‘2) · (𝑞‘3)), 0))
43	13, 11	wceq 1570	. . . . . . 7 wff 𝑘 = 6
44	29, 16, 35	co 7416	. . . . . . 7 class ((𝑞‘3) · (𝑞‘1))
45	43, 44, 20	cif 4485	. . . . . 6 class if(𝑘 = 6, ((𝑞‘3) · (𝑞‘1)), 0)
46	42, 45, 26	co 7416	. . . . 5 class ((if(𝑘 = 4, ((𝑞‘1) · (𝑞‘2)), 0) + if(𝑘 = 5, ((𝑞‘2) · (𝑞‘3)), 0)) + if(𝑘 = 6, ((𝑞‘3) · (𝑞‘1)), 0))
47	32, 46, 26	co 7416	. . . 4 class (((if(𝑘 = 1, ((𝑞‘1)↑2), 0) + if(𝑘 = 2, ((𝑞‘2)↑2), 0)) + if(𝑘 = 3, ((𝑞‘3)↑2), 0)) + ((if(𝑘 = 4, ((𝑞‘1) · (𝑞‘2)), 0) + if(𝑘 = 5, ((𝑞‘2) · (𝑞‘3)), 0)) + if(𝑘 = 6, ((𝑞‘3) · (𝑞‘1)), 0)))
48	10, 12, 47	cmpt 5190	. . 3 class (𝑘 ∈ (1...6) ↦ (((if(𝑘 = 1, ((𝑞‘1)↑2), 0) + if(𝑘 = 2, ((𝑞‘2)↑2), 0)) + if(𝑘 = 3, ((𝑞‘3)↑2), 0)) + ((if(𝑘 = 4, ((𝑞‘1) · (𝑞‘2)), 0) + if(𝑘 = 5, ((𝑞‘2) · (𝑞‘3)), 0)) + if(𝑘 = 6, ((𝑞‘3) · (𝑞‘1)), 0))))
49	2, 9, 48	cmpt 5190	. 2 class (𝑞 ∈ (ℝ ↑m (1...3)) ↦ (𝑘 ∈ (1...6) ↦ (((if(𝑘 = 1, ((𝑞‘1)↑2), 0) + if(𝑘 = 2, ((𝑞‘2)↑2), 0)) + if(𝑘 = 3, ((𝑞‘3)↑2), 0)) + ((if(𝑘 = 4, ((𝑞‘1) · (𝑞‘2)), 0) + if(𝑘 = 5, ((𝑞‘2) · (𝑞‘3)), 0)) + if(𝑘 = 6, ((𝑞‘3) · (𝑞‘1)), 0)))))
50	1, 49	wceq 1570	1 wff veronese = (𝑞 ∈ (ℝ ↑m (1...3)) ↦ (𝑘 ∈ (1...6) ↦ (((if(𝑘 = 1, ((𝑞‘1)↑2), 0) + if(𝑘 = 2, ((𝑞‘2)↑2), 0)) + if(𝑘 = 3, ((𝑞‘3)↑2), 0)) + ((if(𝑘 = 4, ((𝑞‘1) · (𝑞‘2)), 0) + if(𝑘 = 5, ((𝑞‘2) · (𝑞‘3)), 0)) + if(𝑘 = 6, ((𝑞‘3) · (𝑞‘1)), 0)))))

This definition is used by:  veronesevald  50786