Metamath Proof Explorer

Theorem veronesevald

Description: Value of the Veronese map at a point, expressed as a maps-to function on the six coordinates. (Contributed by Jiamin Zhao, 14-Aug-2026)

Ref Expression
Hypothesis veroneseval.1 ⊢ ( 𝜑 → 𝑃 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
Assertion veronesevald ( 𝜑 → ( veronese ‘ 𝑃 ) = ( 𝑘 ∈ ( 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 veroneseval.1 ⊢ ( 𝜑 → 𝑃 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
2 fveq1 ⊢ ( 𝑞 = 𝑃 → ( 𝑞 ‘ 1 ) = ( 𝑃 ‘ 1 ) )
3 2 oveq1d ⊢ ( 𝑞 = 𝑃 → ( ( 𝑞 ‘ 1 ) ↑ 2 ) = ( ( 𝑃 ‘ 1 ) ↑ 2 ) )
4 3 ifeq1d ⊢ ( 𝑞 = 𝑃 → if ( 𝑘 = 1 , ( ( 𝑞 ‘ 1 ) ↑ 2 ) , 0 ) = if ( 𝑘 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) )
5 fveq1 ⊢ ( 𝑞 = 𝑃 → ( 𝑞 ‘ 2 ) = ( 𝑃 ‘ 2 ) )
6 5 oveq1d ⊢ ( 𝑞 = 𝑃 → ( ( 𝑞 ‘ 2 ) ↑ 2 ) = ( ( 𝑃 ‘ 2 ) ↑ 2 ) )
7 6 ifeq1d ⊢ ( 𝑞 = 𝑃 → if ( 𝑘 = 2 , ( ( 𝑞 ‘ 2 ) ↑ 2 ) , 0 ) = if ( 𝑘 = 2 , ( ( 𝑃 ‘ 2 ) ↑ 2 ) , 0 ) )
8 4 7 oveq12d ⊢ ( 𝑞 = 𝑃 → ( if ( 𝑘 = 1 , ( ( 𝑞 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑞 ‘ 2 ) ↑ 2 ) , 0 ) ) = ( if ( 𝑘 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑃 ‘ 2 ) ↑ 2 ) , 0 ) ) )
9 fveq1 ⊢ ( 𝑞 = 𝑃 → ( 𝑞 ‘ 3 ) = ( 𝑃 ‘ 3 ) )
10 9 oveq1d ⊢ ( 𝑞 = 𝑃 → ( ( 𝑞 ‘ 3 ) ↑ 2 ) = ( ( 𝑃 ‘ 3 ) ↑ 2 ) )
11 10 ifeq1d ⊢ ( 𝑞 = 𝑃 → if ( 𝑘 = 3 , ( ( 𝑞 ‘ 3 ) ↑ 2 ) , 0 ) = if ( 𝑘 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) )
12 8 11 oveq12d ⊢ ( 𝑞 = 𝑃 → ( ( if ( 𝑘 = 1 , ( ( 𝑞 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑞 ‘ 2 ) ↑ 2 ) , 0 ) ) + if ( 𝑘 = 3 , ( ( 𝑞 ‘ 3 ) ↑ 2 ) , 0 ) ) = ( ( if ( 𝑘 = 1 , ( ( 𝑃 ‘ 1 ) ↑ 2 ) , 0 ) + if ( 𝑘 = 2 , ( ( 𝑃 ‘ 2 ) ↑ 2 ) , 0 ) ) + if ( 𝑘 = 3 , ( ( 𝑃 ‘ 3 ) ↑ 2 ) , 0 ) ) )
13 2 5 oveq12d ⊢ ( 𝑞 = 𝑃 → ( ( 𝑞 ‘ 1 ) · ( 𝑞 ‘ 2 ) ) = ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) )
14 13 ifeq1d ⊢ ( 𝑞 = 𝑃 → if ( 𝑘 = 4 , ( ( 𝑞 ‘ 1 ) · ( 𝑞 ‘ 2 ) ) , 0 ) = if ( 𝑘 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) )
15 5 9 oveq12d ⊢ ( 𝑞 = 𝑃 → ( ( 𝑞 ‘ 2 ) · ( 𝑞 ‘ 3 ) ) = ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) )
16 15 ifeq1d ⊢ ( 𝑞 = 𝑃 → if ( 𝑘 = 5 , ( ( 𝑞 ‘ 2 ) · ( 𝑞 ‘ 3 ) ) , 0 ) = if ( 𝑘 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) )
17 14 16 oveq12d ⊢ ( 𝑞 = 𝑃 → ( if ( 𝑘 = 4 , ( ( 𝑞 ‘ 1 ) · ( 𝑞 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑞 ‘ 2 ) · ( 𝑞 ‘ 3 ) ) , 0 ) ) = ( if ( 𝑘 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) )
18 9 2 oveq12d ⊢ ( 𝑞 = 𝑃 → ( ( 𝑞 ‘ 3 ) · ( 𝑞 ‘ 1 ) ) = ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) )
19 18 ifeq1d ⊢ ( 𝑞 = 𝑃 → if ( 𝑘 = 6 , ( ( 𝑞 ‘ 3 ) · ( 𝑞 ‘ 1 ) ) , 0 ) = if ( 𝑘 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) )
20 17 19 oveq12d ⊢ ( 𝑞 = 𝑃 → ( ( if ( 𝑘 = 4 , ( ( 𝑞 ‘ 1 ) · ( 𝑞 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑞 ‘ 2 ) · ( 𝑞 ‘ 3 ) ) , 0 ) ) + if ( 𝑘 = 6 , ( ( 𝑞 ‘ 3 ) · ( 𝑞 ‘ 1 ) ) , 0 ) ) = ( ( if ( 𝑘 = 4 , ( ( 𝑃 ‘ 1 ) · ( 𝑃 ‘ 2 ) ) , 0 ) + if ( 𝑘 = 5 , ( ( 𝑃 ‘ 2 ) · ( 𝑃 ‘ 3 ) ) , 0 ) ) + if ( 𝑘 = 6 , ( ( 𝑃 ‘ 3 ) · ( 𝑃 ‘ 1 ) ) , 0 ) ) )
21 12 20 oveq12d ⊢ ( 𝑞 = 𝑃 → ( ( ( 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 ) ) ) = ( ( ( 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 ) ) ) )
22 21 mpteq2dv ⊢ ( 𝑞 = 𝑃 → ( 𝑘 ∈ ( 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 ) ) ) ) = ( 𝑘 ∈ ( 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 ) ) ) ) )
23 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 ) ) ) ) )
24 ovex ⊢ ( 1 ... 6 ) ∈ V
25 24 mptex ⊢ ( 𝑘 ∈ ( 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 ) ) ) ) ∈ V
26 22 23 25 fvmpt3i ⊢ ( 𝑃 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( veronese ‘ 𝑃 ) = ( 𝑘 ∈ ( 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 ) ) ) ) )
27 1 26 syl ⊢ ( 𝜑 → ( veronese ‘ 𝑃 ) = ( 𝑘 ∈ ( 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 ) ) ) ) )