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	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	veronesematrowd	Could not format assertion : No typesetting found for |- ( ph -> curry V = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) ) with typecode |-

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		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 |-
4	3	fveq1d	Could not format ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) ) : No typesetting found for |- ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) ) with typecode |-
5		fveq2	Could not format ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) ) : No typesetting found for |- ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) ) with typecode |-
6	4 5	cbvmpov	Could not format ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) : No typesetting found for |- ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) with typecode |-
7	1 6	eqtri	Could not format V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) : No typesetting found for |- V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) with typecode |-
8	2	adantr	$$⊢\left(\phi \wedge \left(u\in \left(1\dots 6\right)\wedge v\in \left(1\dots 6\right)\right)\right)\to A:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 3\right)}$$
9		simprl	$$⊢\left(\phi \wedge \left(u\in \left(1\dots 6\right)\wedge v\in \left(1\dots 6\right)\right)\right)\to u\in \left(1\dots 6\right)$$
10	8 9	ffvelcdmd	$$⊢\left(\phi \wedge \left(u\in \left(1\dots 6\right)\wedge v\in \left(1\dots 6\right)\right)\right)\to A\left(u\right)\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
11		simprr	$$⊢\left(\phi \wedge \left(u\in \left(1\dots 6\right)\wedge v\in \left(1\dots 6\right)\right)\right)\to v\in \left(1\dots 6\right)$$
12		veronesefvcl	Could not format ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) : No typesetting found for |- ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) with typecode |-
13	10 11 12	syl2anc	Could not format ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) : No typesetting found for |- ( ( ph /\ ( u e. ( 1 ... 6 ) /\ v e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) with typecode |-
14	13	ralrimivva	Could not format ( ph -> A. u e. ( 1 ... 6 ) A. v e. ( 1 ... 6 ) ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) : No typesetting found for |- ( ph -> A. u e. ( 1 ... 6 ) A. v e. ( 1 ... 6 ) ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) with typecode |-
15		1nn	$$⊢1\in \mathbb{N}$$
16		6nn	$$⊢6\in \mathbb{N}$$
17		1re	$$⊢1\in ℝ$$
18		6re	$$⊢6\in ℝ$$
19		1lt6	$$⊢1<6$$
20	17 18 19	ltleii	$$⊢1\le 6$$
21		elfz1b	$$⊢1\in \left(1\dots 6\right)\leftrightarrow \left(1\in \mathbb{N}\wedge 6\in \mathbb{N}\wedge 1\le 6\right)$$
22	15 16 20 21	mpbir3an	$$⊢1\in \left(1\dots 6\right)$$
23	22	ne0ii	$$⊢\left(1\dots 6\right)\ne \varnothing$$
24	23	a1i	$$⊢\phi \to \left(1\dots 6\right)\ne \varnothing$$
25	7 14 24	mpocurryd	Could not format ( ph -> curry V = ( u e. ( 1 ... 6 ) |-> ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) ) : No typesetting found for |- ( ph -> curry V = ( u e. ( 1 ... 6 ) |-> ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) ) with typecode |-
26		ovex	$$⊢\left(if\left(k=1,{A\left(u\right)\left(1\right)}^2,0\right)+if\left(k=2,{A\left(u\right)\left(2\right)}^2,0\right)\right)+if\left(k=3,{A\left(u\right)\left(3\right)}^2,0\right)+\left(if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),0\right)+if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),0\right)\right)+if\left(k=6,A\left(u\right)\left(3\right)A\left(u\right)\left(1\right),0\right)\in \mathrm{V}$$
27		eqid	$$⊢\left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{A\left(u\right)\left(1\right)}^2,0\right)+if\left(k=2,{A\left(u\right)\left(2\right)}^2,0\right)\right)+if\left(k=3,{A\left(u\right)\left(3\right)}^2,0\right)+\left(if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),0\right)+if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),0\right)\right)+if\left(k=6,A\left(u\right)\left(3\right)A\left(u\right)\left(1\right),0\right)\right)=\left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{A\left(u\right)\left(1\right)}^2,0\right)+if\left(k=2,{A\left(u\right)\left(2\right)}^2,0\right)\right)+if\left(k=3,{A\left(u\right)\left(3\right)}^2,0\right)+\left(if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),0\right)+if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),0\right)\right)+if\left(k=6,A\left(u\right)\left(3\right)A\left(u\right)\left(1\right),0\right)\right)$$
28	26 27	fnmpti	$$⊢\left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{A\left(u\right)\left(1\right)}^2,0\right)+if\left(k=2,{A\left(u\right)\left(2\right)}^2,0\right)\right)+if\left(k=3,{A\left(u\right)\left(3\right)}^2,0\right)+\left(if\left(k=4,A\left(u\right)\left(1\right)A\left(u\right)\left(2\right),0\right)+if\left(k=5,A\left(u\right)\left(2\right)A\left(u\right)\left(3\right),0\right)\right)+if\left(k=6,A\left(u\right)\left(3\right)A\left(u\right)\left(1\right),0\right)\right)Fn\left(1\dots 6\right)$$
29	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)$$
30	29	veronesevald	Could not format ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) with typecode |-
31	30	fneq1d	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
32	28 31	mpbiri	Could not format ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( veronese ` ( A ` u ) ) Fn ( 1 ... 6 ) ) : No typesetting found for |- ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( veronese ` ( A ` u ) ) Fn ( 1 ... 6 ) ) with typecode |-
33		dffn5	Could not format ( ( veronese ` ( A ` u ) ) Fn ( 1 ... 6 ) <-> ( veronese ` ( A ` u ) ) = ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) : No typesetting found for |- ( ( veronese ` ( A ` u ) ) Fn ( 1 ... 6 ) <-> ( veronese ` ( A ` u ) ) = ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) with typecode |-
34	32 33	sylib	Could not format ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( veronese ` ( A ` u ) ) = ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) : No typesetting found for |- ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( veronese ` ( A ` u ) ) = ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) with typecode |-
35	34	eqcomd	Could not format ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) = ( veronese ` ( A ` u ) ) ) : No typesetting found for |- ( ( ph /\ u e. ( 1 ... 6 ) ) -> ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) = ( veronese ` ( A ` u ) ) ) with typecode |-
36	35	mpteq2dva	Could not format ( ph -> ( u e. ( 1 ... 6 ) |-> ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) = ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) ) : No typesetting found for |- ( ph -> ( u e. ( 1 ... 6 ) |-> ( v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) = ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) ) with typecode |-
37	25 36	eqtrd	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 |-
38		2fveq3	Could not format ( u = i -> ( veronese ` ( A ` u ) ) = ( veronese ` ( A ` i ) ) ) : No typesetting found for |- ( u = i -> ( veronese ` ( A ` u ) ) = ( veronese ` ( A ` i ) ) ) with typecode |-
39	38	cbvmptv	Could not format ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) : No typesetting found for |- ( u e. ( 1 ... 6 ) |-> ( veronese ` ( A ` u ) ) ) = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) with typecode |-
40	37 39	eqtrdi	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 |-