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	No typesetting found for |- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) with typecode |-
	veronesemat.f	$$⊢\phi \to A:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 3\right)}$$
Assertion	veronesematrowexpd	$$⊢\phi \to curryV=\left(i\in \left(1\dots 6\right)⟼\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{A\left(i\right)\left(1\right)}^2,if\left(k=2,{A\left(i\right)\left(2\right)}^2,if\left(k=3,{A\left(i\right)\left(3\right)}^2,if\left(k=4,A\left(i\right)\left(1\right)A\left(i\right)\left(2\right),if\left(k=5,A\left(i\right)\left(2\right)A\left(i\right)\left(3\right),A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		veronesemat.a	Could not format V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) : No typesetting found for |- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) with typecode |-
2		veronesemat.f	$$⊢\phi \to A:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 3\right)}$$
3	1 2	veronesematrowd	Could not format ( ph -> curry V = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) ) : No typesetting found for |- ( ph -> curry V = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) ) with typecode |-
4		2fveq3	Could not format ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) ) : No typesetting found for |- ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) ) with typecode |-
5	4	cbvmptv	Could not format ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) = ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) : No typesetting found for |- ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) = ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) with typecode |-
6	3 5	eqtrdi	Could not format ( ph -> curry V = ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) ) : No typesetting found for |- ( ph -> curry V = ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) ) with typecode |-
7	2	ffvelcdmda	$$⊢\left(\phi \wedge u\in \left(1\dots 6\right)\right)\to A\left(u\right)\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
8	7	veronesevrowd	Could not format ( ( 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 ) ) ) ) ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) ) ) ) ) with typecode |-
9	8	mpteq2dva	Could not format ( 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 ) ) ) ) ) ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) ) ) ) ) ) with typecode |-
10	6 9	eqtrd	$$⊢\phi \to curryV=\left(u\in \left(1\dots 6\right)⟼\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{A\left(u\right)\left(1\right)}^2,if\left(k=2,{A\left(u\right)\left(2\right)}^2,if\left(k=3,{A\left(u\right)\left(3\right)}^2,if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),A\left(u\right)\left(3\right)A\left(u\right)\left(1\right)\right)\right)\right)\right)\right)\right)\right)$$
11		fveq2	$$⊢u=i\to A\left(u\right)=A\left(i\right)$$
12	11	fveq1d	$$⊢u=i\to A\left(u\right)\left(1\right)=A\left(i\right)\left(1\right)$$
13	12	oveq1d	$$⊢u=i\to {A\left(u\right)\left(1\right)}^2={A\left(i\right)\left(1\right)}^2$$
14	11	fveq1d	$$⊢u=i\to A\left(u\right)\left(2\right)=A\left(i\right)\left(2\right)$$
15	14	oveq1d	$$⊢u=i\to {A\left(u\right)\left(2\right)}^2={A\left(i\right)\left(2\right)}^2$$
16	11	fveq1d	$$⊢u=i\to A\left(u\right)\left(3\right)=A\left(i\right)\left(3\right)$$
17	16	oveq1d	$$⊢u=i\to {A\left(u\right)\left(3\right)}^2={A\left(i\right)\left(3\right)}^2$$
18	12 14	oveq12d	$$⊢u=i\to A\left(u\right)\left(1\right)A\left(u\right)\left(2\right)=A\left(i\right)\left(1\right)A\left(i\right)\left(2\right)$$
19	14 16	oveq12d	$$⊢u=i\to A\left(u\right)\left(2\right)A\left(u\right)\left(3\right)=A\left(i\right)\left(2\right)A\left(i\right)\left(3\right)$$
20	16 12	oveq12d	$$⊢u=i\to A\left(u\right)\left(3\right)A\left(u\right)\left(1\right)=A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)$$
21	19 20	ifeq12d	$$⊢u=i\to if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),A\left(u\right)\left(3\right)A\left(u\right)\left(1\right)\right)=if\left(k=5,A\left(i\right)\left(2\right)A\left(i\right)\left(3\right),A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)\right)$$
22	18 21	ifeq12d	$$⊢u=i\to if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),A\left(u\right)\left(3\right)A\left(u\right)\left(1\right)\right)\right)=if\left(k=4,A\left(i\right)\left(1\right)A\left(i\right)\left(2\right),if\left(k=5,A\left(i\right)\left(2\right)A\left(i\right)\left(3\right),A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)\right)\right)$$
23	17 22	ifeq12d	$$⊢u=i\to if\left(k=3,{A\left(u\right)\left(3\right)}^2,if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),A\left(u\right)\left(3\right)A\left(u\right)\left(1\right)\right)\right)\right)=if\left(k=3,{A\left(i\right)\left(3\right)}^2,if\left(k=4,A\left(i\right)\left(1\right)A\left(i\right)\left(2\right),if\left(k=5,A\left(i\right)\left(2\right)A\left(i\right)\left(3\right),A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)\right)\right)\right)$$
24	15 23	ifeq12d	$$⊢u=i\to if\left(k=2,{A\left(u\right)\left(2\right)}^2,if\left(k=3,{A\left(u\right)\left(3\right)}^2,if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),A\left(u\right)\left(3\right)A\left(u\right)\left(1\right)\right)\right)\right)\right)=if\left(k=2,{A\left(i\right)\left(2\right)}^2,if\left(k=3,{A\left(i\right)\left(3\right)}^2,if\left(k=4,A\left(i\right)\left(1\right)A\left(i\right)\left(2\right),if\left(k=5,A\left(i\right)\left(2\right)A\left(i\right)\left(3\right),A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)\right)\right)\right)\right)$$
25	13 24	ifeq12d	$$⊢u=i\to if\left(k=1,{A\left(u\right)\left(1\right)}^2,if\left(k=2,{A\left(u\right)\left(2\right)}^2,if\left(k=3,{A\left(u\right)\left(3\right)}^2,if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),A\left(u\right)\left(3\right)A\left(u\right)\left(1\right)\right)\right)\right)\right)\right)=if\left(k=1,{A\left(i\right)\left(1\right)}^2,if\left(k=2,{A\left(i\right)\left(2\right)}^2,if\left(k=3,{A\left(i\right)\left(3\right)}^2,if\left(k=4,A\left(i\right)\left(1\right)A\left(i\right)\left(2\right),if\left(k=5,A\left(i\right)\left(2\right)A\left(i\right)\left(3\right),A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)\right)\right)\right)\right)\right)$$
26	25	mpteq2dv	$$⊢u=i\to \left(k\in \left(1\dots 6\right)⟼if\left(k=1,{A\left(u\right)\left(1\right)}^2,if\left(k=2,{A\left(u\right)\left(2\right)}^2,if\left(k=3,{A\left(u\right)\left(3\right)}^2,if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),A\left(u\right)\left(3\right)A\left(u\right)\left(1\right)\right)\right)\right)\right)\right)\right)=\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{A\left(i\right)\left(1\right)}^2,if\left(k=2,{A\left(i\right)\left(2\right)}^2,if\left(k=3,{A\left(i\right)\left(3\right)}^2,if\left(k=4,A\left(i\right)\left(1\right)A\left(i\right)\left(2\right),if\left(k=5,A\left(i\right)\left(2\right)A\left(i\right)\left(3\right),A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)\right)\right)\right)\right)\right)\right)$$
27	26	cbvmptv	$$⊢\left(u\in \left(1\dots 6\right)⟼\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{A\left(u\right)\left(1\right)}^2,if\left(k=2,{A\left(u\right)\left(2\right)}^2,if\left(k=3,{A\left(u\right)\left(3\right)}^2,if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),A\left(u\right)\left(3\right)A\left(u\right)\left(1\right)\right)\right)\right)\right)\right)\right)\right)=\left(i\in \left(1\dots 6\right)⟼\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{A\left(i\right)\left(1\right)}^2,if\left(k=2,{A\left(i\right)\left(2\right)}^2,if\left(k=3,{A\left(i\right)\left(3\right)}^2,if\left(k=4,A\left(i\right)\left(1\right)A\left(i\right)\left(2\right),if\left(k=5,A\left(i\right)\left(2\right)A\left(i\right)\left(3\right),A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)\right)\right)\right)\right)\right)\right)\right)$$
28	10 27	eqtrdi	$$⊢\phi \to curryV=\left(i\in \left(1\dots 6\right)⟼\left(k\in \left(1\dots 6\right)⟼if\left(k=1,{A\left(i\right)\left(1\right)}^2,if\left(k=2,{A\left(i\right)\left(2\right)}^2,if\left(k=3,{A\left(i\right)\left(3\right)}^2,if\left(k=4,A\left(i\right)\left(1\right)A\left(i\right)\left(2\right),if\left(k=5,A\left(i\right)\left(2\right)A\left(i\right)\left(3\right),A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)\right)\right)\right)\right)\right)\right)\right)$$