Theorem veroquadnolindfd

Description: A nonzero homogeneous quadratic equation satisfied by all six points gives a linear dependence among the columns of the Veronese matrix. (Contributed by Jiamin Zhao, 27-Aug-2026)

	Ref	Expression
Hypotheses	veroquad.a	No typesetting found for |- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) with typecode |-
	veroquad.f	$$⊢\phi \to A:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 3\right)}$$
	veroquad.k	$$⊢\phi \to K:\left(1\dots 6\right)⟶ℝ$$
	veroquad.q	$$⊢\left(\phi \wedge i\in \left(1\dots 6\right)\right)\to \left(K\left(1\right){A\left(i\right)\left(1\right)}^2+K\left(2\right){A\left(i\right)\left(2\right)}^2\right)+K\left(3\right){A\left(i\right)\left(3\right)}^2+\left(K\left(4\right)A\left(i\right)\left(1\right)A\left(i\right)\left(2\right)+K\left(5\right)A\left(i\right)\left(2\right)A\left(i\right)\left(3\right)\right)+K\left(6\right)A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)=0$$
	veroquadnolindf.n	$$⊢\phi \to K\ne \left(1\dots 6\right)\times \left\{0\right\}$$
Assertion	veroquadnolindfd	$$⊢\phi \to \neg currytposV\mathrm{LIndF}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		veroquad.a	Could not format V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) : No typesetting found for |- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) with typecode |-
2		veroquad.f	$$⊢\phi \to A:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 3\right)}$$
3		veroquad.k	$$⊢\phi \to K:\left(1\dots 6\right)⟶ℝ$$
4		veroquad.q	$$⊢\left(\phi \wedge i\in \left(1\dots 6\right)\right)\to \left(K\left(1\right){A\left(i\right)\left(1\right)}^2+K\left(2\right){A\left(i\right)\left(2\right)}^2\right)+K\left(3\right){A\left(i\right)\left(3\right)}^2+\left(K\left(4\right)A\left(i\right)\left(1\right)A\left(i\right)\left(2\right)+K\left(5\right)A\left(i\right)\left(2\right)A\left(i\right)\left(3\right)\right)+K\left(6\right)A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)=0$$
5		veroquadnolindf.n	$$⊢\phi \to K\ne \left(1\dots 6\right)\times \left\{0\right\}$$
6		refld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
7		isfld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}\leftrightarrow \left({ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{CRing}\right)$$
8	6 7	mpbi	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{CRing}\right)$$
9	8	simpli	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
10		drngring	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\to {ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
11	9 10	ax-mp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
12		ovex	$$⊢\left(1\dots 6\right)\in \mathrm{V}$$
13		eqid	$$⊢{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)={ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)$$
14	13	frlmlmod	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{Ring}\wedge \left(1\dots 6\right)\in \mathrm{V}\right)\to {ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\in \mathrm{LMod}$$
15	11 12 14	mp2an	$$⊢{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\in \mathrm{LMod}$$
16	15	a1i	$$⊢\phi \to {ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\in \mathrm{LMod}$$
17	12	a1i	$$⊢\phi \to \left(1\dots 6\right)\in \mathrm{V}$$
18	6	elexi	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{V}$$
19		fzfi	$$⊢\left(1\dots 6\right)\in \mathrm{Fin}$$
20		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
21	13 20	frlmfibas	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{V}\wedge \left(1\dots 6\right)\in \mathrm{Fin}\right)\to {ℝ}^{\left(1\dots 6\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}$$
22	18 19 21	mp2an	$$⊢{ℝ}^{\left(1\dots 6\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}$$
23	22	a1i	$$⊢\phi \to {ℝ}^{\left(1\dots 6\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}$$
24		2fveq3	Could not format ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) ) : No typesetting found for |- ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) ) with typecode |-
25	24	fveq1d	Could not format ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) ) : No typesetting found for |- ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) ) with typecode |-
26		fveq2	Could not format ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) ) : No typesetting found for |- ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) ) with typecode |-
27	25 26	cbvmpov	Could not format ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) : No typesetting found for |- ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) with typecode |-
28	1 27	eqtri	Could not format V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) : No typesetting found for |- V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) with typecode |-
29	28	tposmpo	Could not format tpos V = ( v e. ( 1 ... 6 ) , u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) : No typesetting found for |- tpos V = ( v e. ( 1 ... 6 ) , u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) with typecode |-
30	29	a1i	Could not format ( ph -> tpos V = ( v e. ( 1 ... 6 ) , u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) : No typesetting found for |- ( ph -> tpos V = ( v e. ( 1 ... 6 ) , u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) ) with typecode |-
31	2	adantr	$$⊢\left(\phi \wedge \left(v\in \left(1\dots 6\right)\wedge u\in \left(1\dots 6\right)\right)\right)\to A:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 3\right)}$$
32		simprr	$$⊢\left(\phi \wedge \left(v\in \left(1\dots 6\right)\wedge u\in \left(1\dots 6\right)\right)\right)\to u\in \left(1\dots 6\right)$$
33	31 32	ffvelcdmd	$$⊢\left(\phi \wedge \left(v\in \left(1\dots 6\right)\wedge u\in \left(1\dots 6\right)\right)\right)\to A\left(u\right)\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
34		simprl	$$⊢\left(\phi \wedge \left(v\in \left(1\dots 6\right)\wedge u\in \left(1\dots 6\right)\right)\right)\to v\in \left(1\dots 6\right)$$
35		veronesefvcl	Could not format ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) : No typesetting found for |- ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) with typecode |-
36	33 34 35	syl2anc	Could not format ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) : No typesetting found for |- ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR ) with typecode |-
37	30 36	fmpod	$$⊢\phi \to tposV:\left(1\dots 6\right)\times \left(1\dots 6\right)⟶ℝ$$
38		1nn	$$⊢1\in \mathbb{N}$$
39		6nn	$$⊢6\in \mathbb{N}$$
40		1re	$$⊢1\in ℝ$$
41		6re	$$⊢6\in ℝ$$
42		1lt6	$$⊢1<6$$
43	40 41 42	ltleii	$$⊢1\le 6$$
44		elfz1b	$$⊢1\in \left(1\dots 6\right)\leftrightarrow \left(1\in \mathbb{N}\wedge 6\in \mathbb{N}\wedge 1\le 6\right)$$
45	38 39 43 44	mpbir3an	$$⊢1\in \left(1\dots 6\right)$$
46	45	ne0ii	$$⊢\left(1\dots 6\right)\ne \varnothing$$
47		eldifsn	$$⊢\left(1\dots 6\right)\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\leftrightarrow \left(\left(1\dots 6\right)\in \mathrm{V}\wedge \left(1\dots 6\right)\ne \varnothing \right)$$
48	12 46 47	mpbir2an	$$⊢\left(1\dots 6\right)\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
49	48	a1i	$$⊢\phi \to \left(1\dots 6\right)\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
50		reex	$$⊢ℝ\in \mathrm{V}$$
51	50	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
52		curf	$$⊢\left(tposV:\left(1\dots 6\right)\times \left(1\dots 6\right)⟶ℝ\wedge \left(1\dots 6\right)\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\wedge ℝ\in \mathrm{V}\right)\to currytposV:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 6\right)}$$
53	37 49 51 52	syl3anc	$$⊢\phi \to currytposV:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 6\right)}$$
54	23 53	feq3dd	$$⊢\phi \to currytposV:\left(1\dots 6\right)⟶{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}$$
55	50 12	elmap	$$⊢K\in \left({ℝ}^{\left(1\dots 6\right)}\right)\leftrightarrow K:\left(1\dots 6\right)⟶ℝ$$
56	3 55	sylibr	$$⊢\phi \to K\in \left({ℝ}^{\left(1\dots 6\right)}\right)$$
57	56 23	eleqtrd	$$⊢\phi \to K\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}$$
58	1 2 3 4	veroquadmodzerod	$$⊢\phi \to {\sum }_{{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)}\left(K{{\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}}_{f}currytposV\right)=0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}$$
59		eqid	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}$$
60	13	frlmsca	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{V}\wedge \left(1\dots 6\right)\in \mathrm{V}\right)\to {ℝ}_{\mathrm{fld}}=\mathrm{Scalar}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)$$
61	18 12 60	mp2an	$$⊢{ℝ}_{\mathrm{fld}}=\mathrm{Scalar}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)$$
62		eqid	$$⊢{\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}={\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}$$
63		eqid	$$⊢0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}=0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}$$
64		re0g	$$⊢0=0_{{ℝ}_{\mathrm{fld}}}$$
65	59 61 62 63 64 59	nellindf	$$⊢\left(\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\in \mathrm{LMod}\wedge \left(1\dots 6\right)\in \mathrm{V}\wedge currytposV:\left(1\dots 6\right)⟶{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}\right)\wedge \left(K\in {\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}\wedge K\ne \left(1\dots 6\right)\times \left\{0\right\}\wedge {\sum }_{{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)}\left(K{{\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}}_{f}currytposV\right)=0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}\right)\right)\to \neg currytposV\mathrm{LIndF}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)$$
66	16 17 54 57 5 58 65	syl33anc	$$⊢\phi \to \neg currytposV\mathrm{LIndF}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)$$