Metamath Proof Explorer

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 
|- 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 veroquaddetzerod 
|- ( ph -> ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) = 0 )

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 simpri 
 |-  RRfld e. CRing
10 1 2 veronesematbasd 
 |-  ( ph -> V e. ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) )
11 eqid 
 |-  ( ( 1 ... 6 ) maDet RRfld ) = ( ( 1 ... 6 ) maDet RRfld )
12 eqid 
 |-  ( ( 1 ... 6 ) Mat RRfld ) = ( ( 1 ... 6 ) Mat RRfld )
13 eqid 
 |-  ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) = ( Base ` ( ( 1 ... 6 ) Mat RRfld ) )
14 rebase 
 |-  RR = ( Base ` RRfld )
15 11 12 13 14 mdetcl 
 |-  ( ( RRfld e. CRing /\ V e. ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) ) -> ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) e. RR )
16 9 10 15 sylancr 
 |-  ( ph -> ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) e. RR )
17 11 12 13 mdettpos 
 |-  ( ( RRfld e. CRing /\ V e. ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) ) -> ( ( ( 1 ... 6 ) maDet RRfld ) ` tpos V ) = ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) )
18 9 10 17 sylancr 
 |-  ( ph -> ( ( ( 1 ... 6 ) maDet RRfld ) ` tpos V ) = ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) )
19 1 2 3 4 5 veroquadnolindfd 
 |-  ( ph -> -. curry tpos V LIndF ( RRfld freeLMod ( 1 ... 6 ) ) )
20 2fveq3 
 |-  ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) )
21 20 fveq1d 
 |-  ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) )
22 fveq2 
 |-  ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) )
23 21 22 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 ) )
24 1 23 eqtri 
 |-  V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
25 24 tposmpo 
 |-  tpos V = ( v e. ( 1 ... 6 ) , u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
26 25 a1i 
 |-  ( ph -> tpos V = ( v e. ( 1 ... 6 ) , u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) )
27 2 adantr 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
28 simprr 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> u e. ( 1 ... 6 ) )
29 27 28 ffvelcdmd 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) )
30 simprl 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> v e. ( 1 ... 6 ) )
31 veronesefvcl 
 |-  ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
32 29 30 31 syl2anc 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
33 26 32 fmpod 
 |-  ( ph -> tpos V : ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) --> RR )
34 reex 
 |-  RR e. _V
35 ovex 
 |-  ( 1 ... 6 ) e. _V
36 sqxpexg 
 |-  ( ( 1 ... 6 ) e. _V -> ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) e. _V )
37 35 36 ax-mp 
 |-  ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) e. _V
38 34 37 elmap 
 |-  ( tpos V e. ( RR ^m ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) ) <-> tpos V : ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) --> RR )
39 33 38 sylibr 
 |-  ( ph -> tpos V e. ( RR ^m ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) ) )
40 fzfi 
 |-  ( 1 ... 6 ) e. Fin
41 6 elexi 
 |-  RRfld e. _V
42 12 14 matbas2 
 |-  ( ( ( 1 ... 6 ) e. Fin /\ RRfld e. _V ) -> ( RR ^m ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) ) = ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) )
43 40 41 42 mp2an 
 |-  ( RR ^m ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) ) = ( Base ` ( ( 1 ... 6 ) Mat RRfld ) )
44 39 43 eleqtrdi 
 |-  ( ph -> tpos V e. ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) )
45 matunitlindf 
 |-  ( ( RRfld e. Field /\ tpos V e. ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) ) -> ( tpos V e. ( Unit ` ( ( 1 ... 6 ) Mat RRfld ) ) <-> curry tpos V LIndF ( RRfld freeLMod ( 1 ... 6 ) ) ) )
46 6 44 45 sylancr 
 |-  ( ph -> ( tpos V e. ( Unit ` ( ( 1 ... 6 ) Mat RRfld ) ) <-> curry tpos V LIndF ( RRfld freeLMod ( 1 ... 6 ) ) ) )
47 19 46 mtbird 
 |-  ( ph -> -. tpos V e. ( Unit ` ( ( 1 ... 6 ) Mat RRfld ) ) )
48 eqid 
 |-  ( Unit ` ( ( 1 ... 6 ) Mat RRfld ) ) = ( Unit ` ( ( 1 ... 6 ) Mat RRfld ) )
49 eqid 
 |-  ( Unit ` RRfld ) = ( Unit ` RRfld )
50 12 11 13 48 49 matunit 
 |-  ( ( RRfld e. CRing /\ tpos V e. ( Base ` ( ( 1 ... 6 ) Mat RRfld ) ) ) -> ( tpos V e. ( Unit ` ( ( 1 ... 6 ) Mat RRfld ) ) <-> ( ( ( 1 ... 6 ) maDet RRfld ) ` tpos V ) e. ( Unit ` RRfld ) ) )
51 9 44 50 sylancr 
 |-  ( ph -> ( tpos V e. ( Unit ` ( ( 1 ... 6 ) Mat RRfld ) ) <-> ( ( ( 1 ... 6 ) maDet RRfld ) ` tpos V ) e. ( Unit ` RRfld ) ) )
52 47 51 mtbid 
 |-  ( ph -> -. ( ( ( 1 ... 6 ) maDet RRfld ) ` tpos V ) e. ( Unit ` RRfld ) )
53 18 52 eqneltrrd 
 |-  ( ph -> -. ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) e. ( Unit ` RRfld ) )
54 8 simpli 
 |-  RRfld e. DivRing
55 eqid 
 |-  ( 0g ` RRfld ) = ( 0g ` RRfld )
56 14 49 55 drngunit 
 |-  ( RRfld e. DivRing -> ( ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) e. ( Unit ` RRfld ) <-> ( ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) e. RR /\ ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) =/= ( 0g ` RRfld ) ) ) )
57 54 56 mp1i 
 |-  ( ph -> ( ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) e. ( Unit ` RRfld ) <-> ( ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) e. RR /\ ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) =/= ( 0g ` RRfld ) ) ) )
58 53 57 mtbid 
 |-  ( ph -> -. ( ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) e. RR /\ ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) =/= ( 0g ` RRfld ) ) )
59 16 58 mpnanrd 
 |-  ( ph -> -. ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) =/= ( 0g ` RRfld ) )
60 nne 
 |-  ( -. ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) =/= ( 0g ` RRfld ) <-> ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) = ( 0g ` RRfld ) )
61 59 60 sylib 
 |-  ( ph -> ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) = ( 0g ` RRfld ) )
62 re0g 
 |-  0 = ( 0g ` RRfld )
63 61 62 eqtr4di 
 |-  ( ph -> ( ( ( 1 ... 6 ) maDet RRfld ) ` V ) = 0 )