Definition df-veronese

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)

	Ref	Expression
Assertion	df-veronese	Could not format assertion : No typesetting found for |- veronese = ( q e. ( RR ^m ( 1 ... 3 ) ) |-> ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( q ` 1 ) x. ( q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( q ` 2 ) x. ( q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( q ` 3 ) x. ( q ` 1 ) ) , 0 ) ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cveronese	Could not format veronese : No typesetting found for class veronese with typecode class
1		vq	$$setvarq$$
2		cr	$$classℝ$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4		c1	$$class1$$
5		cfz	$$class\dots$$
6		c3	$$class3$$
7	4 6 5	co	$$class\left(1\dots 3\right)$$
8	2 7 3	co	$$class\left({ℝ}^{\left(1\dots 3\right)}\right)$$
9		vk	$$setvark$$
10		c6	$$class6$$
11	4 10 5	co	$$class\left(1\dots 6\right)$$
12	9	cv	$$setvark$$
13	12 4	wceq	$$wffk=1$$
14	1	cv	$$setvarq$$
15	4 14	cfv	$$classq\left(1\right)$$
16		cexp	$$class^$$
17		c2	$$class2$$
18	15 17 16	co	$$class{q\left(1\right)}^2$$
19		cc0	$$class0$$
20	13 18 19	cif	$$classif\left(k=1,{q\left(1\right)}^2,0\right)$$
21		caddc	$$class+$$
22	12 17	wceq	$$wffk=2$$
23	17 14	cfv	$$classq\left(2\right)$$
24	23 17 16	co	$$class{q\left(2\right)}^2$$
25	22 24 19	cif	$$classif\left(k=2,{q\left(2\right)}^2,0\right)$$
26	20 25 21	co	$$class\left(if\left(k=1,{q\left(1\right)}^2,0\right)+if\left(k=2,{q\left(2\right)}^2,0\right)\right)$$
27	12 6	wceq	$$wffk=3$$
28	6 14	cfv	$$classq\left(3\right)$$
29	28 17 16	co	$$class{q\left(3\right)}^2$$
30	27 29 19	cif	$$classif\left(k=3,{q\left(3\right)}^2,0\right)$$
31	26 30 21	co	$$class\left(if\left(k=1,{q\left(1\right)}^2,0\right)+if\left(k=2,{q\left(2\right)}^2,0\right)+if\left(k=3,{q\left(3\right)}^2,0\right)\right)$$
32		c4	$$class4$$
33	12 32	wceq	$$wffk=4$$
34		cmul	$$class\times$$
35	15 23 34	co	$$classq\left(1\right)q\left(2\right)$$
36	33 35 19	cif	$$classif\left(k=4,q\left(1\right)q\left(2\right),0\right)$$
37		c5	$$class5$$
38	12 37	wceq	$$wffk=5$$
39	23 28 34	co	$$classq\left(2\right)q\left(3\right)$$
40	38 39 19	cif	$$classif\left(k=5,q\left(2\right)q\left(3\right),0\right)$$
41	36 40 21	co	$$class\left(if\left(k=4,q\left(1\right)q\left(2\right),0\right)+if\left(k=5,q\left(2\right)q\left(3\right),0\right)\right)$$
42	12 10	wceq	$$wffk=6$$
43	28 15 34	co	$$classq\left(3\right)q\left(1\right)$$
44	42 43 19	cif	$$classif\left(k=6,q\left(3\right)q\left(1\right),0\right)$$
45	41 44 21	co	$$class\left(if\left(k=4,q\left(1\right)q\left(2\right),0\right)+if\left(k=5,q\left(2\right)q\left(3\right),0\right)+if\left(k=6,q\left(3\right)q\left(1\right),0\right)\right)$$
46	31 45 21	co	$$class\left(\left(if\left(k=1,{q\left(1\right)}^2,0\right)+if\left(k=2,{q\left(2\right)}^2,0\right)\right)+if\left(k=3,{q\left(3\right)}^2,0\right)+\left(if\left(k=4,q\left(1\right)q\left(2\right),0\right)+if\left(k=5,q\left(2\right)q\left(3\right),0\right)\right)+if\left(k=6,q\left(3\right)q\left(1\right),0\right)\right)$$
47	9 11 46	cmpt	$$class\left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{q\left(1\right)}^2,0\right)+if\left(k=2,{q\left(2\right)}^2,0\right)\right)+if\left(k=3,{q\left(3\right)}^2,0\right)+\left(if\left(k=4,q\left(1\right)q\left(2\right),0\right)+if\left(k=5,q\left(2\right)q\left(3\right),0\right)\right)+if\left(k=6,q\left(3\right)q\left(1\right),0\right)\right)$$
48	1 8 47	cmpt	$$class\left(q\in \left({ℝ}^{\left(1\dots 3\right)}\right)⟼\left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{q\left(1\right)}^2,0\right)+if\left(k=2,{q\left(2\right)}^2,0\right)\right)+if\left(k=3,{q\left(3\right)}^2,0\right)+\left(if\left(k=4,q\left(1\right)q\left(2\right),0\right)+if\left(k=5,q\left(2\right)q\left(3\right),0\right)\right)+if\left(k=6,q\left(3\right)q\left(1\right),0\right)\right)\right)$$
49	0 48	wceq	Could not format veronese = ( q e. ( RR ^m ( 1 ... 3 ) ) |-> ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( q ` 1 ) x. ( q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( q ` 2 ) x. ( q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( q ` 3 ) x. ( q ` 1 ) ) , 0 ) ) ) ) ) : No typesetting found for wff veronese = ( q e. ( RR ^m ( 1 ... 3 ) ) |-> ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( q ` 1 ) x. ( q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( q ` 2 ) x. ( q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( q ` 3 ) x. ( q ` 1 ) ) , 0 ) ) ) ) ) with typecode wff