Metamath Proof Explorer

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 
|- 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 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cveronese 
 |-  veronese
1 vq 
 |-  q
2 cr 
 |-  RR
3 cmap 
 |-  ^m
4 c1 
 |-  1
5 cfz 
 |-  ...
6 c3 
 |-  3
7 4 6 5 co 
 |-  ( 1 ... 3 )
8 2 7 3 co 
 |-  ( RR ^m ( 1 ... 3 ) )
9 vk 
 |-  k
10 c6 
 |-  6
11 4 10 5 co 
 |-  ( 1 ... 6 )
12 9 cv 
 |-  k
13 12 4 wceq 
 |-  k = 1
14 1 cv 
 |-  q
15 4 14 cfv 
 |-  ( q ` 1 )
16 cexp 
 |-  ^
17 c2 
 |-  2
18 15 17 16 co 
 |-  ( ( q ` 1 ) ^ 2 )
19 cc0 
 |-  0
20 13 18 19 cif 
 |-  if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 )
21 caddc 
 |-  +
22 12 17 wceq 
 |-  k = 2
23 17 14 cfv 
 |-  ( q ` 2 )
24 23 17 16 co 
 |-  ( ( q ` 2 ) ^ 2 )
25 22 24 19 cif 
 |-  if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 )
26 20 25 21 co 
 |-  ( if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 ) )
27 12 6 wceq 
 |-  k = 3
28 6 14 cfv 
 |-  ( q ` 3 )
29 28 17 16 co 
 |-  ( ( q ` 3 ) ^ 2 )
30 27 29 19 cif 
 |-  if ( k = 3 , ( ( q ` 3 ) ^ 2 ) , 0 )
31 26 30 21 co 
 |-  ( ( if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( q ` 3 ) ^ 2 ) , 0 ) )
32 c4 
 |-  4
33 12 32 wceq 
 |-  k = 4
34 cmul 
 |-  x.
35 15 23 34 co 
 |-  ( ( q ` 1 ) x. ( q ` 2 ) )
36 33 35 19 cif 
 |-  if ( k = 4 , ( ( q ` 1 ) x. ( q ` 2 ) ) , 0 )
37 c5 
 |-  5
38 12 37 wceq 
 |-  k = 5
39 23 28 34 co 
 |-  ( ( q ` 2 ) x. ( q ` 3 ) )
40 38 39 19 cif 
 |-  if ( k = 5 , ( ( q ` 2 ) x. ( q ` 3 ) ) , 0 )
41 36 40 21 co 
 |-  ( if ( k = 4 , ( ( q ` 1 ) x. ( q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( q ` 2 ) x. ( q ` 3 ) ) , 0 ) )
42 12 10 wceq 
 |-  k = 6
43 28 15 34 co 
 |-  ( ( q ` 3 ) x. ( q ` 1 ) )
44 42 43 19 cif 
 |-  if ( k = 6 , ( ( q ` 3 ) x. ( q ` 1 ) ) , 0 )
45 41 44 21 co 
 |-  ( ( 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 ) )
46 31 45 21 co 
 |-  ( ( ( 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 ) ) )
47 9 11 46 cmpt 
 |-  ( 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 ) ) ) )
48 1 8 47 cmpt 
 |-  ( 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 ) ) ) ) )
49 0 48 wceq 
 |-  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 ) ) ) ) )