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	No typesetting found for \|- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) \|-> ( ( veronese ` ( A ` i ) ) ` j ) ) with typecode \|-
	veroquad.f	$⊢ φ \to A : (1 \dots 6) ⟶ ℝ^{(1 \dots 3)}$
	veroquad.k	$⊢ φ \to K : (1 \dots 6) ⟶ ℝ$
	veroquad.q	$⊢ (φ \land i \in (1 \dots 6)) \to (K (1) {A (i) (1)}^{2} + K (2) {A (i) (2)}^{2}) + K (3) {A (i) (3)}^{2} + (K (4) A (i) (1) A (i) (2) + K (5) A (i) (2) A (i) (3)) + K (6) A (i) (3) A (i) (1) = 0$
Assertion	veroquadgsumlem	$⊢ (φ \land i \in (1 \dots 6)) \to {\sum_{ℝ_{fld}}}_{j = 1}^{6} K (j) curry V (i) (j) = 0$

Proof

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

Metamath Proof Explorer

Theorem veroquadgsumlem

Proof