Theorem veronesev1lem

Description: Lemma for veronesevrowd . Value of the first coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 15-Aug-2026)

	Ref	Expression
Hypothesis	veronesevrow.1	$$⊢\phi \to P\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	veronesev1lem	Could not format assertion : No typesetting found for |- ( ph -> ( ( veronese ` P ) ` 1 ) = ( ( P ` 1 ) ^ 2 ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		veronesevrow.1	$$⊢\phi \to P\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2	1	veronesevald	Could not format ( ph -> ( veronese ` P ) = ( x e. ( 1 ... 6 ) |-> ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) ) : No typesetting found for |- ( ph -> ( veronese ` P ) = ( x e. ( 1 ... 6 ) |-> ( ( ( if ( x = 1 , ( ( P ` 1 ) ^ 2 ) , 0 ) + if ( x = 2 , ( ( P ` 2 ) ^ 2 ) , 0 ) ) + if ( x = 3 , ( ( P ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( x = 4 , ( ( P ` 1 ) x. ( P ` 2 ) ) , 0 ) + if ( x = 5 , ( ( P ` 2 ) x. ( P ` 3 ) ) , 0 ) ) + if ( x = 6 , ( ( P ` 3 ) x. ( P ` 1 ) ) , 0 ) ) ) ) ) with typecode |-
3		iftrue	$$⊢x=1\to if\left(x=1,{P\left(1\right)}^2,0\right)={P\left(1\right)}^2$$
4	3	oveq1d	$$⊢x=1\to if\left(x=1,{P\left(1\right)}^2,0\right)+if\left(x=2,{P\left(2\right)}^2,0\right)={P\left(1\right)}^2+if\left(x=2,{P\left(2\right)}^2,0\right)$$
5	4	oveq1d	$$⊢x=1\to if\left(x=1,{P\left(1\right)}^2,0\right)+if\left(x=2,{P\left(2\right)}^2,0\right)+if\left(x=3,{P\left(3\right)}^2,0\right)={P\left(1\right)}^2+if\left(x=2,{P\left(2\right)}^2,0\right)+if\left(x=3,{P\left(3\right)}^2,0\right)$$
6	5	oveq1d	$$⊢x=1\to \left(if\left(x=1,{P\left(1\right)}^2,0\right)+if\left(x=2,{P\left(2\right)}^2,0\right)\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=\left({P\left(1\right)}^2+if\left(x=2,{P\left(2\right)}^2,0\right)\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)$$
7		1ne2	$$⊢1\ne 2$$
8		neeq1	$$⊢x=1\to \left(x\ne 2\leftrightarrow 1\ne 2\right)$$
9	7 8	mpbiri	$$⊢x=1\to x\ne 2$$
10	9	neneqd	$$⊢x=1\to \neg x=2$$
11	10	iffalsed	$$⊢x=1\to if\left(x=2,{P\left(2\right)}^2,0\right)=0$$
12	11	oveq2d	$$⊢x=1\to {P\left(1\right)}^2+if\left(x=2,{P\left(2\right)}^2,0\right)={P\left(1\right)}^2+0$$
13	12	oveq1d	$$⊢x=1\to {P\left(1\right)}^2+if\left(x=2,{P\left(2\right)}^2,0\right)+if\left(x=3,{P\left(3\right)}^2,0\right)={P\left(1\right)}^2+0+if\left(x=3,{P\left(3\right)}^2,0\right)$$
14	13	oveq1d	$$⊢x=1\to \left({P\left(1\right)}^2+if\left(x=2,{P\left(2\right)}^2,0\right)\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=\left({P\left(1\right)}^2+0\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)$$
15	6 14	eqtrd	$$⊢x=1\to \left(if\left(x=1,{P\left(1\right)}^2,0\right)+if\left(x=2,{P\left(2\right)}^2,0\right)\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=\left({P\left(1\right)}^2+0\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)$$
16		1ne3	$$⊢1\ne 3$$
17		neeq1	$$⊢x=1\to \left(x\ne 3\leftrightarrow 1\ne 3\right)$$
18	16 17	mpbiri	$$⊢x=1\to x\ne 3$$
19	18	neneqd	$$⊢x=1\to \neg x=3$$
20	19	iffalsed	$$⊢x=1\to if\left(x=3,{P\left(3\right)}^2,0\right)=0$$
21	20	oveq2d	$$⊢x=1\to {P\left(1\right)}^2+0+if\left(x=3,{P\left(3\right)}^2,0\right)={P\left(1\right)}^2+0+0$$
22	21	oveq1d	$$⊢x=1\to \left({P\left(1\right)}^2+0\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=\left({P\left(1\right)}^2+0\right)+0+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)$$
23		1re	$$⊢1\in ℝ$$
24		1lt4	$$⊢1<4$$
25	23 24	ltneii	$$⊢1\ne 4$$
26		neeq1	$$⊢x=1\to \left(x\ne 4\leftrightarrow 1\ne 4\right)$$
27	25 26	mpbiri	$$⊢x=1\to x\ne 4$$
28	27	neneqd	$$⊢x=1\to \neg x=4$$
29	28	iffalsed	$$⊢x=1\to if\left(x=4,P\left(1\right)P\left(2\right),0\right)=0$$
30	29	oveq1d	$$⊢x=1\to if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)=0+if\left(x=5,P\left(2\right)P\left(3\right),0\right)$$
31	30	oveq1d	$$⊢x=1\to if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=0+if\left(x=5,P\left(2\right)P\left(3\right),0\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)$$
32	31	oveq2d	$$⊢x=1\to \left({P\left(1\right)}^2+0\right)+0+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=\left({P\left(1\right)}^2+0\right)+0+\left(0+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)$$
33	15 22 32	3eqtrd	$$⊢x=1\to \left(if\left(x=1,{P\left(1\right)}^2,0\right)+if\left(x=2,{P\left(2\right)}^2,0\right)\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=\left({P\left(1\right)}^2+0\right)+0+\left(0+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)$$
34		1lt5	$$⊢1<5$$
35	23 34	ltneii	$$⊢1\ne 5$$
36		neeq1	$$⊢x=1\to \left(x\ne 5\leftrightarrow 1\ne 5\right)$$
37	35 36	mpbiri	$$⊢x=1\to x\ne 5$$
38	37	neneqd	$$⊢x=1\to \neg x=5$$
39	38	iffalsed	$$⊢x=1\to if\left(x=5,P\left(2\right)P\left(3\right),0\right)=0$$
40	39	oveq2d	$$⊢x=1\to 0+if\left(x=5,P\left(2\right)P\left(3\right),0\right)=0+0$$
41	40	oveq1d	$$⊢x=1\to 0+if\left(x=5,P\left(2\right)P\left(3\right),0\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=0+0+if\left(x=6,P\left(3\right)P\left(1\right),0\right)$$
42	41	oveq2d	$$⊢x=1\to \left({P\left(1\right)}^2+0\right)+0+\left(0+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=\left({P\left(1\right)}^2+0\right)+0+\left(0+0\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)$$
43		1lt6	$$⊢1<6$$
44	23 43	ltneii	$$⊢1\ne 6$$
45		neeq1	$$⊢x=1\to \left(x\ne 6\leftrightarrow 1\ne 6\right)$$
46	44 45	mpbiri	$$⊢x=1\to x\ne 6$$
47	46	neneqd	$$⊢x=1\to \neg x=6$$
48	47	iffalsed	$$⊢x=1\to if\left(x=6,P\left(3\right)P\left(1\right),0\right)=0$$
49	48	oveq2d	$$⊢x=1\to 0+0+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=0+0+0$$
50	49	oveq2d	$$⊢x=1\to \left({P\left(1\right)}^2+0\right)+0+\left(0+0\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=\left({P\left(1\right)}^2+0\right)+0+\left(0+0\right)+0$$
51	33 42 50	3eqtrd	$$⊢x=1\to \left(if\left(x=1,{P\left(1\right)}^2,0\right)+if\left(x=2,{P\left(2\right)}^2,0\right)\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=\left({P\left(1\right)}^2+0\right)+0+\left(0+0\right)+0$$
52	51	adantl	$$⊢\left(\phi \wedge x=1\right)\to \left(if\left(x=1,{P\left(1\right)}^2,0\right)+if\left(x=2,{P\left(2\right)}^2,0\right)\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)=\left({P\left(1\right)}^2+0\right)+0+\left(0+0\right)+0$$
53	1	rr3fv1cld	$$⊢\phi \to P\left(1\right)\in ℝ$$
54	53	adantr	$$⊢\left(\phi \wedge x=1\right)\to P\left(1\right)\in ℝ$$
55	54	resqcld	$$⊢\left(\phi \wedge x=1\right)\to {P\left(1\right)}^2\in ℝ$$
56		0red	$$⊢\left(\phi \wedge x=1\right)\to 0\in ℝ$$
57	55 56	readdcld	$$⊢\left(\phi \wedge x=1\right)\to {P\left(1\right)}^2+0\in ℝ$$
58	57	recnd	$$⊢\left(\phi \wedge x=1\right)\to {P\left(1\right)}^2+0\in ℂ$$
59	58	addridd	$$⊢\left(\phi \wedge x=1\right)\to {P\left(1\right)}^2+0+0={P\left(1\right)}^2+0$$
60	59	oveq1d	$$⊢\left(\phi \wedge x=1\right)\to \left({P\left(1\right)}^2+0\right)+0+\left(0+0\right)+0={P\left(1\right)}^2+0+\left(0+0\right)+0$$
61	55	recnd	$$⊢\left(\phi \wedge x=1\right)\to {P\left(1\right)}^2\in ℂ$$
62	61	addridd	$$⊢\left(\phi \wedge x=1\right)\to {P\left(1\right)}^2+0={P\left(1\right)}^2$$
63	62	oveq1d	$$⊢\left(\phi \wedge x=1\right)\to {P\left(1\right)}^2+0+\left(0+0\right)+0={P\left(1\right)}^2+\left(0+0\right)+0$$
64	60 63	eqtrd	$$⊢\left(\phi \wedge x=1\right)\to \left({P\left(1\right)}^2+0\right)+0+\left(0+0\right)+0={P\left(1\right)}^2+\left(0+0\right)+0$$
65	56 56	readdcld	$$⊢\left(\phi \wedge x=1\right)\to 0+0\in ℝ$$
66	65	recnd	$$⊢\left(\phi \wedge x=1\right)\to 0+0\in ℂ$$
67	66	addridd	$$⊢\left(\phi \wedge x=1\right)\to 0+0+0=0+0$$
68	67	oveq2d	$$⊢\left(\phi \wedge x=1\right)\to {P\left(1\right)}^2+\left(0+0\right)+0={P\left(1\right)}^2+0+0$$
69		00id	$$⊢0+0=0$$
70	69	a1i	$$⊢\left(\phi \wedge x=1\right)\to 0+0=0$$
71	70	oveq2d	$$⊢\left(\phi \wedge x=1\right)\to {P\left(1\right)}^2+0+0={P\left(1\right)}^2+0$$
72	64 68 71	3eqtrd	$$⊢\left(\phi \wedge x=1\right)\to \left({P\left(1\right)}^2+0\right)+0+\left(0+0\right)+0={P\left(1\right)}^2+0$$
73	52 72 62	3eqtrd	$$⊢\left(\phi \wedge x=1\right)\to \left(if\left(x=1,{P\left(1\right)}^2,0\right)+if\left(x=2,{P\left(2\right)}^2,0\right)\right)+if\left(x=3,{P\left(3\right)}^2,0\right)+\left(if\left(x=4,P\left(1\right)P\left(2\right),0\right)+if\left(x=5,P\left(2\right)P\left(3\right),0\right)\right)+if\left(x=6,P\left(3\right)P\left(1\right),0\right)={P\left(1\right)}^2$$
74		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
75		6nn	$$⊢6\in \mathbb{N}$$
76	75	nnzi	$$⊢6\in \mathbb{Z}$$
77	76	a1i	$$⊢\phi \to 6\in \mathbb{Z}$$
78		1le1	$$⊢1\le 1$$
79	78	a1i	$$⊢\phi \to 1\le 1$$
80		6re	$$⊢6\in ℝ$$
81	23 80 43	ltleii	$$⊢1\le 6$$
82	81	a1i	$$⊢\phi \to 1\le 6$$
83	74 77 74 79 82	elfzd	$$⊢\phi \to 1\in \left(1\dots 6\right)$$
84	53	resqcld	$$⊢\phi \to {P\left(1\right)}^2\in ℝ$$
85	2 73 83 84	fvmptd	Could not format ( ph -> ( ( veronese ` P ) ` 1 ) = ( ( P ` 1 ) ^ 2 ) ) : No typesetting found for |- ( ph -> ( ( veronese ` P ) ` 1 ) = ( ( P ` 1 ) ^ 2 ) ) with typecode |-