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 ⊢ 𝑉 = ( 𝑖 ∈ ( 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 veroquadnolindfd ( 𝜑 → ¬ curry tpos 𝑉 LIndF ( ℝfld freeLMod ( 1 ... 6 ) ) )

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 simpli ⊢ ℝfld ∈ DivRing
10 drngring ⊢ ( ℝfld ∈ DivRing → ℝfld ∈ Ring )
11 9 10 ax-mp ⊢ ℝfld ∈ Ring
12 ovex ⊢ ( 1 ... 6 ) ∈ V
13 eqid ⊢ ( ℝfld freeLMod ( 1 ... 6 ) ) = ( ℝfld freeLMod ( 1 ... 6 ) )
14 13 frlmlmod ⊢ ( ( ℝfld ∈ Ring ∧ ( 1 ... 6 ) ∈ V ) → ( ℝfld freeLMod ( 1 ... 6 ) ) ∈ LMod )
15 11 12 14 mp2an ⊢ ( ℝfld freeLMod ( 1 ... 6 ) ) ∈ LMod
16 15 a1i ⊢ ( 𝜑 → ( ℝfld freeLMod ( 1 ... 6 ) ) ∈ LMod )
17 12 a1i ⊢ ( 𝜑 → ( 1 ... 6 ) ∈ V )
18 6 elexi ⊢ ℝfld ∈ V
19 fzfi ⊢ ( 1 ... 6 ) ∈ Fin
20 rebase ⊢ ℝ = ( Base ‘ ℝfld )
21 13 20 frlmfibas ⊢ ( ( ℝfld ∈ V ∧ ( 1 ... 6 ) ∈ Fin ) → ( ℝ ↑m ( 1 ... 6 ) ) = ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
22 18 19 21 mp2an ⊢ ( ℝ ↑m ( 1 ... 6 ) ) = ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
23 22 a1i ⊢ ( 𝜑 → ( ℝ ↑m ( 1 ... 6 ) ) = ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
24 2fveq3 ⊢ ( 𝑖 = 𝑢 → ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) = ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) )
25 24 fveq1d ⊢ ( 𝑖 = 𝑢 → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑗 ) )
26 fveq2 ⊢ ( 𝑗 = 𝑣 → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
27 25 26 cbvmpov ⊢ ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) ) = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
28 1 27 eqtri ⊢ 𝑉 = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
29 28 tposmpo ⊢ tpos 𝑉 = ( 𝑣 ∈ ( 1 ... 6 ) , 𝑢 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
30 29 a1i ⊢ ( 𝜑 → tpos 𝑉 = ( 𝑣 ∈ ( 1 ... 6 ) , 𝑢 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
31 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
32 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → 𝑢 ∈ ( 1 ... 6 ) )
33 31 32 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
34 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → 𝑣 ∈ ( 1 ... 6 ) )
35 veronesefvcl ⊢ ( ( ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
36 33 34 35 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
37 30 36 fmpod ⊢ ( 𝜑 → tpos 𝑉 : ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ⟶ ℝ )
38 1nn ⊢ 1 ∈ ℕ
39 6nn ⊢ 6 ∈ ℕ
40 1re ⊢ 1 ∈ ℝ
41 6re ⊢ 6 ∈ ℝ
42 1lt6 ⊢ 1 < 6
43 40 41 42 ltleii ⊢ 1 ≤ 6
44 elfz1b ⊢ ( 1 ∈ ( 1 ... 6 ) ↔ ( 1 ∈ ℕ ∧ 6 ∈ ℕ ∧ 1 ≤ 6 ) )
45 38 39 43 44 mpbir3an ⊢ 1 ∈ ( 1 ... 6 )
46 45 ne0ii ⊢ ( 1 ... 6 ) ≠ ∅
47 eldifsn ⊢ ( ( 1 ... 6 ) ∈ ( V ∖ { ∅ } ) ↔ ( ( 1 ... 6 ) ∈ V ∧ ( 1 ... 6 ) ≠ ∅ ) )
48 12 46 47 mpbir2an ⊢ ( 1 ... 6 ) ∈ ( V ∖ { ∅ } )
49 48 a1i ⊢ ( 𝜑 → ( 1 ... 6 ) ∈ ( V ∖ { ∅ } ) )
50 reex ⊢ ℝ ∈ V
51 50 a1i ⊢ ( 𝜑 → ℝ ∈ V )
52 curf ⊢ ( ( tpos 𝑉 : ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ⟶ ℝ ∧ ( 1 ... 6 ) ∈ ( V ∖ { ∅ } ) ∧ ℝ ∈ V ) → curry tpos 𝑉 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 6 ) ) )
53 37 49 51 52 syl3anc ⊢ ( 𝜑 → curry tpos 𝑉 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 6 ) ) )
54 23 53 feq3dd ⊢ ( 𝜑 → curry tpos 𝑉 : ( 1 ... 6 ) ⟶ ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
55 50 12 elmap ⊢ ( 𝐾 ∈ ( ℝ ↑m ( 1 ... 6 ) ) ↔ 𝐾 : ( 1 ... 6 ) ⟶ ℝ )
56 3 55 sylibr ⊢ ( 𝜑 → 𝐾 ∈ ( ℝ ↑m ( 1 ... 6 ) ) )
57 56 23 eleqtrd ⊢ ( 𝜑 → 𝐾 ∈ ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
58 1 2 3 4 veroquadmodzerod ⊢ ( 𝜑 → ( ( ℝfld freeLMod ( 1 ... 6 ) ) Σg ( 𝐾 ∘f ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) curry tpos 𝑉 ) ) = ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
59 eqid ⊢ ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) = ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
60 13 frlmsca ⊢ ( ( ℝfld ∈ V ∧ ( 1 ... 6 ) ∈ V ) → ℝfld = ( Scalar ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
61 18 12 60 mp2an ⊢ ℝfld = ( Scalar ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
62 eqid ⊢ ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) = ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
63 eqid ⊢ ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) = ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
64 re0g ⊢ 0 = ( 0g ‘ ℝfld )
65 59 61 62 63 64 59 nellindf ⊢ ( ( ( ( ℝfld freeLMod ( 1 ... 6 ) ) ∈ LMod ∧ ( 1 ... 6 ) ∈ V ∧ curry tpos 𝑉 : ( 1 ... 6 ) ⟶ ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) ) ∧ ( 𝐾 ∈ ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) ∧ 𝐾 ≠ ( ( 1 ... 6 ) × { 0 } ) ∧ ( ( ℝfld freeLMod ( 1 ... 6 ) ) Σg ( 𝐾 ∘f ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) curry tpos 𝑉 ) ) = ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) ) ) → ¬ curry tpos 𝑉 LIndF ( ℝfld freeLMod ( 1 ... 6 ) ) )
66 16 17 54 57 5 58 65 syl33anc ⊢ ( 𝜑 → ¬ curry tpos 𝑉 LIndF ( ℝfld freeLMod ( 1 ... 6 ) ) )