Theorem veronesev2lem

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

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