Theorem veronesefvcl

Description: Every coordinate of the Veronese map of a real 3-vector is real. (Contributed by Jiamin Zhao, 19-Aug-2026)

	Ref	Expression
Assertion	veronesefvcl	Could not format assertion : No typesetting found for |- ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( veronese ` Q ) ` K ) e. RR ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2	1	veronesevald	Could not format ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( veronese ` Q ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) ) ) ) ) : No typesetting found for |- ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( veronese ` Q ) = ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) ) ) ) ) with typecode |-
3	2	fveq1d	Could not format ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( veronese ` Q ) ` K ) = ( ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) ) ) ) ` K ) ) : No typesetting found for |- ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( veronese ` Q ) ` K ) = ( ( k e. ( 1 ... 6 ) |-> ( ( ( if ( k = 1 , ( ( Q ` 1 ) ^ 2 ) , 0 ) + if ( k = 2 , ( ( Q ` 2 ) ^ 2 ) , 0 ) ) + if ( k = 3 , ( ( Q ` 3 ) ^ 2 ) , 0 ) ) + ( ( if ( k = 4 , ( ( Q ` 1 ) x. ( Q ` 2 ) ) , 0 ) + if ( k = 5 , ( ( Q ` 2 ) x. ( Q ` 3 ) ) , 0 ) ) + if ( k = 6 , ( ( Q ` 3 ) x. ( Q ` 1 ) ) , 0 ) ) ) ) ` K ) ) with typecode |-
4	1	rr3fv1cld	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to Q\left(1\right)\in ℝ$$
5	4	resqcld	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to {Q\left(1\right)}^2\in ℝ$$
6	5	adantr	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to {Q\left(1\right)}^2\in ℝ$$
7		0red	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to 0\in ℝ$$
8	6 7	ifcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to if\left(k=1,{Q\left(1\right)}^2,0\right)\in ℝ$$
9	1	rr3fv2cld	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to Q\left(2\right)\in ℝ$$
10	9	resqcld	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to {Q\left(2\right)}^2\in ℝ$$
11	10	adantr	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to {Q\left(2\right)}^2\in ℝ$$
12	11 7	ifcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to if\left(k=2,{Q\left(2\right)}^2,0\right)\in ℝ$$
13	8 12	readdcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to if\left(k=1,{Q\left(1\right)}^2,0\right)+if\left(k=2,{Q\left(2\right)}^2,0\right)\in ℝ$$
14	1	rr3fv3cld	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to Q\left(3\right)\in ℝ$$
15	14	resqcld	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to {Q\left(3\right)}^2\in ℝ$$
16	15	adantr	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to {Q\left(3\right)}^2\in ℝ$$
17	16 7	ifcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to if\left(k=3,{Q\left(3\right)}^2,0\right)\in ℝ$$
18	13 17	readdcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to if\left(k=1,{Q\left(1\right)}^2,0\right)+if\left(k=2,{Q\left(2\right)}^2,0\right)+if\left(k=3,{Q\left(3\right)}^2,0\right)\in ℝ$$
19	4 9	remulcld	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to Q\left(1\right)Q\left(2\right)\in ℝ$$
20	19	adantr	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to Q\left(1\right)Q\left(2\right)\in ℝ$$
21	20 7	ifcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to if\left(k=4,Q\left(1\right)Q\left(2\right),0\right)\in ℝ$$
22	9 14	remulcld	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to Q\left(2\right)Q\left(3\right)\in ℝ$$
23	22	adantr	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to Q\left(2\right)Q\left(3\right)\in ℝ$$
24	23 7	ifcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to if\left(k=5,Q\left(2\right)Q\left(3\right),0\right)\in ℝ$$
25	21 24	readdcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to if\left(k=4,Q\left(1\right)Q\left(2\right),0\right)+if\left(k=5,Q\left(2\right)Q\left(3\right),0\right)\in ℝ$$
26	14 4	remulcld	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to Q\left(3\right)Q\left(1\right)\in ℝ$$
27	26	adantr	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to Q\left(3\right)Q\left(1\right)\in ℝ$$
28	27 7	ifcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to if\left(k=6,Q\left(3\right)Q\left(1\right),0\right)\in ℝ$$
29	25 28	readdcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to if\left(k=4,Q\left(1\right)Q\left(2\right),0\right)+if\left(k=5,Q\left(2\right)Q\left(3\right),0\right)+if\left(k=6,Q\left(3\right)Q\left(1\right),0\right)\in ℝ$$
30	18 29	readdcld	$$⊢\left(\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\wedge k\in \left(1\dots 6\right)\right)\to \left(if\left(k=1,{Q\left(1\right)}^2,0\right)+if\left(k=2,{Q\left(2\right)}^2,0\right)\right)+if\left(k=3,{Q\left(3\right)}^2,0\right)+\left(if\left(k=4,Q\left(1\right)Q\left(2\right),0\right)+if\left(k=5,Q\left(2\right)Q\left(3\right),0\right)\right)+if\left(k=6,Q\left(3\right)Q\left(1\right),0\right)\in ℝ$$
31	30	fmpttd	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to \left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{Q\left(1\right)}^2,0\right)+if\left(k=2,{Q\left(2\right)}^2,0\right)\right)+if\left(k=3,{Q\left(3\right)}^2,0\right)+\left(if\left(k=4,Q\left(1\right)Q\left(2\right),0\right)+if\left(k=5,Q\left(2\right)Q\left(3\right),0\right)\right)+if\left(k=6,Q\left(3\right)Q\left(1\right),0\right)\right):\left(1\dots 6\right)⟶ℝ$$
32		simpr	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to K\in \left(1\dots 6\right)$$
33	31 32	ffvelcdmd	$$⊢\left(Q\in \left({ℝ}^{\left(1\dots 3\right)}\right)\wedge K\in \left(1\dots 6\right)\right)\to \left(k\in \left(1\dots 6\right)⟼\left(if\left(k=1,{Q\left(1\right)}^2,0\right)+if\left(k=2,{Q\left(2\right)}^2,0\right)\right)+if\left(k=3,{Q\left(3\right)}^2,0\right)+\left(if\left(k=4,Q\left(1\right)Q\left(2\right),0\right)+if\left(k=5,Q\left(2\right)Q\left(3\right),0\right)\right)+if\left(k=6,Q\left(3\right)Q\left(1\right),0\right)\right)\left(K\right)\in ℝ$$
34	3 33	eqeltrd	Could not format ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( veronese ` Q ) ` K ) e. RR ) : No typesetting found for |- ( ( Q e. ( RR ^m ( 1 ... 3 ) ) /\ K e. ( 1 ... 6 ) ) -> ( ( veronese ` Q ) ` K ) e. RR ) with typecode |-