Theorem veronesev5lem

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