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 ⊢ 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) )
veronesemat.f ⊢ ( 𝜑 → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
Assertion veronesematrowd ( 𝜑 → curry 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ) )

Proof

Step Hyp Ref Expression
1 veronesemat.a ⊢ 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) )
2 veronesemat.f ⊢ ( 𝜑 → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
3 2fveq3 ⊢ ( 𝑖 = 𝑢 → ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) = ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) )
4 3 fveq1d ⊢ ( 𝑖 = 𝑢 → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑗 ) )
5 fveq2 ⊢ ( 𝑗 = 𝑣 → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
6 4 5 cbvmpov ⊢ ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) ) = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
7 1 6 eqtri ⊢ 𝑉 = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
8 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... 6 ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) ) → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
9 simprl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... 6 ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) ) → 𝑢 ∈ ( 1 ... 6 ) )
10 8 9 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... 6 ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) ) → ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
11 simprr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... 6 ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) ) → 𝑣 ∈ ( 1 ... 6 ) )
12 veronesefvcl ⊢ ( ( ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
13 10 11 12 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... 6 ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
14 13 ralrimivva ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 1 ... 6 ) ∀ 𝑣 ∈ ( 1 ... 6 ) ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
15 1nn ⊢ 1 ∈ ℕ
16 6nn ⊢ 6 ∈ ℕ
17 1re ⊢ 1 ∈ ℝ
18 6re ⊢ 6 ∈ ℝ
19 1lt6 ⊢ 1 < 6
20 17 18 19 ltleii ⊢ 1 ≤ 6
21 elfz1b ⊢ ( 1 ∈ ( 1 ... 6 ) ↔ ( 1 ∈ ℕ ∧ 6 ∈ ℕ ∧ 1 ≤ 6 ) )
22 15 16 20 21 mpbir3an ⊢ 1 ∈ ( 1 ... 6 )
23 22 ne0ii ⊢ ( 1 ... 6 ) ≠ ∅
24 23 a1i ⊢ ( 𝜑 → ( 1 ... 6 ) ≠ ∅ )
25 7 14 24 mpocurryd ⊢ ( 𝜑 → curry 𝑉 = ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) ) )
26 ovex ⊢ ( ( ( 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
27 eqid ⊢ ( 𝑘 ∈ ( 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 ) ) ) )
28 26 27 fnmpti ⊢ ( 𝑘 ∈ ( 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 ) ) ) ) Fn ( 1 ... 6 )
29 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 6 ) ) → ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
30 29 veronesevald ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 6 ) ) → ( 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 ) ) ) ) )
31 30 fneq1d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) Fn ( 1 ... 6 ) ↔ ( 𝑘 ∈ ( 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 ) ) ) ) Fn ( 1 ... 6 ) ) )
32 28 31 mpbiri ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 6 ) ) → ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) Fn ( 1 ... 6 ) )
33 dffn5 ⊢ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) Fn ( 1 ... 6 ) ↔ ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) = ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
34 32 33 sylib ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 6 ) ) → ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) = ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
35 34 eqcomd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 6 ) ) → ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) = ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) )
36 35 mpteq2dva ⊢ ( 𝜑 → ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) ) = ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ) )
37 25 36 eqtrd ⊢ ( 𝜑 → curry 𝑉 = ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ) )
38 2fveq3 ⊢ ( 𝑢 = 𝑖 → ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) = ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) )
39 38 cbvmptv ⊢ ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ) = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) )
40 37 39 eqtrdi ⊢ ( 𝜑 → curry 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ) )