Theorem veronesevald

Description: Value of the Veronese map at a point, expressed as a maps-to function on the six coordinates. (Contributed by Jiamin Zhao, 14-Aug-2026)

	Ref	Expression
Hypothesis	veroneseval.1	$$⊢\phi \to P\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	veronesevald	Could not format assertion : No typesetting found for |- ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		veroneseval.1	$$⊢\phi \to P\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		fveq1	$$⊢q=P\to q\left(1\right)=P\left(1\right)$$
3	2	oveq1d	$$⊢q=P\to {q\left(1\right)}^2={P\left(1\right)}^2$$
4	3	ifeq1d	$$⊢q=P\to if\left(k=1,{q\left(1\right)}^2,0\right)=if\left(k=1,{P\left(1\right)}^2,0\right)$$
5		fveq1	$$⊢q=P\to q\left(2\right)=P\left(2\right)$$
6	5	oveq1d	$$⊢q=P\to {q\left(2\right)}^2={P\left(2\right)}^2$$
7	6	ifeq1d	$$⊢q=P\to if\left(k=2,{q\left(2\right)}^2,0\right)=if\left(k=2,{P\left(2\right)}^2,0\right)$$
8	4 7	oveq12d	$$⊢q=P\to if\left(k=1,{q\left(1\right)}^2,0\right)+if\left(k=2,{q\left(2\right)}^2,0\right)=if\left(k=1,{P\left(1\right)}^2,0\right)+if\left(k=2,{P\left(2\right)}^2,0\right)$$
9		fveq1	$$⊢q=P\to q\left(3\right)=P\left(3\right)$$
10	9	oveq1d	$$⊢q=P\to {q\left(3\right)}^2={P\left(3\right)}^2$$
11	10	ifeq1d	$$⊢q=P\to if\left(k=3,{q\left(3\right)}^2,0\right)=if\left(k=3,{P\left(3\right)}^2,0\right)$$
12	8 11	oveq12d	$$⊢q=P\to if\left(k=1,{q\left(1\right)}^2,0\right)+if\left(k=2,{q\left(2\right)}^2,0\right)+if\left(k=3,{q\left(3\right)}^2,0\right)=if\left(k=1,{P\left(1\right)}^2,0\right)+if\left(k=2,{P\left(2\right)}^2,0\right)+if\left(k=3,{P\left(3\right)}^2,0\right)$$
13	2 5	oveq12d	$$⊢q=P\to q\left(1\right)q\left(2\right)=P\left(1\right)P\left(2\right)$$
14	13	ifeq1d	$$⊢q=P\to if\left(k=4,q\left(1\right)q\left(2\right),0\right)=if\left(k=4,P\left(1\right)P\left(2\right),0\right)$$
15	5 9	oveq12d	$$⊢q=P\to q\left(2\right)q\left(3\right)=P\left(2\right)P\left(3\right)$$
16	15	ifeq1d	$$⊢q=P\to if\left(k=5,q\left(2\right)q\left(3\right),0\right)=if\left(k=5,P\left(2\right)P\left(3\right),0\right)$$
17	14 16	oveq12d	$$⊢q=P\to if\left(k=4,q\left(1\right)q\left(2\right),0\right)+if\left(k=5,q\left(2\right)q\left(3\right),0\right)=if\left(k=4,P\left(1\right)P\left(2\right),0\right)+if\left(k=5,P\left(2\right)P\left(3\right),0\right)$$
18	9 2	oveq12d	$$⊢q=P\to q\left(3\right)q\left(1\right)=P\left(3\right)P\left(1\right)$$
19	18	ifeq1d	$$⊢q=P\to if\left(k=6,q\left(3\right)q\left(1\right),0\right)=if\left(k=6,P\left(3\right)P\left(1\right),0\right)$$
20	17 19	oveq12d	$$⊢q=P\to if\left(k=4,q\left(1\right)q\left(2\right),0\right)+if\left(k=5,q\left(2\right)q\left(3\right),0\right)+if\left(k=6,q\left(3\right)q\left(1\right),0\right)=if\left(k=4,P\left(1\right)P\left(2\right),0\right)+if\left(k=5,P\left(2\right)P\left(3\right),0\right)+if\left(k=6,P\left(3\right)P\left(1\right),0\right)$$
21	12 20	oveq12d	$$⊢q=P\to \left(if\left(k=1,{q\left(1\right)}^2,0\right)+if\left(k=2,{q\left(2\right)}^2,0\right)\right)+if\left(k=3,{q\left(3\right)}^2,0\right)+\left(if\left(k=4,q\left(1\right)q\left(2\right),0\right)+if\left(k=5,q\left(2\right)q\left(3\right),0\right)\right)+if\left(k=6,q\left(3\right)q\left(1\right),0\right)=\left(if\left(k=1,{P\left(1\right)}^2,0\right)+if\left(k=2,{P\left(2\right)}^2,0\right)\right)+if\left(k=3,{P\left(3\right)}^2,0\right)+\left(if\left(k=4,P\left(1\right)P\left(2\right),0\right)+if\left(k=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(k=6,P\left(3\right)P\left(1\right),0\right)$$
22	21	mpteq2dv	$$⊢q=P\to \left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{q\left(1\right)}^2,0\right)+if\left(k=2,{q\left(2\right)}^2,0\right)\right)+if\left(k=3,{q\left(3\right)}^2,0\right)+\left(if\left(k=4,q\left(1\right)q\left(2\right),0\right)+if\left(k=5,q\left(2\right)q\left(3\right),0\right)\right)+if\left(k=6,q\left(3\right)q\left(1\right),0\right)\right)=\left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{P\left(1\right)}^2,0\right)+if\left(k=2,{P\left(2\right)}^2,0\right)\right)+if\left(k=3,{P\left(3\right)}^2,0\right)+\left(if\left(k=4,P\left(1\right)P\left(2\right),0\right)+if\left(k=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(k=6,P\left(3\right)P\left(1\right),0\right)\right)$$
23		df-veronese	Could not format veronese = ( q e. ( RR ^m ( 1 ... 3 ) ) |-> ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( q ` 1 ) x. ( q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( q ` 2 ) x. ( q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( q ` 3 ) x. ( q ` 1 ) ) , 0 ) ) ) ) ) : No typesetting found for |- veronese = ( q e. ( RR ^m ( 1 ... 3 ) ) |-> ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( q ` 1 ) x. ( q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( q ` 2 ) x. ( q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( q ` 3 ) x. ( q ` 1 ) ) , 0 ) ) ) ) ) with typecode |-
24		ovex	$$⊢\left(1\dots 6\right)\in \mathrm{V}$$
25	24	mptex	$$⊢\left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{q\left(1\right)}^2,0\right)+if\left(k=2,{q\left(2\right)}^2,0\right)\right)+if\left(k=3,{q\left(3\right)}^2,0\right)+\left(if\left(k=4,q\left(1\right)q\left(2\right),0\right)+if\left(k=5,q\left(2\right)q\left(3\right),0\right)\right)+if\left(k=6,q\left(3\right)q\left(1\right),0\right)\right)\in \mathrm{V}$$
26	22 23 25	fvmpt3i	Could not format ( P e. ( RR ^m ( 1 ... 3 ) ) -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) ) : No typesetting found for |- ( P e. ( RR ^m ( 1 ... 3 ) ) -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) ) with typecode |-
27	1 26	syl	Could not format ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) ) : No typesetting found for |- ( ph -> ( veronese ` P ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( k = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) ) with typecode |-