Metamath Proof Explorer

Theorem veroquadmodzerod

Description: The columns of the Veronese matrix, weighted by the coefficients K , sum to the zero vector of RRfld freeLMod ( 1 ... 6 ) . (Contributed by Jiamin Zhao, 19-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 )
Assertion veroquadmodzerod ( 𝜑 → ( ( ℝfld freeLMod ( 1 ... 6 ) ) Σg ( 𝐾 ∘f ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) curry tpos 𝑉 ) ) = ( 0g ‘ ( ℝ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 3 ffnd ⊢ ( 𝜑 → 𝐾 Fn ( 1 ... 6 ) )
6 2fveq3 ⊢ ( 𝑖 = 𝑢 → ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) = ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) )
7 6 fveq1d ⊢ ( 𝑖 = 𝑢 → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑗 ) )
8 fveq2 ⊢ ( 𝑗 = 𝑣 → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
9 7 8 cbvmpov ⊢ ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) ) = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
10 1 9 eqtri ⊢ 𝑉 = ( 𝑢 ∈ ( 1 ... 6 ) , 𝑣 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
11 10 tposmpo ⊢ tpos 𝑉 = ( 𝑣 ∈ ( 1 ... 6 ) , 𝑢 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) )
12 11 a1i ⊢ ( 𝜑 → tpos 𝑉 = ( 𝑣 ∈ ( 1 ... 6 ) , 𝑢 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
13 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
14 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → 𝑢 ∈ ( 1 ... 6 ) )
15 13 14 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
16 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → 𝑣 ∈ ( 1 ... 6 ) )
17 veronesefvcl ⊢ ( ( ( 𝐴 ‘ 𝑢 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑣 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
18 15 16 17 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 1 ... 6 ) ∧ 𝑢 ∈ ( 1 ... 6 ) ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
19 12 18 fmpod ⊢ ( 𝜑 → tpos 𝑉 : ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ⟶ ℝ )
20 ovex ⊢ ( 1 ... 6 ) ∈ V
21 1nn ⊢ 1 ∈ ℕ
22 6nn ⊢ 6 ∈ ℕ
23 1re ⊢ 1 ∈ ℝ
24 6re ⊢ 6 ∈ ℝ
25 1lt6 ⊢ 1 < 6
26 23 24 25 ltleii ⊢ 1 ≤ 6
27 elfz1b ⊢ ( 1 ∈ ( 1 ... 6 ) ↔ ( 1 ∈ ℕ ∧ 6 ∈ ℕ ∧ 1 ≤ 6 ) )
28 21 22 26 27 mpbir3an ⊢ 1 ∈ ( 1 ... 6 )
29 28 ne0ii ⊢ ( 1 ... 6 ) ≠ ∅
30 eldifsn ⊢ ( ( 1 ... 6 ) ∈ ( V ∖ { ∅ } ) ↔ ( ( 1 ... 6 ) ∈ V ∧ ( 1 ... 6 ) ≠ ∅ ) )
31 20 29 30 mpbir2an ⊢ ( 1 ... 6 ) ∈ ( V ∖ { ∅ } )
32 31 a1i ⊢ ( 𝜑 → ( 1 ... 6 ) ∈ ( V ∖ { ∅ } ) )
33 reex ⊢ ℝ ∈ V
34 33 a1i ⊢ ( 𝜑 → ℝ ∈ V )
35 curf ⊢ ( ( tpos 𝑉 : ( ( 1 ... 6 ) × ( 1 ... 6 ) ) ⟶ ℝ ∧ ( 1 ... 6 ) ∈ ( V ∖ { ∅ } ) ∧ ℝ ∈ V ) → curry tpos 𝑉 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 6 ) ) )
36 19 32 34 35 syl3anc ⊢ ( 𝜑 → curry tpos 𝑉 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 6 ) ) )
37 36 ffnd ⊢ ( 𝜑 → curry tpos 𝑉 Fn ( 1 ... 6 ) )
38 20 a1i ⊢ ( 𝜑 → ( 1 ... 6 ) ∈ V )
39 inidm ⊢ ( ( 1 ... 6 ) ∩ ( 1 ... 6 ) ) = ( 1 ... 6 )
40 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑛 ) )
41 18 ralrimivva ⊢ ( 𝜑 → ∀ 𝑣 ∈ ( 1 ... 6 ) ∀ 𝑢 ∈ ( 1 ... 6 ) ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ∀ 𝑣 ∈ ( 1 ... 6 ) ∀ 𝑢 ∈ ( 1 ... 6 ) ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ∈ ℝ )
43 29 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( 1 ... 6 ) ≠ ∅ )
44 20 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( 1 ... 6 ) ∈ V )
45 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → 𝑛 ∈ ( 1 ... 6 ) )
46 11 42 43 44 45 mpocurryvald ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( curry tpos 𝑉 ‘ 𝑛 ) = ( 𝑢 ∈ ( 1 ... 6 ) ↦ ⦋ 𝑛 / 𝑣 ⦌ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
47 csbfv ⊢ ⦋ 𝑛 / 𝑣 ⦌ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑛 )
48 47 mpteq2i ⊢ ( 𝑢 ∈ ( 1 ... 6 ) ↦ ⦋ 𝑛 / 𝑣 ⦌ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑣 ) ) = ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑛 ) )
49 46 48 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( curry tpos 𝑉 ‘ 𝑛 ) = ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑛 ) ) )
50 2fveq3 ⊢ ( 𝑢 = 𝑖 → ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) = ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) )
51 50 fveq1d ⊢ ( 𝑢 = 𝑖 → ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) )
52 51 cbvmptv ⊢ ( 𝑢 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑢 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) )
53 49 52 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( curry tpos 𝑉 ‘ 𝑛 ) = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) )
54 5 37 38 38 39 40 53 offval ⊢ ( 𝜑 → ( 𝐾 ∘f ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) curry tpos 𝑉 ) = ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) ) ) )
55 eqid ⊢ ( ℝfld freeLMod ( 1 ... 6 ) ) = ( ℝfld freeLMod ( 1 ... 6 ) )
56 eqid ⊢ ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) = ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
57 rebase ⊢ ℝ = ( Base ‘ ℝfld )
58 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 𝑛 ) ∈ ℝ )
59 refld ⊢ ℝfld ∈ Field
60 59 elexi ⊢ ℝfld ∈ V
61 fzfi ⊢ ( 1 ... 6 ) ∈ Fin
62 55 57 frlmfibas ⊢ ( ( ℝfld ∈ V ∧ ( 1 ... 6 ) ∈ Fin ) → ( ℝ ↑m ( 1 ... 6 ) ) = ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
63 60 61 62 mp2an ⊢ ( ℝ ↑m ( 1 ... 6 ) ) = ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
64 63 a1i ⊢ ( 𝜑 → ( ℝ ↑m ( 1 ... 6 ) ) = ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
65 64 36 feq3dd ⊢ ( 𝜑 → curry tpos 𝑉 : ( 1 ... 6 ) ⟶ ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
66 65 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( curry tpos 𝑉 ‘ 𝑛 ) ∈ ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
67 53 66 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) ∈ ( Base ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
68 eqid ⊢ ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) = ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
69 remulr ⊢ · = ( .r ‘ ℝfld )
70 55 56 57 44 58 67 68 69 frlmvscafval ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 𝑛 ) ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) ) = ( ( ( 1 ... 6 ) × { ( 𝐾 ‘ 𝑛 ) } ) ∘f · ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) ) )
71 70 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( ( 1 ... 6 ) × { ( 𝐾 ‘ 𝑛 ) } ) ∘f · ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) ) ) )
72 fvexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 𝑛 ) ∈ V )
73 fnconstg ⊢ ( ( 𝐾 ‘ 𝑛 ) ∈ V → ( ( 1 ... 6 ) × { ( 𝐾 ‘ 𝑛 ) } ) Fn ( 1 ... 6 ) )
74 72 73 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( ( 1 ... 6 ) × { ( 𝐾 ‘ 𝑛 ) } ) Fn ( 1 ... 6 ) )
75 fvex ⊢ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ∈ V
76 eqid ⊢ ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) )
77 75 76 fnmpti ⊢ ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) Fn ( 1 ... 6 )
78 77 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) Fn ( 1 ... 6 ) )
79 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → 𝑚 ∈ ( 1 ... 6 ) )
80 fvex ⊢ ( 𝐾 ‘ 𝑛 ) ∈ V
81 80 fvconst2 ⊢ ( 𝑚 ∈ ( 1 ... 6 ) → ( ( ( 1 ... 6 ) × { ( 𝐾 ‘ 𝑛 ) } ) ‘ 𝑚 ) = ( 𝐾 ‘ 𝑛 ) )
82 79 81 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ( ( 1 ... 6 ) × { ( 𝐾 ‘ 𝑛 ) } ) ‘ 𝑚 ) = ( 𝐾 ‘ 𝑛 ) )
83 2fveq3 ⊢ ( 𝑖 = 𝑚 → ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) = ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) )
84 83 fveq1d ⊢ ( 𝑖 = 𝑚 → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) )
85 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 6 ) ) → 𝑚 ∈ ( 1 ... 6 ) )
86 fvexd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ∈ V )
87 76 84 85 86 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) ‘ 𝑚 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) )
88 87 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) ‘ 𝑚 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) )
89 74 78 44 44 39 82 88 offval ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( ( ( 1 ... 6 ) × { ( 𝐾 ‘ 𝑛 ) } ) ∘f · ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) ) = ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) )
90 89 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( ( 1 ... 6 ) × { ( 𝐾 ‘ 𝑛 ) } ) ∘f · ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ) )
91 54 71 90 3eqtrd ⊢ ( 𝜑 → ( 𝐾 ∘f ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) curry tpos 𝑉 ) = ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ) )
92 91 oveq2d ⊢ ( 𝜑 → ( ( ℝfld freeLMod ( 1 ... 6 ) ) Σg ( 𝐾 ∘f ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) curry tpos 𝑉 ) ) = ( ( ℝfld freeLMod ( 1 ... 6 ) ) Σg ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ) ) )
93 eqid ⊢ ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) = ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
94 isfld ⊢ ( ℝfld ∈ Field ↔ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) )
95 59 94 mpbi ⊢ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing )
96 95 simpli ⊢ ℝfld ∈ DivRing
97 drngring ⊢ ( ℝfld ∈ DivRing → ℝfld ∈ Ring )
98 96 97 ax-mp ⊢ ℝfld ∈ Ring
99 98 a1i ⊢ ( 𝜑 → ℝfld ∈ Ring )
100 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( 𝐾 ‘ 𝑛 ) ∈ ℝ )
101 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → 𝜑 )
102 101 2 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → 𝐴 : ( 1 ... 6 ) ⟶ ( ℝ ↑m ( 1 ... 3 ) ) )
103 102 79 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( 𝐴 ‘ 𝑚 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
104 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → 𝑛 ∈ ( 1 ... 6 ) )
105 veronesefvcl ⊢ ( ( ( 𝐴 ‘ 𝑚 ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ∈ ℝ )
106 103 104 105 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ∈ ℝ )
107 100 106 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ∈ ℝ )
108 107 fmpttd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) : ( 1 ... 6 ) ⟶ ℝ )
109 33 20 elmap ⊢ ( ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ∈ ( ℝ ↑m ( 1 ... 6 ) ) ↔ ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) : ( 1 ... 6 ) ⟶ ℝ )
110 108 109 sylibr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ∈ ( ℝ ↑m ( 1 ... 6 ) ) )
111 eqid ⊢ ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) )
112 61 a1i ⊢ ( 𝜑 → ( 1 ... 6 ) ∈ Fin )
113 fvexd ⊢ ( 𝜑 → ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) ∈ V )
114 111 112 110 113 fsuppmptdm ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ) finSupp ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
115 55 63 93 38 38 99 110 114 frlmgsum ⊢ ( 𝜑 → ( ( ℝfld freeLMod ( 1 ... 6 ) ) Σg ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ) ) = ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ℝfld Σg ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ) ) )
116 1 2 veronesematrowd ⊢ ( 𝜑 → curry 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ) )
117 101 116 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → curry 𝑉 = ( 𝑖 ∈ ( 1 ... 6 ) ↦ ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ) )
118 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ∈ V )
119 83 117 79 118 fvmptd4 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( curry 𝑉 ‘ 𝑚 ) = ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) )
120 119 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ( curry 𝑉 ‘ 𝑚 ) ‘ 𝑛 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) )
121 120 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) = ( ( curry 𝑉 ‘ 𝑚 ) ‘ 𝑛 ) )
122 121 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 6 ) ) ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) = ( ( 𝐾 ‘ 𝑛 ) · ( ( curry 𝑉 ‘ 𝑚 ) ‘ 𝑛 ) ) )
123 122 an32s ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 6 ) ) ∧ 𝑛 ∈ ( 1 ... 6 ) ) → ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) = ( ( 𝐾 ‘ 𝑛 ) · ( ( curry 𝑉 ‘ 𝑚 ) ‘ 𝑛 ) ) )
124 123 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( curry 𝑉 ‘ 𝑚 ) ‘ 𝑛 ) ) ) )
125 124 oveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ℝfld Σg ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ) = ( ℝfld Σg ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( curry 𝑉 ‘ 𝑚 ) ‘ 𝑛 ) ) ) ) )
126 83 fveq1d ⊢ ( 𝑖 = 𝑚 → ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑗 ) )
127 fveq2 ⊢ ( 𝑗 = 𝑛 → ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑗 ) = ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) )
128 126 127 cbvmpov ⊢ ( 𝑖 ∈ ( 1 ... 6 ) , 𝑗 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑖 ) ) ‘ 𝑗 ) ) = ( 𝑚 ∈ ( 1 ... 6 ) , 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) )
129 1 128 eqtri ⊢ 𝑉 = ( 𝑚 ∈ ( 1 ... 6 ) , 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) )
130 fveq2 ⊢ ( 𝑖 = 𝑚 → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑚 ) )
131 130 fveq1d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) = ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) )
132 131 oveq1d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) = ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ↑ 2 ) )
133 132 oveq2d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) = ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ↑ 2 ) ) )
134 130 fveq1d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) = ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) )
135 134 oveq1d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) = ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ↑ 2 ) )
136 135 oveq2d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) = ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ↑ 2 ) ) )
137 133 136 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) = ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ↑ 2 ) ) ) )
138 130 fveq1d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) = ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) )
139 138 oveq1d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) = ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ↑ 2 ) )
140 139 oveq2d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) = ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ↑ 2 ) ) )
141 137 140 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) = ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ↑ 2 ) ) ) )
142 131 134 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) = ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ) )
143 142 oveq2d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) = ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ) ) )
144 134 138 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) = ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ) )
145 144 oveq2d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) = ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ) ) )
146 143 145 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) = ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ) ) ) )
147 138 131 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) = ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ) )
148 147 oveq2d ⊢ ( 𝑖 = 𝑚 → ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) = ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ) ) )
149 146 148 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) = ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ) ) ) )
150 141 149 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) = ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ) ) ) ) )
151 150 eqeq1d ⊢ ( 𝑖 = 𝑚 → ( ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) = 0 ↔ ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ) ) ) ) = 0 ) )
152 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... 6 ) ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) = 0 )
153 152 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ∀ 𝑖 ∈ ( 1 ... 6 ) ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑖 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑖 ) ‘ 1 ) ) ) ) ) = 0 )
154 151 153 85 rspcdva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ( ( ( ( 𝐾 ‘ 1 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ↑ 2 ) ) + ( ( 𝐾 ‘ 2 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ↑ 2 ) ) ) + ( ( 𝐾 ‘ 3 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ↑ 2 ) ) ) + ( ( ( ( 𝐾 ‘ 4 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) ) ) + ( ( 𝐾 ‘ 5 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 2 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) ) ) ) + ( ( 𝐾 ‘ 6 ) · ( ( ( 𝐴 ‘ 𝑚 ) ‘ 3 ) · ( ( 𝐴 ‘ 𝑚 ) ‘ 1 ) ) ) ) ) = 0 )
155 129 2 3 154 veroquadgsumlem ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ℝfld Σg ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( curry 𝑉 ‘ 𝑚 ) ‘ 𝑛 ) ) ) ) = 0 )
156 125 155 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 6 ) ) → ( ℝfld Σg ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ) = 0 )
157 156 mpteq2dva ⊢ ( 𝜑 → ( 𝑚 ∈ ( 1 ... 6 ) ↦ ( ℝfld Σg ( 𝑛 ∈ ( 1 ... 6 ) ↦ ( ( 𝐾 ‘ 𝑛 ) · ( ( veronese ‘ ( 𝐴 ‘ 𝑚 ) ) ‘ 𝑛 ) ) ) ) ) = ( 𝑚 ∈ ( 1 ... 6 ) ↦ 0 ) )
158 92 115 157 3eqtrd ⊢ ( 𝜑 → ( ( ℝfld freeLMod ( 1 ... 6 ) ) Σg ( 𝐾 ∘f ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) curry tpos 𝑉 ) ) = ( 𝑚 ∈ ( 1 ... 6 ) ↦ 0 ) )
159 fconstmpt ⊢ ( ( 1 ... 6 ) × { 0 } ) = ( 𝑚 ∈ ( 1 ... 6 ) ↦ 0 )
160 re0g ⊢ 0 = ( 0g ‘ ℝfld )
161 55 160 frlm0 ⊢ ( ( ℝfld ∈ Ring ∧ ( 1 ... 6 ) ∈ V ) → ( ( 1 ... 6 ) × { 0 } ) = ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )
162 98 20 161 mp2an ⊢ ( ( 1 ... 6 ) × { 0 } ) = ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
163 159 162 eqtr3i ⊢ ( 𝑚 ∈ ( 1 ... 6 ) ↦ 0 ) = ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) )
164 158 163 eqtrdi ⊢ ( 𝜑 → ( ( ℝfld freeLMod ( 1 ... 6 ) ) Σg ( 𝐾 ∘f ( ·𝑠 ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) curry tpos 𝑉 ) ) = ( 0g ‘ ( ℝfld freeLMod ( 1 ... 6 ) ) ) )