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 = ( 𝑞 ∈ ( ℝ ↑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 ) ) ) ) )

Detailed syntax breakdown

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