Theorem veronesev3lem

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

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