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 ⊢ 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) )
veroquad.f ⊢ ( 𝜑 → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
veroquad.k ⊢ ( 𝜑 → 𝐾 : ( 1 ... 6 ) ⟶ ℝ )
veroquad.q ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) = 0 )
veroquadnolindf.n ⊢ ( 𝜑 → 𝐾 ≠ ( ( 1 ... 6 ) × { 0 } ) )
Assertion veroquaddetzerod ( 𝜑 → ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) = 0 )

Proof

Step Hyp Ref Expression
1 veroquad.a ⊢ 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) )
2 veroquad.f ⊢ ( 𝜑 → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
3 veroquad.k ⊢ ( 𝜑 → 𝐾 : ( 1 ... 6 ) ⟶ ℝ )
4 veroquad.q ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 6 ) ) → ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) = 0 )
5 veroquadnolindf.n ⊢ ( 𝜑 → 𝐾 ≠ ( ( 1 ... 6 ) × { 0 } ) )
6 refld ⊢ ℝfld ∈ Field
7 isfld ⊢ ( ℝfld ∈ Field ↔ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) )
8 6 7 mpbi ⊢ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing )
9 8 simpri ⊢ ℝfld ∈ CRing
10 1 2 veronesematbasd ⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) )
11 eqid ⊢ ( ( 1 ... 6 ) maDet ℝfld ) = ( ( 1 ... 6 ) maDet ℝfld )
12 eqid ⊢ ( ( 1 ... 6 ) Mat ℝfld ) = ( ( 1 ... 6 ) Mat ℝfld )
13 eqid ⊢ ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) = ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) )
14 rebase ⊢ ℝ = ( Base ‘ ℝfld )
15 11 12 13 14 mdetcl ⊢ ( ( ℝfld ∈ CRing ∧ 𝑉 ∈ ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) ) → ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ∈ ℝ )
16 9 10 15 sylancr ⊢ ( 𝜑 → ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ∈ ℝ )
17 11 12 13 mdettpos ⊢ ( ( ℝfld ∈ CRing ∧ 𝑉 ∈ ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) ) → ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ tpos 𝑉 ) = ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) )
18 9 10 17 sylancr ⊢ ( 𝜑 → ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ tpos 𝑉 ) = ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) )
19 1 2 3 4 5 veroquadnolindfd ⊢ ( 𝜑 → ¬ curry tpos 𝑉 LIndF ( ℝfld freeLMod ( 1 ... 6 ) ) )
20 2fveq3 ⊢ ( 𝑖 = 𝑢 → ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) = ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) )
21 20 fveq1d ⊢ ( 𝑖 = 𝑢 → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑗 ) )
22 fveq2 ⊢ ( 𝑗 = 𝑣 → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
23 21 22 cbvmpov ⊢ ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) ) = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
24 1 23 eqtri ⊢ 𝑉 = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
25 24 tposmpo ⊢ tpos 𝑉 = ( 𝑣 ∈ ( 1 ... 6 ) , 𝑢 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
26 25 a1i ⊢ ( 𝜑 → tpos 𝑉 = ( 𝑣 ∈ ( 1 ... 6 ) , 𝑢 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
27 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
28 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → 𝑢 ∈ ( 1 ... 6 ) )
29 27 28 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
30 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → 𝑣 ∈ ( 1 ... 6 ) )
31 veronesefvcl ⊢ ( ( ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
32 29 30 31 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
33 26 32 fmpod ⊢ ( 𝜑 → tpos 𝑉 : ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ⟶ ℝ )
34 reex ⊢ ℝ ∈ V
35 ovex ⊢ ( 1 ... 6 ) ∈ V
36 sqxpexg ⊢ ( ( 1 ... 6 ) ∈ V → ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ∈ V )
37 35 36 ax-mp ⊢ ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ∈ V
38 34 37 elmap ⊢ ( tpos 𝑉 ∈ ( ℝ ↑m ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ) ↔ tpos 𝑉 : ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ⟶ ℝ )
39 33 38 sylibr ⊢ ( 𝜑 → tpos 𝑉 ∈ ( ℝ ↑m ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ) )
40 fzfi ⊢ ( 1 ... 6 ) ∈ Fin
41 6 elexi ⊢ ℝfld ∈ V
42 12 14 matbas2 ⊢ ( ( ( 1 ... 6 ) ∈ Fin ∧ ℝfld ∈ V ) → ( ℝ ↑m ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ) = ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) )
43 40 41 42 mp2an ⊢ ( ℝ ↑m ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ) = ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) )
44 39 43 eleqtrdi ⊢ ( 𝜑 → tpos 𝑉 ∈ ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) )
45 matunitlindf ⊢ ( ( ℝfld ∈ Field ∧ tpos 𝑉 ∈ ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) ) → ( tpos 𝑉 ∈ ( Unit ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) ↔ curry tpos 𝑉 LIndF ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
46 6 44 45 sylancr ⊢ ( 𝜑 → ( tpos 𝑉 ∈ ( Unit ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) ↔ curry tpos 𝑉 LIndF ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
47 19 46 mtbird ⊢ ( 𝜑 → ¬ tpos 𝑉 ∈ ( Unit ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) )
48 eqid ⊢ ( Unit ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) = ( Unit ‘ ( ( 1 ... 6 ) Mat ℝfld ) )
49 eqid ⊢ ( Unit ‘ ℝfld ) = ( Unit ‘ ℝfld )
50 12 11 13 48 49 matunit ⊢ ( ( ℝfld ∈ CRing ∧ tpos 𝑉 ∈ ( Base ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) ) → ( tpos 𝑉 ∈ ( Unit ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) ↔ ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ tpos 𝑉 ) ∈ ( Unit ‘ ℝfld ) ) )
51 9 44 50 sylancr ⊢ ( 𝜑 → ( tpos 𝑉 ∈ ( Unit ‘ ( ( 1 ... 6 ) Mat ℝfld ) ) ↔ ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ tpos 𝑉 ) ∈ ( Unit ‘ ℝfld ) ) )
52 47 51 mtbid ⊢ ( 𝜑 → ¬ ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ tpos 𝑉 ) ∈ ( Unit ‘ ℝfld ) )
53 18 52 eqneltrrd ⊢ ( 𝜑 → ¬ ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ∈ ( Unit ‘ ℝfld ) )
54 8 simpli ⊢ ℝfld ∈ DivRing
55 eqid ⊢ ( 0g ‘ ℝfld ) = ( 0g ‘ ℝfld )
56 14 49 55 drngunit ⊢ ( ℝfld ∈ DivRing → ( ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ∈ ( Unit ‘ ℝfld ) ↔ ( ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ∈ ℝ ∧ ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ≠ ( 0g ‘ ℝfld ) ) ) )
57 54 56 mp1i ⊢ ( 𝜑 → ( ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ∈ ( Unit ‘ ℝfld ) ↔ ( ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ∈ ℝ ∧ ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ≠ ( 0g ‘ ℝfld ) ) ) )
58 53 57 mtbid ⊢ ( 𝜑 → ¬ ( ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ∈ ℝ ∧ ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ≠ ( 0g ‘ ℝfld ) ) )
59 16 58 mpnanrd ⊢ ( 𝜑 → ¬ ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ≠ ( 0g ‘ ℝfld ) )
60 nne ⊢ ( ¬ ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) ≠ ( 0g ‘ ℝfld ) ↔ ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) = ( 0g ‘ ℝfld ) )
61 59 60 sylib ⊢ ( 𝜑 → ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) = ( 0g ‘ ℝfld ) )
62 re0g ⊢ 0 = ( 0g ‘ ℝfld )
63 61 62 eqtr4di ⊢ ( 𝜑 → ( ( ( 1 ... 6 ) maDet ℝfld ) ‘ 𝑉 ) = 0 )