Metamath Proof Explorer

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 
|- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) )
veroquad.f 
|- ( ph -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
veroquad.k 
|- ( ph -> K : ( 1 ... 6 ) --> RR )
veroquad.q 
|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( ( ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) ) + ( ( K ` 3 ) x. ( ( ( A ` i ) ` 3 ) ^ 2 ) ) ) + ( ( ( ( K ` 4 ) x. ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) ) + ( ( K ` 5 ) x. ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) ) ) + ( ( K ` 6 ) x. ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) ) ) = 0 )
veroquadnolindf.n 
|- ( ph -> K =/= ( ( 1 ... 6 ) X. { 0 } ) )
Assertion veroquadnolindfd 
|- ( ph -> -. curry tpos V LIndF ( RRfld freeLMod ( 1 ... 6 ) ) )

Proof

Step Hyp Ref Expression
1 veroquad.a 
 |-  V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) )
2 veroquad.f 
 |-  ( ph -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
3 veroquad.k 
 |-  ( ph -> K : ( 1 ... 6 ) --> RR )
4 veroquad.q 
 |-  ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( ( ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) ) + ( ( K ` 3 ) x. ( ( ( A ` i ) ` 3 ) ^ 2 ) ) ) + ( ( ( ( K ` 4 ) x. ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) ) + ( ( K ` 5 ) x. ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) ) ) + ( ( K ` 6 ) x. ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) ) ) = 0 )
5 veroquadnolindf.n 
 |-  ( ph -> K =/= ( ( 1 ... 6 ) X. { 0 } ) )
6 refld 
 |-  RRfld e. Field
7 isfld 
 |-  ( RRfld e. Field <-> ( RRfld e. DivRing /\ RRfld e. CRing ) )
8 6 7 mpbi 
 |-  ( RRfld e. DivRing /\ RRfld e. CRing )
9 8 simpli 
 |-  RRfld e. DivRing
10 drngring 
 |-  ( RRfld e. DivRing -> RRfld e. Ring )
11 9 10 ax-mp 
 |-  RRfld e. Ring
12 ovex 
 |-  ( 1 ... 6 ) e. _V
13 eqid 
 |-  ( RRfld freeLMod ( 1 ... 6 ) ) = ( RRfld freeLMod ( 1 ... 6 ) )
14 13 frlmlmod 
 |-  ( ( RRfld e. Ring /\ ( 1 ... 6 ) e. _V ) -> ( RRfld freeLMod ( 1 ... 6 ) ) e. LMod )
15 11 12 14 mp2an 
 |-  ( RRfld freeLMod ( 1 ... 6 ) ) e. LMod
16 15 a1i 
 |-  ( ph -> ( RRfld freeLMod ( 1 ... 6 ) ) e. LMod )
17 12 a1i 
 |-  ( ph -> ( 1 ... 6 ) e. _V )
18 6 elexi 
 |-  RRfld e. _V
19 fzfi 
 |-  ( 1 ... 6 ) e. Fin
20 rebase 
 |-  RR = ( Base ` RRfld )
21 13 20 frlmfibas 
 |-  ( ( RRfld e. _V /\ ( 1 ... 6 ) e. Fin ) -> ( RR ^m ( 1 ... 6 ) ) = ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
22 18 19 21 mp2an 
 |-  ( RR ^m ( 1 ... 6 ) ) = ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) )
23 22 a1i 
 |-  ( ph -> ( RR ^m ( 1 ... 6 ) ) = ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
24 2fveq3 
 |-  ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) )
25 24 fveq1d 
 |-  ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) )
26 fveq2 
 |-  ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) )
27 25 26 cbvmpov 
 |-  ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
28 1 27 eqtri 
 |-  V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
29 28 tposmpo 
 |-  tpos V = ( v e. ( 1 ... 6 ) , u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
30 29 a1i 
 |-  ( ph -> tpos V = ( v e. ( 1 ... 6 ) , u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) )
31 2 adantr 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
32 simprr 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> u e. ( 1 ... 6 ) )
33 31 32 ffvelcdmd 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) )
34 simprl 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> v e. ( 1 ... 6 ) )
35 veronesefvcl 
 |-  ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
36 33 34 35 syl2anc 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
37 30 36 fmpod 
 |-  ( ph -> tpos V : ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) --> RR )
38 1nn 
 |-  1 e. NN
39 6nn 
 |-  6 e. NN
40 1re 
 |-  1 e. RR
41 6re 
 |-  6 e. RR
42 1lt6 
 |-  1 < 6
43 40 41 42 ltleii 
 |-  1 <_ 6
44 elfz1b 
 |-  ( 1 e. ( 1 ... 6 ) <-> ( 1 e. NN /\ 6 e. NN /\ 1 <_ 6 ) )
45 38 39 43 44 mpbir3an 
 |-  1 e. ( 1 ... 6 )
46 45 ne0ii 
 |-  ( 1 ... 6 ) =/= (/)
47 eldifsn 
 |-  ( ( 1 ... 6 ) e. ( _V \ { (/) } ) <-> ( ( 1 ... 6 ) e. _V /\ ( 1 ... 6 ) =/= (/) ) )
48 12 46 47 mpbir2an 
 |-  ( 1 ... 6 ) e. ( _V \ { (/) } )
49 48 a1i 
 |-  ( ph -> ( 1 ... 6 ) e. ( _V \ { (/) } ) )
50 reex 
 |-  RR e. _V
51 50 a1i 
 |-  ( ph -> RR e. _V )
52 curf 
 |-  ( ( tpos V : ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) --> RR /\ ( 1 ... 6 ) e. ( _V \ { (/) } ) /\ RR e. _V ) -> curry tpos V : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 6 ) ) )
53 37 49 51 52 syl3anc 
 |-  ( ph -> curry tpos V : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 6 ) ) )
54 23 53 feq3dd 
 |-  ( ph -> curry tpos V : ( 1 ... 6 ) --> ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
55 50 12 elmap 
 |-  ( K e. ( RR ^m ( 1 ... 6 ) ) <-> K : ( 1 ... 6 ) --> RR )
56 3 55 sylibr 
 |-  ( ph -> K e. ( RR ^m ( 1 ... 6 ) ) )
57 56 23 eleqtrd 
 |-  ( ph -> K e. ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
58 1 2 3 4 veroquadmodzerod 
 |-  ( ph -> ( ( RRfld freeLMod ( 1 ... 6 ) ) gsum ( K oF ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) curry tpos V ) ) = ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
59 eqid 
 |-  ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) = ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) )
60 13 frlmsca 
 |-  ( ( RRfld e. _V /\ ( 1 ... 6 ) e. _V ) -> RRfld = ( Scalar ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
61 18 12 60 mp2an 
 |-  RRfld = ( Scalar ` ( RRfld freeLMod ( 1 ... 6 ) ) )
62 eqid 
 |-  ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) = ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) )
63 eqid 
 |-  ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) ) = ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) )
64 re0g 
 |-  0 = ( 0g ` RRfld )
65 59 61 62 63 64 59 nellindf 
 |-  ( ( ( ( RRfld freeLMod ( 1 ... 6 ) ) e. LMod /\ ( 1 ... 6 ) e. _V /\ curry tpos V : ( 1 ... 6 ) --> ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) ) /\ ( K e. ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) /\ K =/= ( ( 1 ... 6 ) X. { 0 } ) /\ ( ( RRfld freeLMod ( 1 ... 6 ) ) gsum ( K oF ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) curry tpos V ) ) = ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) ) ) ) -> -. curry tpos V LIndF ( RRfld freeLMod ( 1 ... 6 ) ) )
66 16 17 54 57 5 58 65 syl33anc 
 |-  ( ph -> -. curry tpos V LIndF ( RRfld freeLMod ( 1 ... 6 ) ) )