Metamath Proof Explorer

Theorem veronesematrowd

Description: Currying the Veronese matrix gives the indexed family of Veronese images of the points Ai . (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 veronesematrowd 
|- ( ph -> curry V = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) )

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 2fveq3 
 |-  ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) )
4 3 fveq1d 
 |-  ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) )
5 fveq2 
 |-  ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) )
6 4 5 cbvmpov 
 |-  ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
7 1 6 eqtri 
 |-  V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
8 2 adantr 
 |-  ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
9 simprl 
 |-  ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> u e. ( 1 ... 6 ) )
10 8 9 ffvelcdmd 
 |-  ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) )
11 simprr 
 |-  ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> v e. ( 1 ... 6 ) )
12 veronesefvcl 
 |-  ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
13 10 11 12 syl2anc 
 |-  ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
14 13 ralrimivva 
 |-  ( ph -> A. u e. ( 1 ... 6 ) A. v e. ( 1 ... 6 ) ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
15 1nn 
 |-  1 e. NN
16 6nn 
 |-  6 e. NN
17 1re 
 |-  1 e. RR
18 6re 
 |-  6 e. RR
19 1lt6 
 |-  1 < 6
20 17 18 19 ltleii 
 |-  1 <_ 6
21 elfz1b 
 |-  ( 1 e. ( 1 ... 6 ) <-> ( 1 e. NN /\ 6 e. NN /\ 1 <_ 6 ) )
22 15 16 20 21 mpbir3an 
 |-  1 e. ( 1 ... 6 )
23 22 ne0ii 
 |-  ( 1 ... 6 ) =/= (/)
24 23 a1i 
 |-  ( ph -> ( 1 ... 6 ) =/= (/) )
25 7 14 24 mpocurryd 
 |-  ( ph -> curry V = ( u e. ( 1 ... 6 ) |-> ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) )
26 ovex 
 |-  ( ( ( if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , 0 ) + if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) , 0 ) ) ) e. _V
27 eqid 
 |-  ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , 0 ) + if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) , 0 ) ) ) ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , 0 ) + if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) , 0 ) ) ) )
28 26 27 fnmpti 
 |-  ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , 0 ) + if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) , 0 ) ) ) ) Fn ( 1 ... 6 )
29 2 ffvelcdmda 
 |-  ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) )
30 29 veronesevald 
 |-  ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( veronese ` ( A ` u ) ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , 0 ) + if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) , 0 ) ) ) ) )
31 30 fneq1d 
 |-  ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) Fn ( 1 ... 6 ) <-> ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( ( A ` u ) ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( ( A ` u ) ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( ( A ` u ) ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( ( A ` u ) ` 1 ) x. ( ( A ` u ) ` 2 ) ) , 0 ) + if ( k = 5 , ( ( ( A ` u ) ` 2 ) x. ( ( A ` u ) ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( ( A ` u ) ` 3 ) x. ( ( A ` u ) ` 1 ) ) , 0 ) ) ) ) Fn ( 1 ... 6 ) ) )
32 28 31 mpbiri 
 |-  ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( veronese ` ( A ` u ) ) Fn ( 1 ... 6 ) )
33 dffn5 
 |-  ( ( veronese ` ( A ` u ) ) Fn ( 1 ... 6 ) <-> ( veronese ` ( A ` u ) ) = ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) )
34 32 33 sylib 
 |-  ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( veronese ` ( A ` u ) ) = ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) )
35 34 eqcomd 
 |-  ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) = ( veronese ` ( A ` u ) ) )
36 35 mpteq2dva 
 |-  ( ph -> ( u e. ( 1 ... 6 ) |-> ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) = ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) )
37 25 36 eqtrd 
 |-  ( ph -> curry V = ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) )
38 2fveq3 
 |-  ( u = i -> ( veronese ` ( A ` u ) ) = ( veronese ` ( A ` i ) ) )
39 38 cbvmptv 
 |-  ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) )
40 37 39 eqtrdi 
 |-  ( ph -> curry V = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) )