Theorem veronesev4lem

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