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

Proof

Step Hyp Ref Expression
1 veronesemat.a ⊢ 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) )
2 veronesemat.f ⊢ ( 𝜑 → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
3 1 2 veronesematrowd ⊢ ( 𝜑 → curry 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ) )
4 2fveq3 ⊢ ( 𝑖 = 𝑢 → ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) = ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) )
5 4 cbvmptv ⊢ ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ) = ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) )
6 3 5 eqtrdi ⊢ ( 𝜑 → curry 𝑉 = ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ) )
7 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 6 ) ) → ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
8 7 veronesevrowd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 6 ) ) → ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) = ( 𝑘 ∈ ( 1 ... 6 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ↑ 2 ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) ) ) ) ) ) ) )
9 8 mpteq2dva ⊢ ( 𝜑 → ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ) = ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( 𝑘 ∈ ( 1 ... 6 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ↑ 2 ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) ) ) ) ) ) ) ) )
10 6 9 eqtrd ⊢ ( 𝜑 → curry 𝑉 = ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( 𝑘 ∈ ( 1 ... 6 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ↑ 2 ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) ) ) ) ) ) ) ) )
11 fveq2 ⊢ ( 𝑢 = 𝑖 → ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑖 ) )
12 11 fveq1d ⊢ ( 𝑢 = 𝑖 → ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) = ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) )
13 12 oveq1d ⊢ ( 𝑢 = 𝑖 → ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ↑ 2 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) )
14 11 fveq1d ⊢ ( 𝑢 = 𝑖 → ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) = ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) )
15 14 oveq1d ⊢ ( 𝑢 = 𝑖 → ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ↑ 2 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) )
16 11 fveq1d ⊢ ( 𝑢 = 𝑖 → ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) = ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) )
17 16 oveq1d ⊢ ( 𝑢 = 𝑖 → ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ↑ 2 ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) )
18 12 14 oveq12d ⊢ ( 𝑢 = 𝑖 → ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) )
19 14 16 oveq12d ⊢ ( 𝑢 = 𝑖 → ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) )
20 16 12 oveq12d ⊢ ( 𝑢 = 𝑖 → ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) = ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) )
21 19 20 ifeq12d ⊢ ( 𝑢 = 𝑖 → if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) ) = if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) )
22 18 21 ifeq12d ⊢ ( 𝑢 = 𝑖 → if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) ) ) = if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) )
23 17 22 ifeq12d ⊢ ( 𝑢 = 𝑖 → if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) ) ) ) = if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) )
24 15 23 ifeq12d ⊢ ( 𝑢 = 𝑖 → if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) ) ) ) ) = if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) ) )
25 13 24 ifeq12d ⊢ ( 𝑢 = 𝑖 → if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ↑ 2 ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) ) ) ) ) ) = if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) ) ) )
26 25 mpteq2dv ⊢ ( 𝑢 = 𝑖 → ( 𝑘 ∈ ( 1 ... 6 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ↑ 2 ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) ) ) ) ) ) ) = ( 𝑘 ∈ ( 1 ... 6 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) ) ) ) )
27 26 cbvmptv ⊢ ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( 𝑘 ∈ ( 1 ... 6 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ↑ 2 ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑢 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑢 ) ‘ 1 ) ) ) ) ) ) ) ) ) = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( 𝑘 ∈ ( 1 ... 6 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) ) ) ) )
28 10 27 eqtrdi ⊢ ( 𝜑 → curry 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( 𝑘 ∈ ( 1 ... 6 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) , if ( 𝑘 = 3 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) , if ( 𝑘 = 4 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) , if ( 𝑘 = 5 , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) , ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) ) ) ) ) )