Theorem veronesev6lem

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