Theorem veroquadgsumlem

Description: Lemma for veroquadmodzerod . Express the common homogeneous quadratic equation in RRfld gsum form using the Veronese matrix V . (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	veroquadgsumlem	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( RRfld gsum ( j e. ( 1 ... 6 ) |-> ( ( K ` j ) x. ( ( curry V ` i ) ` j ) ) ) ) = 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		rebase	|- RR = ( Base ` RRfld )
6		replusg	|- + = ( +g ` RRfld )
7		refld	|- RRfld e. Field
8	7	elexi	|- RRfld e. _V
9	8	a1i	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> RRfld e. _V )
10		6nn	|- 6 e. NN
11		nnuz	|- NN = ( ZZ>= ` 1 )
12	10 11	eleqtri	|- 6 e. ( ZZ>= ` 1 )
13	12	a1i	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> 6 e. ( ZZ>= ` 1 ) )
14	3	ad2antrr	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> K : ( 1 ... 6 ) --> RR )
15		simpr	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> v e. ( 1 ... 6 ) )
16	14 15	ffvelcdmd	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> ( K ` v ) e. RR )
17	1 2	veronesematrowd	|- ( ph -> curry V = ( i e. ( 1 ... 6 ) |-> ( veronese ` ( A ` i ) ) ) )
18		fvexd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( veronese ` ( A ` i ) ) e. _V )
19	17 18	fvmpt2d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( curry V ` i ) = ( veronese ` ( A ` i ) ) )
20	19	adantr	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> ( curry V ` i ) = ( veronese ` ( A ` i ) ) )
21	20	fveq1d	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` v ) = ( ( veronese ` ( A ` i ) ) ` v ) )
22	2	ad2antrr	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> A : ( 1 ... 6 ) --> ( RR ^m ( 1 ... 3 ) ) )
23		simplr	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> i e. ( 1 ... 6 ) )
24	22 23	ffvelcdmd	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> ( A ` i ) e. ( RR ^m ( 1 ... 3 ) ) )
25		veronesefvcl	|- ( ( ( A ` i ) e. ( RR ^m ( 1 ... 3 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` i ) ) ` v ) e. RR )
26	24 25	sylancom	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` i ) ) ` v ) e. RR )
27	21 26	eqeltrd	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` v ) e. RR )
28	16 27	remulcld	|- ( ( ( ph /\ i e. ( 1 ... 6 ) ) /\ v e. ( 1 ... 6 ) ) -> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) e. RR )
29	28	fmpttd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) : ( 1 ... 6 ) --> RR )
30	5 6 9 13 29	gsumval2	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( RRfld gsum ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) = ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 6 ) )
31		5nn	|- 5 e. NN
32	31 11	eleqtri	|- 5 e. ( ZZ>= ` 1 )
33		seqp1	|- ( 5 e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 5 + 1 ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 5 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 5 + 1 ) ) ) )
34	32 33	ax-mp	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 5 + 1 ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 5 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 5 + 1 ) ) )
35		5p1e6	|- ( 5 + 1 ) = 6
36	35	fveq2i	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 5 + 1 ) ) = ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 6 )
37	35	fveq2i	|- ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 5 + 1 ) ) = ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 6 )
38	37	oveq2i	|- ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 5 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 5 + 1 ) ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 5 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 6 ) )
39	34 36 38	3eqtr3i	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 6 ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 5 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 6 ) )
40		4nn	|- 4 e. NN
41	40 11	eleqtri	|- 4 e. ( ZZ>= ` 1 )
42		seqp1	|- ( 4 e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 4 + 1 ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 4 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 4 + 1 ) ) ) )
43	41 42	ax-mp	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 4 + 1 ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 4 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 4 + 1 ) ) )
44		4p1e5	|- ( 4 + 1 ) = 5
45	44	fveq2i	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 4 + 1 ) ) = ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 5 )
46	44	fveq2i	|- ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 4 + 1 ) ) = ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 5 )
47	46	oveq2i	|- ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 4 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 4 + 1 ) ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 4 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 5 ) )
48	43 45 47	3eqtr3i	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 5 ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 4 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 5 ) )
49		3nn	|- 3 e. NN
50	49 11	eleqtri	|- 3 e. ( ZZ>= ` 1 )
51		seqp1	|- ( 3 e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 3 + 1 ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 3 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 3 + 1 ) ) ) )
52	50 51	ax-mp	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 3 + 1 ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 3 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 3 + 1 ) ) )
53		3p1e4	|- ( 3 + 1 ) = 4
54	53	fveq2i	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 3 + 1 ) ) = ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 4 )
55	53	fveq2i	|- ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 3 + 1 ) ) = ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 4 )
56	55	oveq2i	|- ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 3 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 3 + 1 ) ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 3 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 4 ) )
57	52 54 56	3eqtr3i	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 4 ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 3 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 4 ) )
58		2eluzge1	|- 2 e. ( ZZ>= ` 1 )
59		seqp1	|- ( 2 e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 2 + 1 ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 2 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 2 + 1 ) ) ) )
60	58 59	ax-mp	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 2 + 1 ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 2 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 2 + 1 ) ) )
61		2p1e3	|- ( 2 + 1 ) = 3
62	61	fveq2i	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 2 + 1 ) ) = ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 3 )
63	61	fveq2i	|- ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 2 + 1 ) ) = ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 3 )
64	63	oveq2i	|- ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 2 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 2 + 1 ) ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 2 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 3 ) )
65	60 62 64	3eqtr3i	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 3 ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 2 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 3 ) )
66		1nn	|- 1 e. NN
67	66 11	eleqtri	|- 1 e. ( ZZ>= ` 1 )
68		seqp1	|- ( 1 e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 1 + 1 ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 1 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 1 + 1 ) ) ) )
69	67 68	ax-mp	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 1 + 1 ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 1 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 1 + 1 ) ) )
70		1p1e2	|- ( 1 + 1 ) = 2
71	70	fveq2i	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` ( 1 + 1 ) ) = ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 2 )
72	70	fveq2i	|- ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 1 + 1 ) ) = ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 2 )
73	72	oveq2i	|- ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 1 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` ( 1 + 1 ) ) ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 1 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 2 ) )
74	69 71 73	3eqtr3i	|- ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 2 ) = ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 1 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 2 ) )
75		1z	|- 1 e. ZZ
76		eqid	|- ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) = ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) )
77		fveq2	|- ( v = 1 -> ( K ` v ) = ( K ` 1 ) )
78		fveq2	|- ( v = 1 -> ( ( curry V ` i ) ` v ) = ( ( curry V ` i ) ` 1 ) )
79	77 78	oveq12d	|- ( v = 1 -> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) = ( ( K ` 1 ) x. ( ( curry V ` i ) ` 1 ) ) )
80		1re	|- 1 e. RR
81		6re	|- 6 e. RR
82		1lt6	|- 1 < 6
83	80 81 82	ltleii	|- 1 <_ 6
84		elfz1b	|- ( 1 e. ( 1 ... 6 ) <-> ( 1 e. NN /\ 6 e. NN /\ 1 <_ 6 ) )
85	66 10 83 84	mpbir3an	|- 1 e. ( 1 ... 6 )
86	85	a1i	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> 1 e. ( 1 ... 6 ) )
87		ovexd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 1 ) x. ( ( curry V ` i ) ` 1 ) ) e. _V )
88	76 79 86 87	fvmptd3	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 1 ) = ( ( K ` 1 ) x. ( ( curry V ` i ) ` 1 ) ) )
89	19	fveq1d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 1 ) = ( ( veronese ` ( A ` i ) ) ` 1 ) )
90	2	ffvelcdmda	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( A ` i ) e. ( RR ^m ( 1 ... 3 ) ) )
91	90	veronesev1lem	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` i ) ) ` 1 ) = ( ( ( A ` i ) ` 1 ) ^ 2 ) )
92	89 91	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 1 ) = ( ( ( A ` i ) ` 1 ) ^ 2 ) )
93	92	oveq2d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 1 ) x. ( ( curry V ` i ) ` 1 ) ) = ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) )
94	88 93	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 1 ) = ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) )
95	75 94	seq1i	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 1 ) = ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) )
96		fveq2	|- ( v = 2 -> ( K ` v ) = ( K ` 2 ) )
97		fveq2	|- ( v = 2 -> ( ( curry V ` i ) ` v ) = ( ( curry V ` i ) ` 2 ) )
98	96 97	oveq12d	|- ( v = 2 -> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) = ( ( K ` 2 ) x. ( ( curry V ` i ) ` 2 ) ) )
99		2nn	|- 2 e. NN
100		2re	|- 2 e. RR
101		2lt6	|- 2 < 6
102	100 81 101	ltleii	|- 2 <_ 6
103		elfz1b	|- ( 2 e. ( 1 ... 6 ) <-> ( 2 e. NN /\ 6 e. NN /\ 2 <_ 6 ) )
104	99 10 102 103	mpbir3an	|- 2 e. ( 1 ... 6 )
105	104	a1i	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> 2 e. ( 1 ... 6 ) )
106		ovexd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 2 ) x. ( ( curry V ` i ) ` 2 ) ) e. _V )
107	76 98 105 106	fvmptd3	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 2 ) = ( ( K ` 2 ) x. ( ( curry V ` i ) ` 2 ) ) )
108	19	fveq1d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 2 ) = ( ( veronese ` ( A ` i ) ) ` 2 ) )
109	90	veronesev2lem	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` i ) ) ` 2 ) = ( ( ( A ` i ) ` 2 ) ^ 2 ) )
110	108 109	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 2 ) = ( ( ( A ` i ) ` 2 ) ^ 2 ) )
111	110	oveq2d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 2 ) x. ( ( curry V ` i ) ` 2 ) ) = ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) )
112	107 111	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 2 ) = ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) )
113	95 112	oveq12d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 1 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 2 ) ) = ( ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) ) )
114	74 113	eqtrid	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 2 ) = ( ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) ) )
115		fveq2	|- ( v = 3 -> ( K ` v ) = ( K ` 3 ) )
116		fveq2	|- ( v = 3 -> ( ( curry V ` i ) ` v ) = ( ( curry V ` i ) ` 3 ) )
117	115 116	oveq12d	|- ( v = 3 -> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) = ( ( K ` 3 ) x. ( ( curry V ` i ) ` 3 ) ) )
118		3re	|- 3 e. RR
119		3lt6	|- 3 < 6
120	118 81 119	ltleii	|- 3 <_ 6
121		elfz1b	|- ( 3 e. ( 1 ... 6 ) <-> ( 3 e. NN /\ 6 e. NN /\ 3 <_ 6 ) )
122	49 10 120 121	mpbir3an	|- 3 e. ( 1 ... 6 )
123	122	a1i	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> 3 e. ( 1 ... 6 ) )
124		ovexd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 3 ) x. ( ( curry V ` i ) ` 3 ) ) e. _V )
125	76 117 123 124	fvmptd3	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 3 ) = ( ( K ` 3 ) x. ( ( curry V ` i ) ` 3 ) ) )
126	19	fveq1d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 3 ) = ( ( veronese ` ( A ` i ) ) ` 3 ) )
127	90	veronesev3lem	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` i ) ) ` 3 ) = ( ( ( A ` i ) ` 3 ) ^ 2 ) )
128	126 127	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 3 ) = ( ( ( A ` i ) ` 3 ) ^ 2 ) )
129	128	oveq2d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 3 ) x. ( ( curry V ` i ) ` 3 ) ) = ( ( K ` 3 ) x. ( ( ( A ` i ) ` 3 ) ^ 2 ) ) )
130	125 129	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 3 ) = ( ( K ` 3 ) x. ( ( ( A ` i ) ` 3 ) ^ 2 ) ) )
131	114 130	oveq12d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 2 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 3 ) ) = ( ( ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) ) + ( ( K ` 3 ) x. ( ( ( A ` i ) ` 3 ) ^ 2 ) ) ) )
132	65 131	eqtrid	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 3 ) = ( ( ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) ) + ( ( K ` 3 ) x. ( ( ( A ` i ) ` 3 ) ^ 2 ) ) ) )
133		fveq2	|- ( v = 4 -> ( K ` v ) = ( K ` 4 ) )
134		fveq2	|- ( v = 4 -> ( ( curry V ` i ) ` v ) = ( ( curry V ` i ) ` 4 ) )
135	133 134	oveq12d	|- ( v = 4 -> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) = ( ( K ` 4 ) x. ( ( curry V ` i ) ` 4 ) ) )
136		4re	|- 4 e. RR
137		4lt6	|- 4 < 6
138	136 81 137	ltleii	|- 4 <_ 6
139		elfz1b	|- ( 4 e. ( 1 ... 6 ) <-> ( 4 e. NN /\ 6 e. NN /\ 4 <_ 6 ) )
140	40 10 138 139	mpbir3an	|- 4 e. ( 1 ... 6 )
141	140	a1i	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> 4 e. ( 1 ... 6 ) )
142		ovexd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 4 ) x. ( ( curry V ` i ) ` 4 ) ) e. _V )
143	76 135 141 142	fvmptd3	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 4 ) = ( ( K ` 4 ) x. ( ( curry V ` i ) ` 4 ) ) )
144	19	fveq1d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 4 ) = ( ( veronese ` ( A ` i ) ) ` 4 ) )
145	90	veronesev4lem	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` i ) ) ` 4 ) = ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) )
146	144 145	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 4 ) = ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) )
147	146	oveq2d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 4 ) x. ( ( curry V ` i ) ` 4 ) ) = ( ( K ` 4 ) x. ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) ) )
148	143 147	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 4 ) = ( ( K ` 4 ) x. ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) ) )
149	132 148	oveq12d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 3 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 4 ) ) = ( ( ( ( ( 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 ) ) ) ) )
150	57 149	eqtrid	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 4 ) = ( ( ( ( ( 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 ) ) ) ) )
151		fveq2	|- ( v = 5 -> ( K ` v ) = ( K ` 5 ) )
152		fveq2	|- ( v = 5 -> ( ( curry V ` i ) ` v ) = ( ( curry V ` i ) ` 5 ) )
153	151 152	oveq12d	|- ( v = 5 -> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) = ( ( K ` 5 ) x. ( ( curry V ` i ) ` 5 ) ) )
154		5re	|- 5 e. RR
155		5lt6	|- 5 < 6
156	154 81 155	ltleii	|- 5 <_ 6
157		elfz1b	|- ( 5 e. ( 1 ... 6 ) <-> ( 5 e. NN /\ 6 e. NN /\ 5 <_ 6 ) )
158	31 10 156 157	mpbir3an	|- 5 e. ( 1 ... 6 )
159	158	a1i	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> 5 e. ( 1 ... 6 ) )
160		ovexd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 5 ) x. ( ( curry V ` i ) ` 5 ) ) e. _V )
161	76 153 159 160	fvmptd3	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 5 ) = ( ( K ` 5 ) x. ( ( curry V ` i ) ` 5 ) ) )
162	19	fveq1d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 5 ) = ( ( veronese ` ( A ` i ) ) ` 5 ) )
163	90	veronesev5lem	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` i ) ) ` 5 ) = ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) )
164	162 163	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 5 ) = ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) )
165	164	oveq2d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 5 ) x. ( ( curry V ` i ) ` 5 ) ) = ( ( K ` 5 ) x. ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) ) )
166	161 165	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 5 ) = ( ( K ` 5 ) x. ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) ) )
167	150 166	oveq12d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 4 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 5 ) ) = ( ( ( ( ( ( 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 ) ) ) ) )
168	48 167	eqtrid	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 5 ) = ( ( ( ( ( ( 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 ) ) ) ) )
169		fveq2	|- ( v = 6 -> ( K ` v ) = ( K ` 6 ) )
170		fveq2	|- ( v = 6 -> ( ( curry V ` i ) ` v ) = ( ( curry V ` i ) ` 6 ) )
171	169 170	oveq12d	|- ( v = 6 -> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) = ( ( K ` 6 ) x. ( ( curry V ` i ) ` 6 ) ) )
172	81	leidi	|- 6 <_ 6
173		elfz1b	|- ( 6 e. ( 1 ... 6 ) <-> ( 6 e. NN /\ 6 e. NN /\ 6 <_ 6 ) )
174	10 10 172 173	mpbir3an	|- 6 e. ( 1 ... 6 )
175	174	a1i	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> 6 e. ( 1 ... 6 ) )
176		ovexd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 6 ) x. ( ( curry V ` i ) ` 6 ) ) e. _V )
177	76 171 175 176	fvmptd3	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 6 ) = ( ( K ` 6 ) x. ( ( curry V ` i ) ` 6 ) ) )
178	19	fveq1d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 6 ) = ( ( veronese ` ( A ` i ) ) ` 6 ) )
179	90	veronesev6lem	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( veronese ` ( A ` i ) ) ` 6 ) = ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) )
180	178 179	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( curry V ` i ) ` 6 ) = ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) )
181	180	oveq2d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 6 ) x. ( ( curry V ` i ) ` 6 ) ) = ( ( K ` 6 ) x. ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) )
182	177 181	eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 6 ) = ( ( K ` 6 ) x. ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) )
183	168 182	oveq12d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 5 ) + ( ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ` 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 ) ) ) ) )
184	39 183	eqtrid	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( seq 1 ( + , ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) ` 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 ) ) ) ) )
185	3	adantr	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> K : ( 1 ... 6 ) --> RR )
186	185 86	ffvelcdmd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( K ` 1 ) e. RR )
187	90	rr3fv1cld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( A ` i ) ` 1 ) e. RR )
188	187	resqcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( ( A ` i ) ` 1 ) ^ 2 ) e. RR )
189	186 188	remulcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) e. RR )
190	189	recnd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) e. CC )
191	185 105	ffvelcdmd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( K ` 2 ) e. RR )
192	90	rr3fv2cld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( A ` i ) ` 2 ) e. RR )
193	192	resqcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( ( A ` i ) ` 2 ) ^ 2 ) e. RR )
194	191 193	remulcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) e. RR )
195	194	recnd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) e. CC )
196	190 195	addcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( ( K ` 1 ) x. ( ( ( A ` i ) ` 1 ) ^ 2 ) ) + ( ( K ` 2 ) x. ( ( ( A ` i ) ` 2 ) ^ 2 ) ) ) e. CC )
197	185 123	ffvelcdmd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( K ` 3 ) e. RR )
198	90	rr3fv3cld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( A ` i ) ` 3 ) e. RR )
199	198	resqcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( ( A ` i ) ` 3 ) ^ 2 ) e. RR )
200	197 199	remulcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 3 ) x. ( ( ( A ` i ) ` 3 ) ^ 2 ) ) e. RR )
201	200	recnd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 3 ) x. ( ( ( A ` i ) ` 3 ) ^ 2 ) ) e. CC )
202	196 201	addcld	|- ( ( 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 ) ) ) e. CC )
203	185 141	ffvelcdmd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( K ` 4 ) e. RR )
204	187 192	remulcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) e. RR )
205	203 204	remulcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 4 ) x. ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) ) e. RR )
206	205	recnd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 4 ) x. ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) ) e. CC )
207	185 159	ffvelcdmd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( K ` 5 ) e. RR )
208	192 198	remulcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) e. RR )
209	207 208	remulcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 5 ) x. ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) ) e. RR )
210	209	recnd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 5 ) x. ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) ) e. CC )
211	202 206 210	addassd	|- ( ( 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 ` 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 ) ) ) ) ) )
212	211	oveq1d	|- ( ( 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 ) ) ) ) = ( ( ( ( ( ( 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 ) ) ) ) )
213	206 210	addcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( ( K ` 4 ) x. ( ( ( A ` i ) ` 1 ) x. ( ( A ` i ) ` 2 ) ) ) + ( ( K ` 5 ) x. ( ( ( A ` i ) ` 2 ) x. ( ( A ` i ) ` 3 ) ) ) ) e. CC )
214	185 175	ffvelcdmd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( K ` 6 ) e. RR )
215	198 187	remulcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) e. RR )
216	214 215	remulcld	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 6 ) x. ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) e. RR )
217	216	recnd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( ( K ` 6 ) x. ( ( ( A ` i ) ` 3 ) x. ( ( A ` i ) ` 1 ) ) ) e. CC )
218	202 213 217	addassd	|- ( ( 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 ) ) ) ) = ( ( ( ( ( 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 ) ) ) ) ) )
219	212 218	eqtrd	|- ( ( 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 ) ) ) ) = ( ( ( ( ( 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 ) ) ) ) ) )
220	30 184 219	3eqtrd	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( RRfld gsum ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) = ( ( ( ( ( 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 ) ) ) ) ) )
221		fveq2	|- ( v = j -> ( K ` v ) = ( K ` j ) )
222		fveq2	|- ( v = j -> ( ( curry V ` i ) ` v ) = ( ( curry V ` i ) ` j ) )
223	221 222	oveq12d	|- ( v = j -> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) = ( ( K ` j ) x. ( ( curry V ` i ) ` j ) ) )
224	223	cbvmptv	|- ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) = ( j e. ( 1 ... 6 ) |-> ( ( K ` j ) x. ( ( curry V ` i ) ` j ) ) )
225	224	a1i	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) = ( j e. ( 1 ... 6 ) |-> ( ( K ` j ) x. ( ( curry V ` i ) ` j ) ) ) )
226	225	oveq2d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( RRfld gsum ( v e. ( 1 ... 6 ) |-> ( ( K ` v ) x. ( ( curry V ` i ) ` v ) ) ) ) = ( RRfld gsum ( j e. ( 1 ... 6 ) |-> ( ( K ` j ) x. ( ( curry V ` i ) ` j ) ) ) ) )
227	220 226 4	3eqtr3d	|- ( ( ph /\ i e. ( 1 ... 6 ) ) -> ( RRfld gsum ( j e. ( 1 ... 6 ) |-> ( ( K ` j ) x. ( ( curry V ` i ) ` j ) ) ) ) = 0 )