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	No typesetting found for |- V = ( i e. ( 1 ... 6 ) , j e. ( 1 ... 6 ) |-> ( ( veronese ` ( A ` i ) ) ` j ) ) with typecode |-
	veroquad.f	$$⊢\phi \to A:\left(1\dots 6\right)⟶{ℝ}^{\left(1\dots 3\right)}$$
	veroquad.k	$$⊢\phi \to K:\left(1\dots 6\right)⟶ℝ$$
	veroquad.q	$$⊢\left(\phi \wedge i\in \left(1\dots 6\right)\right)\to \left(K\left(1\right){A\left(i\right)\left(1\right)}^2+K\left(2\right){A\left(i\right)\left(2\right)}^2\right)+K\left(3\right){A\left(i\right)\left(3\right)}^2+\left(K\left(4\right)A\left(i\right)\left(1\right)A\left(i\right)\left(2\right)+K\left(5\right)A\left(i\right)\left(2\right)A\left(i\right)\left(3\right)\right)+K\left(6\right)A\left(i\right)\left(3\right)A\left(i\right)\left(1\right)=0$$
Assertion	veroquadmodzerod	$$⊢\phi \to {\sum }_{{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)}\left(K{{\cdot }_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}}_{f}currytposV\right)=0_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}\left(1\dots 6\right)\right)}$$

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