Metamath Proof Explorer

Theorem veronesematrowexpd

Description: Currying the Veronese matrix gives the indexed family of Veronese images, with each image expressed explicitly by coordinates. (Contributed by Jiamin Zhao, 19-Aug-2026)

Ref Expression
Hypotheses veronesemat.a 
|- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) )
veronesemat.f 
|- ( ph -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
Assertion veronesematrowexpd 
|- ( ph -> curry V = ( i e. ( 1 ... 6 ) |-> ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( ( A ` i ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` i ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` i ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) , ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 veronesemat.a 
 |-  V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) )
2 veronesemat.f 
 |-  ( ph -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
3 1 2 veronesematrowd 
 |-  ( ph -> curry V = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) )
4 2fveq3 
 |-  ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) )
5 4 cbvmptv 
 |-  ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) = ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) )
6 3 5 eqtrdi 
 |-  ( ph -> curry V = ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) )
7 2 ffvelcdmda 
 |-  ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) )
8 7 veronesevrowd 
 |-  ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( veronese ` ( A ` u ) ) = ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) ) ) ) ) ) ) )
9 8 mpteq2dva 
 |-  ( ph -> ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) = ( u e. ( 1 ... 6 ) |-> ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) ) ) ) ) ) ) ) )
10 6 9 eqtrd 
 |-  ( ph -> curry V = ( u e. ( 1 ... 6 ) |-> ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) ) ) ) ) ) ) ) )
11 fveq2 
 |-  ( u = i -> ( A ` u ) = ( A ` i ) )
12 11 fveq1d 
 |-  ( u = i -> ( ( A ` u ) ` 1 ) = ( ( A ` i ) ` 1 ) )
13 12 oveq1d 
 |-  ( u = i -> ( ( ( A ` u ) ` 1 ) ^ 2 ) = ( ( ( A ` i ) ` 1 ) ^ 2 ) )
14 11 fveq1d 
 |-  ( u = i -> ( ( A ` u ) ` 2 ) = ( ( A ` i ) ` 2 ) )
15 14 oveq1d 
 |-  ( u = i -> ( ( ( A ` u ) ` 2 ) ^ 2 ) = ( ( ( A ` i ) ` 2 ) ^ 2 ) )
16 11 fveq1d 
 |-  ( u = i -> ( ( A ` u ) ` 3 ) = ( ( A ` i ) ` 3 ) )
17 16 oveq1d 
 |-  ( u = i -> ( ( ( A ` u ) ` 3 ) ^ 2 ) = ( ( ( A ` i ) ` 3 ) ^ 2 ) )
18 12 14 oveq12d 
 |-  ( u = i -> ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) = ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) )
19 14 16 oveq12d 
 |-  ( u = i -> ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) = ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) )
20 16 12 oveq12d 
 |-  ( u = i -> ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) = ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) )
21 19 20 ifeq12d 
 |-  ( u = i -> if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) ) = if ( k = 5 , ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) , ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) )
22 18 21 ifeq12d 
 |-  ( u = i -> if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) ) ) = if ( k = 4 , ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) , ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) ) )
23 17 22 ifeq12d 
 |-  ( u = i -> if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) ) ) ) = if ( k = 3 , ( ( ( A ` i ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) , ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) ) ) )
24 15 23 ifeq12d 
 |-  ( u = i -> if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) ) ) ) ) = if ( k = 2 , ( ( ( A ` i ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` i ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) , ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) ) ) ) )
25 13 24 ifeq12d 
 |-  ( u = i -> if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) ) ) ) ) ) = if ( k = 1 , ( ( ( A ` i ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` i ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` i ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) , ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) ) ) ) ) )
26 25 mpteq2dv 
 |-  ( u = i -> ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) ) ) ) ) ) ) = ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( ( A ` i ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` i ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` i ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) , ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) ) ) ) ) ) )
27 26 cbvmptv 
 |-  ( u e. ( 1 ... 6 ) |-> ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) ) ) ) ) ) ) ) = ( i e. ( 1 ... 6 ) |-> ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( ( A ` i ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` i ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` i ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) , ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) ) ) ) ) ) )
28 10 27 eqtrdi 
 |-  ( ph -> curry V = ( i e. ( 1 ... 6 ) |-> ( k e. ( 1 ... 6 ) |-> if ( k = 1 , ( ( ( A ` i ) ` 1 ) ^ 2 ) , if ( k = 2 , ( ( ( A ` i ) ` 2 ) ^ 2 ) , if ( k = 3 , ( ( ( A ` i ) ` 3 ) ^ 2 ) , if ( k = 4 , ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) , if ( k = 5 , ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) , ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) ) ) ) ) ) ) )