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 
|- 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 )
Assertion veroquadmodzerod 
|- ( ph -> ( ( RRfld freeLMod ( 1 ... 6 ) ) gsum ( K oF ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) curry tpos V ) ) = ( 0g ` ( 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 3 ffnd 
 |-  ( ph -> K Fn ( 1 ... 6 ) )
6 2fveq3 
 |-  ( i = u -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` u ) ) )
7 6 fveq1d 
 |-  ( i = u -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` j ) )
8 fveq2 
 |-  ( j = v -> ( ( veronese ` ( A ` u ) ) ` j ) = ( ( veronese ` ( A ` u ) ) ` v ) )
9 7 8 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 ) )
10 1 9 eqtri 
 |-  V = ( u e. ( 1 ... 6 ) , v e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
11 10 tposmpo 
 |-  tpos V = ( v e. ( 1 ... 6 ) , u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) )
12 11 a1i 
 |-  ( ph -> tpos V = ( v e. ( 1 ... 6 ) , u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` v ) ) )
13 2 adantr 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
14 simprr 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> u e. ( 1 ... 6 ) )
15 13 14 ffvelcdmd 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) )
16 simprl 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> v e. ( 1 ... 6 ) )
17 veronesefvcl 
 |-  ( ( ( A ` u ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
18 15 16 17 syl2anc 
 |-  ( ( ph /\ ( v e. ( 1 ... 6 ) /\ u e. ( 1 ... 6 ) ) ) -> ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
19 12 18 fmpod 
 |-  ( ph -> tpos V : ( ( 1 ... 6 ) X. ( 1 ... 6 ) ) --> RR )
20 ovex 
 |-  ( 1 ... 6 ) e. _V
21 1nn 
 |-  1 e. NN
22 6nn 
 |-  6 e. NN
23 1re 
 |-  1 e. RR
24 6re 
 |-  6 e. RR
25 1lt6 
 |-  1 < 6
26 23 24 25 ltleii 
 |-  1 <_ 6
27 elfz1b 
 |-  ( 1 e. ( 1 ... 6 ) <-> ( 1 e. NN /\ 6 e. NN /\ 1 <_ 6 ) )
28 21 22 26 27 mpbir3an 
 |-  1 e. ( 1 ... 6 )
29 28 ne0ii 
 |-  ( 1 ... 6 ) =/= (/)
30 eldifsn 
 |-  ( ( 1 ... 6 ) e. ( _V \ { (/) } ) <-> ( ( 1 ... 6 ) e. _V /\ ( 1 ... 6 ) =/= (/) ) )
31 20 29 30 mpbir2an 
 |-  ( 1 ... 6 ) e. ( _V \ { (/) } )
32 31 a1i 
 |-  ( ph -> ( 1 ... 6 ) e. ( _V \ { (/) } ) )
33 reex 
 |-  RR e. _V
34 33 a1i 
 |-  ( ph -> RR e. _V )
35 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 ) ) )
36 19 32 34 35 syl3anc 
 |-  ( ph -> curry tpos V : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 6 ) ) )
37 36 ffnd 
 |-  ( ph -> curry tpos V Fn ( 1 ... 6 ) )
38 20 a1i 
 |-  ( ph -> ( 1 ... 6 ) e. _V )
39 inidm 
 |-  ( ( 1 ... 6 ) i^i ( 1 ... 6 ) ) = ( 1 ... 6 )
40 eqidd 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( K ` n ) = ( K ` n ) )
41 18 ralrimivva 
 |-  ( ph -> A. v e. ( 1 ... 6 ) A. u e. ( 1 ... 6 ) ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
42 41 adantr 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> A. v e. ( 1 ... 6 ) A. u e. ( 1 ... 6 ) ( ( veronese ` ( A ` u ) ) ` v ) e. RR )
43 29 a1i 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( 1 ... 6 ) =/= (/) )
44 20 a1i 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( 1 ... 6 ) e. _V )
45 simpr 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> n e. ( 1 ... 6 ) )
46 11 42 43 44 45 mpocurryvald 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( curry tpos V ` n ) = ( u e. ( 1 ... 6 ) |-> [_ n / v ]_ ( ( veronese ` ( A ` u ) ) ` v ) ) )
47 csbfv 
 |-  [_ n / v ]_ ( ( veronese ` ( A ` u ) ) ` v ) = ( ( veronese ` ( A ` u ) ) ` n )
48 47 mpteq2i 
 |-  ( u e. ( 1 ... 6 ) |-> [_ n / v ]_ ( ( veronese ` ( A ` u ) ) ` v ) ) = ( u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` n ) )
49 46 48 eqtrdi 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( curry tpos V ` n ) = ( u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` n ) ) )
50 2fveq3 
 |-  ( u = i -> ( veronese ` ( A ` u ) ) = ( veronese ` ( A ` i ) ) )
51 50 fveq1d 
 |-  ( u = i -> ( ( veronese ` ( A ` u ) ) ` n ) = ( ( veronese ` ( A ` i ) ) ` n ) )
52 51 cbvmptv 
 |-  ( u e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` u ) ) ` n ) ) = ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) )
53 49 52 eqtrdi 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( curry tpos V ` n ) = ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) )
54 5 37 38 38 39 40 53 offval 
 |-  ( ph -> ( K oF ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) curry tpos V ) = ( n e. ( 1 ... 6 ) |-> ( ( K ` n ) ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) ) ) )
55 eqid 
 |-  ( RRfld freeLMod ( 1 ... 6 ) ) = ( RRfld freeLMod ( 1 ... 6 ) )
56 eqid 
 |-  ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) = ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) )
57 rebase 
 |-  RR = ( Base ` RRfld )
58 3 ffvelcdmda 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( K ` n ) e. RR )
59 refld 
 |-  RRfld e. Field
60 59 elexi 
 |-  RRfld e. _V
61 fzfi 
 |-  ( 1 ... 6 ) e. Fin
62 55 57 frlmfibas 
 |-  ( ( RRfld e. _V /\ ( 1 ... 6 ) e. Fin ) -> ( RR ^m ( 1 ... 6 ) ) = ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
63 60 61 62 mp2an 
 |-  ( RR ^m ( 1 ... 6 ) ) = ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) )
64 63 a1i 
 |-  ( ph -> ( RR ^m ( 1 ... 6 ) ) = ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
65 64 36 feq3dd 
 |-  ( ph -> curry tpos V : ( 1 ... 6 ) --> ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
66 65 ffvelcdmda 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( curry tpos V ` n ) e. ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
67 53 66 eqeltrrd 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) e. ( Base ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
68 eqid 
 |-  ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) = ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) )
69 remulr 
 |-  x. = ( .r ` RRfld )
70 55 56 57 44 58 67 68 69 frlmvscafval 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( ( K ` n ) ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) ) = ( ( ( 1 ... 6 ) X. { ( K ` n ) } ) oF x. ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) ) )
71 70 mpteq2dva 
 |-  ( ph -> ( n e. ( 1 ... 6 ) |-> ( ( K ` n ) ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) ) ) = ( n e. ( 1 ... 6 ) |-> ( ( ( 1 ... 6 ) X. { ( K ` n ) } ) oF x. ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) ) ) )
72 fvexd 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( K ` n ) e. _V )
73 fnconstg 
 |-  ( ( K ` n ) e. _V -> ( ( 1 ... 6 ) X. { ( K ` n ) } ) Fn ( 1 ... 6 ) )
74 72 73 syl 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( ( 1 ... 6 ) X. { ( K ` n ) } ) Fn ( 1 ... 6 ) )
75 fvex 
 |-  ( ( veronese ` ( A ` i ) ) ` n ) e. _V
76 eqid 
 |-  ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) = ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) )
77 75 76 fnmpti 
 |-  ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) Fn ( 1 ... 6 )
78 77 a1i 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) Fn ( 1 ... 6 ) )
79 simpr 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> m e. ( 1 ... 6 ) )
80 fvex 
 |-  ( K ` n ) e. _V
81 80 fvconst2 
 |-  ( m e. ( 1 ... 6 ) -> ( ( ( 1 ... 6 ) X. { ( K ` n ) } ) ` m ) = ( K ` n ) )
82 79 81 syl 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( ( ( 1 ... 6 ) X. { ( K ` n ) } ) ` m ) = ( K ` n ) )
83 2fveq3 
 |-  ( i = m -> ( veronese ` ( A ` i ) ) = ( veronese ` ( A ` m ) ) )
84 83 fveq1d 
 |-  ( i = m -> ( ( veronese ` ( A ` i ) ) ` n ) = ( ( veronese ` ( A ` m ) ) ` n ) )
85 simpr 
 |-  ( ( ph /\ m e. ( 1 ... 6 ) ) -> m e. ( 1 ... 6 ) )
86 fvexd 
 |-  ( ( ph /\ m e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` m ) ) ` n ) e. _V )
87 76 84 85 86 fvmptd3 
 |-  ( ( ph /\ m e. ( 1 ... 6 ) ) -> ( ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) ` m ) = ( ( veronese ` ( A ` m ) ) ` n ) )
88 87 adantlr 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) ` m ) = ( ( veronese ` ( A ` m ) ) ` n ) )
89 74 78 44 44 39 82 88 offval 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( ( ( 1 ... 6 ) X. { ( K ` n ) } ) oF x. ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) ) = ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) )
90 89 mpteq2dva 
 |-  ( ph -> ( n e. ( 1 ... 6 ) |-> ( ( ( 1 ... 6 ) X. { ( K ` n ) } ) oF x. ( i e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` n ) ) ) ) = ( n e. ( 1 ... 6 ) |-> ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) ) )
91 54 71 90 3eqtrd 
 |-  ( ph -> ( K oF ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) curry tpos V ) = ( n e. ( 1 ... 6 ) |-> ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) ) )
92 91 oveq2d 
 |-  ( ph -> ( ( RRfld freeLMod ( 1 ... 6 ) ) gsum ( K oF ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) curry tpos V ) ) = ( ( RRfld freeLMod ( 1 ... 6 ) ) gsum ( n e. ( 1 ... 6 ) |-> ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) ) ) )
93 eqid 
 |-  ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) ) = ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) )
94 isfld 
 |-  ( RRfld e. Field <-> ( RRfld e. DivRing /\ RRfld e. CRing ) )
95 59 94 mpbi 
 |-  ( RRfld e. DivRing /\ RRfld e. CRing )
96 95 simpli 
 |-  RRfld e. DivRing
97 drngring 
 |-  ( RRfld e. DivRing -> RRfld e. Ring )
98 96 97 ax-mp 
 |-  RRfld e. Ring
99 98 a1i 
 |-  ( ph -> RRfld e. Ring )
100 58 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( K ` n ) e. RR )
101 simpll 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ph )
102 101 2 syl 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
103 102 79 ffvelcdmd 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( A ` m ) e. ( RR ^m ( 1 ... 3 ) ) )
104 simplr 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> n e. ( 1 ... 6 ) )
105 veronesefvcl 
 |-  ( ( ( A ` m ) e. ( RR ^m ( 1 ... 3 ) ) /\ n e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` m ) ) ` n ) e. RR )
106 103 104 105 syl2anc 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` m ) ) ` n ) e. RR )
107 100 106 remulcld 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) e. RR )
108 107 fmpttd 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) : ( 1 ... 6 ) --> RR )
109 33 20 elmap 
 |-  ( ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) e. ( RR ^m ( 1 ... 6 ) ) <-> ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) : ( 1 ... 6 ) --> RR )
110 108 109 sylibr 
 |-  ( ( ph /\ n e. ( 1 ... 6 ) ) -> ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) e. ( RR ^m ( 1 ... 6 ) ) )
111 eqid 
 |-  ( n e. ( 1 ... 6 ) |-> ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) ) = ( n e. ( 1 ... 6 ) |-> ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) )
112 61 a1i 
 |-  ( ph -> ( 1 ... 6 ) e. Fin )
113 fvexd 
 |-  ( ph -> ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) ) e. _V )
114 111 112 110 113 fsuppmptdm 
 |-  ( ph -> ( n e. ( 1 ... 6 ) |-> ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) ) finSupp ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
115 55 63 93 38 38 99 110 114 frlmgsum 
 |-  ( ph -> ( ( RRfld freeLMod ( 1 ... 6 ) ) gsum ( n e. ( 1 ... 6 ) |-> ( m e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) ) ) = ( m e. ( 1 ... 6 ) |-> ( RRfld gsum ( n e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) ) ) )
116 1 2 veronesematrowd 
 |-  ( ph -> curry V = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) )
117 101 116 syl 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> curry V = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) )
118 fvexd 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( veronese ` ( A ` m ) ) e. _V )
119 83 117 79 118 fvmptd4 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( curry V ` m ) = ( veronese ` ( A ` m ) ) )
120 119 fveq1d 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( ( curry V ` m ) ` n ) = ( ( veronese ` ( A ` m ) ) ` n ) )
121 120 eqcomd 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` m ) ) ` n ) = ( ( curry V ` m ) ` n ) )
122 121 oveq2d 
 |-  ( ( ( ph /\ n e. ( 1 ... 6 ) ) /\ m e. ( 1 ... 6 ) ) -> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) = ( ( K ` n ) x. ( ( curry V ` m ) ` n ) ) )
123 122 an32s 
 |-  ( ( ( ph /\ m e. ( 1 ... 6 ) ) /\ n e. ( 1 ... 6 ) ) -> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) = ( ( K ` n ) x. ( ( curry V ` m ) ` n ) ) )
124 123 mpteq2dva 
 |-  ( ( ph /\ m e. ( 1 ... 6 ) ) -> ( n e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) = ( n e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( curry V ` m ) ` n ) ) ) )
125 124 oveq2d 
 |-  ( ( ph /\ m e. ( 1 ... 6 ) ) -> ( RRfld gsum ( n e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) ) = ( RRfld gsum ( n e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( curry V ` m ) ` n ) ) ) ) )
126 83 fveq1d 
 |-  ( i = m -> ( ( veronese ` ( A ` i ) ) ` j ) = ( ( veronese ` ( A ` m ) ) ` j ) )
127 fveq2 
 |-  ( j = n -> ( ( veronese ` ( A ` m ) ) ` j ) = ( ( veronese ` ( A ` m ) ) ` n ) )
128 126 127 cbvmpov 
 |-  ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) = ( m e. ( 1 ... 6 ) , n e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` m ) ) ` n ) )
129 1 128 eqtri 
 |-  V = ( m e. ( 1 ... 6 ) , n e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` m ) ) ` n ) )
130 fveq2 
 |-  ( i = m -> ( A ` i ) = ( A ` m ) )
131 130 fveq1d 
 |-  ( i = m -> ( ( A ` i ) ` 1 ) = ( ( A ` m ) ` 1 ) )
132 131 oveq1d 
 |-  ( i = m -> ( ( ( A ` i ) ` 1 ) ^ 2 ) = ( ( ( A ` m ) ` 1 ) ^ 2 ) )
133 132 oveq2d 
 |-  ( i = m -> ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) = ( ( K ` 1 ) x. ( ( ( A ` m ) ` 1 ) ^ 2 ) ) )
134 130 fveq1d 
 |-  ( i = m -> ( ( A ` i ) ` 2 ) = ( ( A ` m ) ` 2 ) )
135 134 oveq1d 
 |-  ( i = m -> ( ( ( A ` i ) ` 2 ) ^ 2 ) = ( ( ( A ` m ) ` 2 ) ^ 2 ) )
136 135 oveq2d 
 |-  ( i = m -> ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) = ( ( K ` 2 ) x. ( ( ( A ` m ) ` 2 ) ^ 2 ) ) )
137 133 136 oveq12d 
 |-  ( i = m -> ( ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) ) = ( ( ( K ` 1 ) x. ( ( ( A ` m ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` m ) ` 2 ) ^ 2 ) ) ) )
138 130 fveq1d 
 |-  ( i = m -> ( ( A ` i ) ` 3 ) = ( ( A ` m ) ` 3 ) )
139 138 oveq1d 
 |-  ( i = m -> ( ( ( A ` i ) ` 3 ) ^ 2 ) = ( ( ( A ` m ) ` 3 ) ^ 2 ) )
140 139 oveq2d 
 |-  ( i = m -> ( ( K ` 3 ) x. ( ( ( A ` i ) ` 3 ) ^ 2 ) ) = ( ( K ` 3 ) x. ( ( ( A ` m ) ` 3 ) ^ 2 ) ) )
141 137 140 oveq12d 
 |-  ( i = m -> ( ( ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) ) + ( ( K ` 3 ) x. ( ( ( A ` i ) ` 3 ) ^ 2 ) ) ) = ( ( ( ( K ` 1 ) x. ( ( ( A ` m ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` m ) ` 2 ) ^ 2 ) ) ) + ( ( K ` 3 ) x. ( ( ( A ` m ) ` 3 ) ^ 2 ) ) ) )
142 131 134 oveq12d 
 |-  ( i = m -> ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) = ( ( ( A ` m ) ` 1 ) x. ( ( A ` m ) ` 2 ) ) )
143 142 oveq2d 
 |-  ( i = m -> ( ( K ` 4 ) x. ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) ) = ( ( K ` 4 ) x. ( ( ( A ` m ) ` 1 ) x. ( ( A ` m ) ` 2 ) ) ) )
144 134 138 oveq12d 
 |-  ( i = m -> ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) = ( ( ( A ` m ) ` 2 ) x. ( ( A ` m ) ` 3 ) ) )
145 144 oveq2d 
 |-  ( i = m -> ( ( K ` 5 ) x. ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) ) = ( ( K ` 5 ) x. ( ( ( A ` m ) ` 2 ) x. ( ( A ` m ) ` 3 ) ) ) )
146 143 145 oveq12d 
 |-  ( i = m -> ( ( ( K ` 4 ) x. ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) ) + ( ( K ` 5 ) x. ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) ) ) = ( ( ( K ` 4 ) x. ( ( ( A ` m ) ` 1 ) x. ( ( A ` m ) ` 2 ) ) ) + ( ( K ` 5 ) x. ( ( ( A ` m ) ` 2 ) x. ( ( A ` m ) ` 3 ) ) ) ) )
147 138 131 oveq12d 
 |-  ( i = m -> ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) = ( ( ( A ` m ) ` 3 ) x. ( ( A ` m ) ` 1 ) ) )
148 147 oveq2d 
 |-  ( i = m -> ( ( K ` 6 ) x. ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) = ( ( K ` 6 ) x. ( ( ( A ` m ) ` 3 ) x. ( ( A ` m ) ` 1 ) ) ) )
149 146 148 oveq12d 
 |-  ( i = m -> ( ( ( ( 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 ) ) ) ) = ( ( ( ( K ` 4 ) x. ( ( ( A ` m ) ` 1 ) x. ( ( A ` m ) ` 2 ) ) ) + ( ( K ` 5 ) x. ( ( ( A ` m ) ` 2 ) x. ( ( A ` m ) ` 3 ) ) ) ) + ( ( K ` 6 ) x. ( ( ( A ` m ) ` 3 ) x. ( ( A ` m ) ` 1 ) ) ) ) )
150 141 149 oveq12d 
 |-  ( i = m -> ( ( ( ( ( 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 ) ) ) ) ) = ( ( ( ( ( K ` 1 ) x. ( ( ( A ` m ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` m ) ` 2 ) ^ 2 ) ) ) + ( ( K ` 3 ) x. ( ( ( A ` m ) ` 3 ) ^ 2 ) ) ) + ( ( ( ( K ` 4 ) x. ( ( ( A ` m ) ` 1 ) x. ( ( A ` m ) ` 2 ) ) ) + ( ( K ` 5 ) x. ( ( ( A ` m ) ` 2 ) x. ( ( A ` m ) ` 3 ) ) ) ) + ( ( K ` 6 ) x. ( ( ( A ` m ) ` 3 ) x. ( ( A ` m ) ` 1 ) ) ) ) ) )
151 150 eqeq1d 
 |-  ( i = m -> ( ( ( ( ( ( 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 <-> ( ( ( ( ( K ` 1 ) x. ( ( ( A ` m ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` m ) ` 2 ) ^ 2 ) ) ) + ( ( K ` 3 ) x. ( ( ( A ` m ) ` 3 ) ^ 2 ) ) ) + ( ( ( ( K ` 4 ) x. ( ( ( A ` m ) ` 1 ) x. ( ( A ` m ) ` 2 ) ) ) + ( ( K ` 5 ) x. ( ( ( A ` m ) ` 2 ) x. ( ( A ` m ) ` 3 ) ) ) ) + ( ( K ` 6 ) x. ( ( ( A ` m ) ` 3 ) x. ( ( A ` m ) ` 1 ) ) ) ) ) = 0 ) )
152 4 ralrimiva 
 |-  ( ph -> A. 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 )
153 152 adantr 
 |-  ( ( ph /\ m e. ( 1 ... 6 ) ) -> A. 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 )
154 151 153 85 rspcdva 
 |-  ( ( ph /\ m e. ( 1 ... 6 ) ) -> ( ( ( ( ( K ` 1 ) x. ( ( ( A ` m ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` m ) ` 2 ) ^ 2 ) ) ) + ( ( K ` 3 ) x. ( ( ( A ` m ) ` 3 ) ^ 2 ) ) ) + ( ( ( ( K ` 4 ) x. ( ( ( A ` m ) ` 1 ) x. ( ( A ` m ) ` 2 ) ) ) + ( ( K ` 5 ) x. ( ( ( A ` m ) ` 2 ) x. ( ( A ` m ) ` 3 ) ) ) ) + ( ( K ` 6 ) x. ( ( ( A ` m ) ` 3 ) x. ( ( A ` m ) ` 1 ) ) ) ) ) = 0 )
155 129 2 3 154 veroquadgsumlem 
 |-  ( ( ph /\ m e. ( 1 ... 6 ) ) -> ( RRfld gsum ( n e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( curry V ` m ) ` n ) ) ) ) = 0 )
156 125 155 eqtrd 
 |-  ( ( ph /\ m e. ( 1 ... 6 ) ) -> ( RRfld gsum ( n e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) ) = 0 )
157 156 mpteq2dva 
 |-  ( ph -> ( m e. ( 1 ... 6 ) |-> ( RRfld gsum ( n e. ( 1 ... 6 ) |-> ( ( K ` n ) x. ( ( veronese ` ( A ` m ) ) ` n ) ) ) ) ) = ( m e. ( 1 ... 6 ) |-> 0 ) )
158 92 115 157 3eqtrd 
 |-  ( ph -> ( ( RRfld freeLMod ( 1 ... 6 ) ) gsum ( K oF ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) curry tpos V ) ) = ( m e. ( 1 ... 6 ) |-> 0 ) )
159 fconstmpt 
 |-  ( ( 1 ... 6 ) X. { 0 } ) = ( m e. ( 1 ... 6 ) |-> 0 )
160 re0g 
 |-  0 = ( 0g ` RRfld )
161 55 160 frlm0 
 |-  ( ( RRfld e. Ring /\ ( 1 ... 6 ) e. _V ) -> ( ( 1 ... 6 ) X. { 0 } ) = ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )
162 98 20 161 mp2an 
 |-  ( ( 1 ... 6 ) X. { 0 } ) = ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) )
163 159 162 eqtr3i 
 |-  ( m e. ( 1 ... 6 ) |-> 0 ) = ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) )
164 158 163 eqtrdi 
 |-  ( ph -> ( ( RRfld freeLMod ( 1 ... 6 ) ) gsum ( K oF ( .s ` ( RRfld freeLMod ( 1 ... 6 ) ) ) curry tpos V ) ) = ( 0g ` ( RRfld freeLMod ( 1 ... 6 ) ) ) )