Theorem veroquaddetzerod

Description: The Veronese matrix of six points satisfying a common nonzero homogeneous quadratic equation has determinant zero. (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	veroquaddetzerod	$$⊢\phi \to \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)=0$$

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	simpri	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CRing}$$
10	1 2	veronesematbasd	$$⊢\phi \to V\in {\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}$$
11		eqid	$$⊢\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}=\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}$$
12		eqid	$$⊢\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}=\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}$$
13		eqid	$$⊢{\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}={\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}$$
14		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
15	11 12 13 14	mdetcl	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{CRing}\wedge V\in {\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}\right)\to \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\in ℝ$$
16	9 10 15	sylancr	$$⊢\phi \to \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\in ℝ$$
17	11 12 13	mdettpos	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{CRing}\wedge V\in {\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}\right)\to \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(tposV\right)=\left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)$$
18	9 10 17	sylancr	$$⊢\phi \to \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(tposV\right)=\left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)$$
19	1 2 3 4 5	veroquadnolindfd	$$⊢\phi \to \neg currytposV\mathrm{LIndF}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)$$
20		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 |-
21	20	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 |-
22		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 |-
23	21 22	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 |-
24	1 23	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 |-
25	24	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 |-
26	25	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 |-
27	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)}$$
28		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)$$
29	27 28	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)$$
30		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)$$
31		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 |-
32	29 30 31	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 |-
33	26 32	fmpod	$$⊢\phi \to tposV:\left(1\dots 6\right)\times \left(1\dots 6\right)⟶ℝ$$
34		reex	$$⊢ℝ\in \mathrm{V}$$
35		ovex	$$⊢\left(1\dots 6\right)\in \mathrm{V}$$
36		sqxpexg	$$⊢\left(1\dots 6\right)\in \mathrm{V}\to \left(1\dots 6\right)\times \left(1\dots 6\right)\in \mathrm{V}$$
37	35 36	ax-mp	$$⊢\left(1\dots 6\right)\times \left(1\dots 6\right)\in \mathrm{V}$$
38	34 37	elmap	$$⊢tposV\in \left({ℝ}^{\left(\left(1\dots 6\right)\times \left(1\dots 6\right)\right)}\right)\leftrightarrow tposV:\left(1\dots 6\right)\times \left(1\dots 6\right)⟶ℝ$$
39	33 38	sylibr	$$⊢\phi \to tposV\in \left({ℝ}^{\left(\left(1\dots 6\right)\times \left(1\dots 6\right)\right)}\right)$$
40		fzfi	$$⊢\left(1\dots 6\right)\in \mathrm{Fin}$$
41	6	elexi	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{V}$$
42	12 14	matbas2	$$⊢\left(\left(1\dots 6\right)\in \mathrm{Fin}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{V}\right)\to {ℝ}^{\left(\left(1\dots 6\right)\times \left(1\dots 6\right)\right)}={\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}$$
43	40 41 42	mp2an	$$⊢{ℝ}^{\left(\left(1\dots 6\right)\times \left(1\dots 6\right)\right)}={\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}$$
44	39 43	eleqtrdi	$$⊢\phi \to tposV\in {\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}$$
45		matunitlindf	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{Field}\wedge tposV\in {\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}\right)\to \left(tposV\in \mathrm{Unit}\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)\leftrightarrow currytposV\mathrm{LIndF}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)\right)$$
46	6 44 45	sylancr	$$⊢\phi \to \left(tposV\in \mathrm{Unit}\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)\leftrightarrow currytposV\mathrm{LIndF}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)\right)$$
47	19 46	mtbird	$$⊢\phi \to \neg tposV\in \mathrm{Unit}\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)$$
48		eqid	$$⊢\mathrm{Unit}\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)=\mathrm{Unit}\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)$$
49		eqid	$$⊢\mathrm{Unit}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{Unit}\left({ℝ}_{\mathrm{fld}}\right)$$
50	12 11 13 48 49	matunit	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{CRing}\wedge tposV\in {\mathrm{Base}}_{\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)}\right)\to \left(tposV\in \mathrm{Unit}\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)\leftrightarrow \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(tposV\right)\in \mathrm{Unit}\left({ℝ}_{\mathrm{fld}}\right)\right)$$
51	9 44 50	sylancr	$$⊢\phi \to \left(tposV\in \mathrm{Unit}\left(\left(1\dots 6\right)\mathrm{Mat}{ℝ}_{\mathrm{fld}}\right)\leftrightarrow \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(tposV\right)\in \mathrm{Unit}\left({ℝ}_{\mathrm{fld}}\right)\right)$$
52	47 51	mtbid	$$⊢\phi \to \neg \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(tposV\right)\in \mathrm{Unit}\left({ℝ}_{\mathrm{fld}}\right)$$
53	18 52	eqneltrrd	$$⊢\phi \to \neg \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\in \mathrm{Unit}\left({ℝ}_{\mathrm{fld}}\right)$$
54	8	simpli	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
55		eqid	$$⊢0_{{ℝ}_{\mathrm{fld}}}=0_{{ℝ}_{\mathrm{fld}}}$$
56	14 49 55	drngunit	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\to \left(\left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\in \mathrm{Unit}\left({ℝ}_{\mathrm{fld}}\right)\leftrightarrow \left(\left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\in ℝ\wedge \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\ne 0_{{ℝ}_{\mathrm{fld}}}\right)\right)$$
57	54 56	mp1i	$$⊢\phi \to \left(\left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\in \mathrm{Unit}\left({ℝ}_{\mathrm{fld}}\right)\leftrightarrow \left(\left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\in ℝ\wedge \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\ne 0_{{ℝ}_{\mathrm{fld}}}\right)\right)$$
58	53 57	mtbid	$$⊢\phi \to \neg \left(\left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\in ℝ\wedge \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\ne 0_{{ℝ}_{\mathrm{fld}}}\right)$$
59	16 58	mpnanrd	$$⊢\phi \to \neg \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\ne 0_{{ℝ}_{\mathrm{fld}}}$$
60		nne	$$⊢\neg \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)\ne 0_{{ℝ}_{\mathrm{fld}}}\leftrightarrow \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)=0_{{ℝ}_{\mathrm{fld}}}$$
61	59 60	sylib	$$⊢\phi \to \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)=0_{{ℝ}_{\mathrm{fld}}}$$
62		re0g	$$⊢0=0_{{ℝ}_{\mathrm{fld}}}$$
63	61 62	eqtr4di	$$⊢\phi \to \left(\left(1\dots 6\right)\mathrm{maDet}{ℝ}_{\mathrm{fld}}\right)\left(V\right)=0$$