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 
|- ( ph -> P e. ( RR ^m ( 1 ... 3 ) ) )
Assertion veronesevald 
|- ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 veroneseval.1 
 |-  ( ph -> P e. ( RR ^m ( 1 ... 3 ) ) )
2 fveq1 
 |-  ( q = P -> ( q ` 1 ) = ( P ` 1 ) )
3 2 oveq1d 
 |-  ( q = P -> ( ( q ` 1 ) ^ 2 ) = ( ( P ` 1 ) ^ 2 ) )
4 3 ifeq1d 
 |-  ( q = P -> if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 ) = if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) )
5 fveq1 
 |-  ( q = P -> ( q ` 2 ) = ( P ` 2 ) )
6 5 oveq1d 
 |-  ( q = P -> ( ( q ` 2 ) ^ 2 ) = ( ( P ` 2 ) ^ 2 ) )
7 6 ifeq1d 
 |-  ( q = P -> if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 ) = if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) )
8 4 7 oveq12d 
 |-  ( q = P -> ( if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 ) ) = ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) )
9 fveq1 
 |-  ( q = P -> ( q ` 3 ) = ( P ` 3 ) )
10 9 oveq1d 
 |-  ( q = P -> ( ( q ` 3 ) ^ 2 ) = ( ( P ` 3 ) ^ 2 ) )
11 10 ifeq1d 
 |-  ( q = P -> if ( k = 3 , ( ( q ` 3 ) ^ 2 ) , 0 ) = if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) )
12 8 11 oveq12d 
 |-  ( q = P -> ( ( if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( q ` 3 ) ^ 2 ) , 0 ) ) = ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) )
13 2 5 oveq12d 
 |-  ( q = P -> ( ( q ` 1 ) x. ( q ` 2 ) ) = ( ( P ` 1 ) x. ( P ` 2 ) ) )
14 13 ifeq1d 
 |-  ( q = P -> if ( k = 4 , ( ( q ` 1 ) x. ( q ` 2 ) ) , 0 ) = if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) )
15 5 9 oveq12d 
 |-  ( q = P -> ( ( q ` 2 ) x. ( q ` 3 ) ) = ( ( P ` 2 ) x. ( P ` 3 ) ) )
16 15 ifeq1d 
 |-  ( q = P -> if ( k = 5 , ( ( q ` 2 ) x. ( q ` 3 ) ) , 0 ) = if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) )
17 14 16 oveq12d 
 |-  ( q = P -> ( if ( k = 4 , ( ( q ` 1 ) x. ( q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( q ` 2 ) x. ( q ` 3 ) ) , 0 ) ) = ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) )
18 9 2 oveq12d 
 |-  ( q = P -> ( ( q ` 3 ) x. ( q ` 1 ) ) = ( ( P ` 3 ) x. ( P ` 1 ) ) )
19 18 ifeq1d 
 |-  ( q = P -> if ( k = 6 , ( ( q ` 3 ) x. ( q ` 1 ) ) , 0 ) = if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) )
20 17 19 oveq12d 
 |-  ( q = P -> ( ( 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 ) ) = ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) )
21 12 20 oveq12d 
 |-  ( q = P -> ( ( ( 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 ) ) ) = ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) )
22 21 mpteq2dv 
 |-  ( q = P -> ( 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 ) ) ) ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) )
23 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 ) ) ) ) )
24 ovex 
 |-  ( 1 ... 6 ) e. _V
25 24 mptex 
 |-  ( 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 ) ) ) ) e. _V
26 22 23 25 fvmpt3i 
 |-  ( P e. ( RR ^m ( 1 ... 3 ) ) -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) )
27 1 26 syl 
 |-  ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) )