Theorem aacllem 42547

Description: Lemma for other theorems about AA. (Contributed by Brendan Leahy, 3-Jan-2020.) (Revised by Alexander van der Vekens and David A. Wheeler, 25-Apr-2020.)

Hypotheses

Ref	Expression
aacllem.0	|- ( ph -> A e. CC )
aacllem.1	|- ( ph -> N e. NN0 )
aacllem.2	|- ( ( ph /\ n e. ( 1 ... N ) ) -> X e. CC )
aacllem.3	|- ( ( ph /\ k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) -> C e. QQ )
aacllem.4	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ^ k ) = sum_ n e. ( 1 ... N ) ( C x. X ) )

Assertion

Ref	Expression
aacllem	|- ( ph -> A e. AA )

Distinct variable groups:   A, k, n   k, N, n   k, X   ph, k, n

Allowed substitution hints:   C( k, n)   X( n)

Proof of Theorem aacllem

Dummy variables x w y B v z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		aacllem.0	. 2 |- ( ph -> A e. CC )
2		aacllem.1	. . . . . . 7 |- ( ph -> N e. NN0 )
3	2	nn0red 11352	. . . . . 6 |- ( ph -> N e. RR )
4	3	ltp1d 10954	. . . . 5 |- ( ph -> N < ( N + 1 ) )
5		peano2nn0 11333	. . . . . . . 8 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
6	2, 5	syl 17	. . . . . . 7 |- ( ph -> ( N + 1 ) e. NN0 )
7	6	nn0red 11352	. . . . . 6 |- ( ph -> ( N + 1 ) e. RR )
8	3, 7	ltnled 10184	. . . . 5 |- ( ph -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
9	4, 8	mpbid 222	. . . 4 |- ( ph -> -. ( N + 1 ) <_ N )
10		aacllem.3	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) -> C e. QQ )
11	10	3expa 1265	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> C e. QQ )
12		eqid 2622	. . . . . . . . . . 11 |- ( n e. ( 1 ... N ) |-> C ) = ( n e. ( 1 ... N ) |-> C )
13	11, 12	fmptd 6385	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> C ) : ( 1 ... N ) --> QQ )
14		qex 11800	. . . . . . . . . . 11 |- QQ e. _V
15		ovex 6678	. . . . . . . . . . 11 |- ( 1 ... N ) e. _V
16	14, 15	elmap 7886	. . . . . . . . . 10 |- ( ( n e. ( 1 ... N ) |-> C ) e. ( QQ ^m ( 1 ... N ) ) <-> ( n e. ( 1 ... N ) |-> C ) : ( 1 ... N ) --> QQ )
17	13, 16	sylibr 224	. . . . . . . . 9 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> C ) e. ( QQ ^m ( 1 ... N ) ) )
18		eqid 2622	. . . . . . . . 9 |- ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) = ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
19	17, 18	fmptd 6385	. . . . . . . 8 |- ( ph -> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) --> ( QQ ^m ( 1 ... N ) ) )
20		eqid 2622	. . . . . . . . . . . 12 |- (ℂfld ↾s QQ ) = (ℂfld ↾s QQ )
21	20	qdrng 25309	. . . . . . . . . . 11 |- (ℂfld ↾s QQ ) e. DivRing
22		drngring 18754	. . . . . . . . . . 11 |- ( (ℂfld ↾s QQ ) e. DivRing -> (ℂfld ↾s QQ ) e. Ring )
23	21, 22	ax-mp 5	. . . . . . . . . 10 |- (ℂfld ↾s QQ ) e. Ring
24		fzfi 12771	. . . . . . . . . 10 |- ( 1 ... N ) e. Fin
25		eqid 2622	. . . . . . . . . . 11 |- ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) = ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) )
26	25	frlmlmod 20093	. . . . . . . . . 10 |- ( ( (ℂfld ↾s QQ ) e. Ring /\ ( 1 ... N ) e. Fin ) -> ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LMod )
27	23, 24, 26	mp2an 708	. . . . . . . . 9 |- ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LMod
28		fzfi 12771	. . . . . . . . 9 |- ( 0 ... N ) e. Fin
29	20	qrngbas 25308	. . . . . . . . . . . 12 |- QQ = ( Base ` (ℂfld ↾s QQ ) )
30	25, 29	frlmfibas 20105	. . . . . . . . . . 11 |- ( ( (ℂfld ↾s QQ ) e. DivRing /\ ( 1 ... N ) e. Fin ) -> ( QQ ^m ( 1 ... N ) ) = ( Base ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) )
31	21, 24, 30	mp2an 708	. . . . . . . . . 10 |- ( QQ ^m ( 1 ... N ) ) = ( Base ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) )
32	25	frlmsca 20097	. . . . . . . . . . 11 |- ( ( (ℂfld ↾s QQ ) e. DivRing /\ ( 1 ... N ) e. Fin ) -> (ℂfld ↾s QQ ) = (Scalar ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) )
33	21, 24, 32	mp2an 708	. . . . . . . . . 10 |- (ℂfld ↾s QQ ) = (Scalar ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) )
34		eqid 2622	. . . . . . . . . 10 |- ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) = ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) )
35	20	qrng0 25310	. . . . . . . . . . . 12 |- 0 = ( 0g ` (ℂfld ↾s QQ ) )
36	25, 35	frlm0 20098	. . . . . . . . . . 11 |- ( ( (ℂfld ↾s QQ ) e. Ring /\ ( 1 ... N ) e. Fin ) -> ( ( 1 ... N ) X. { 0 } ) = ( 0g ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) )
37	23, 24, 36	mp2an 708	. . . . . . . . . 10 |- ( ( 1 ... N ) X. { 0 } ) = ( 0g ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) )
38		eqid 2622	. . . . . . . . . . . 12 |- ( (ℂfld ↾s QQ ) freeLMod ( 0 ... N ) ) = ( (ℂfld ↾s QQ ) freeLMod ( 0 ... N ) )
39	38, 29	frlmfibas 20105	. . . . . . . . . . 11 |- ( ( (ℂfld ↾s QQ ) e. DivRing /\ ( 0 ... N ) e. Fin ) -> ( QQ ^m ( 0 ... N ) ) = ( Base ` ( (ℂfld ↾s QQ ) freeLMod ( 0 ... N ) ) ) )
40	21, 28, 39	mp2an 708	. . . . . . . . . 10 |- ( QQ ^m ( 0 ... N ) ) = ( Base ` ( (ℂfld ↾s QQ ) freeLMod ( 0 ... N ) ) )
41	31, 33, 34, 37, 35, 40	islindf4 20177	. . . . . . . . 9 |- ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LMod /\ ( 0 ... N ) e. Fin /\ ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) --> ( QQ ^m ( 1 ... N ) ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
42	27, 28, 41	mp3an12 1414	. . . . . . . 8 |- ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) --> ( QQ ^m ( 1 ... N ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
43	19, 42	syl 17	. . . . . . 7 |- ( ph -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
44		elmapi 7879	. . . . . . . . 9 |- ( w e. ( QQ ^m ( 0 ... N ) ) -> w : ( 0 ... N ) --> QQ )
45		fzfid 12772	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( 0 ... N ) e. Fin )
46		fvexd 6203	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. _V )
47	15	mptex 6486	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( 1 ... N ) |-> C ) e. _V
48	47	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> C ) e. _V )
49		simpr 477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> w : ( 0 ... N ) --> QQ )
50	49	feqmptd 6249	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> w = ( k e. ( 0 ... N ) |-> ( w ` k ) ) )
51		eqidd 2623	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) = ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) )
52	45, 46, 48, 50, 51	offval2 6914	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) = ( k e. ( 0 ... N ) |-> ( ( w ` k ) ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( n e. ( 1 ... N ) |-> C ) ) ) )
53		fzfid 12772	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( 1 ... N ) e. Fin )
54		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( w : ( 0 ... N ) --> QQ /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. QQ )
55	54	adantll 750	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. QQ )
56	17	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> C ) e. ( QQ ^m ( 1 ... N ) ) )
57		cnfldmul 19752	. . . . . . . . . . . . . . . . . . . . . 22 |- x. = ( .r ` ℂfld )
58	20, 57	ressmulr 16006	. . . . . . . . . . . . . . . . . . . . 21 |- ( QQ e. _V -> x. = ( .r ` (ℂfld ↾s QQ ) ) )
59	14, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- x. = ( .r ` (ℂfld ↾s QQ ) )
60	25, 31, 29, 53, 55, 56, 34, 59	frlmvscafval 20109	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( n e. ( 1 ... N ) |-> C ) ) = ( ( ( 1 ... N ) X. { ( w ` k ) } ) oF x. ( n e. ( 1 ... N ) |-> C ) ) )
61		fvexd 6203	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( w ` k ) e. _V )
62	11	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> C e. QQ )
63		fconstmpt 5163	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 ... N ) X. { ( w ` k ) } ) = ( n e. ( 1 ... N ) |-> ( w ` k ) )
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( 1 ... N ) X. { ( w ` k ) } ) = ( n e. ( 1 ... N ) |-> ( w ` k ) ) )
65		eqidd 2623	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> C ) = ( n e. ( 1 ... N ) |-> C ) )
66	53, 61, 62, 64, 65	offval2 6914	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( ( 1 ... N ) X. { ( w ` k ) } ) oF x. ( n e. ( 1 ... N ) |-> C ) ) = ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) )
67	60, 66	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( n e. ( 1 ... N ) |-> C ) ) = ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) )
68	67	mpteq2dva 4744	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( k e. ( 0 ... N ) |-> ( ( w ` k ) ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( n e. ( 1 ... N ) |-> C ) ) ) = ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) )
69	52, 68	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) = ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) )
70	69	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) ) )
71		fzfid 12772	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( 1 ... N ) e. Fin )
72	23	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> (ℂfld ↾s QQ ) e. Ring )
73	55	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. QQ )
74	11	an32s 846	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> C e. QQ )
75	74	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> C e. QQ )
76		qmulcl 11806	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( w ` k ) e. QQ /\ C e. QQ ) -> ( ( w ` k ) x. C ) e. QQ )
77	73, 75, 76	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. C ) e. QQ )
78	77	an32s 846	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( ( w ` k ) x. C ) e. QQ )
79		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) = ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) )
80	78, 79	fmptd 6385	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) : ( 1 ... N ) --> QQ )
81	14, 15	elmap 7886	. . . . . . . . . . . . . . . . 17 |- ( ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) e. ( QQ ^m ( 1 ... N ) ) <-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) : ( 1 ... N ) --> QQ )
82	80, 81	sylibr 224	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) e. ( QQ ^m ( 1 ... N ) ) )
83		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) = ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) )
84	15	mptex 6486	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) e. _V
85	84	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) e. _V )
86		snex 4908	. . . . . . . . . . . . . . . . . . 19 |- { 0 } e. _V
87	15, 86	xpex 6962	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 ... N ) X. { 0 } ) e. _V
88	87	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( 1 ... N ) X. { 0 } ) e. _V )
89	83, 45, 85, 88	fsuppmptdm 8286	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) finSupp ( ( 1 ... N ) X. { 0 } ) )
90	25, 31, 37, 71, 45, 72, 82, 89	frlmgsum 20111	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) ) ) = ( n e. ( 1 ... N ) |-> ( (ℂfld ↾s QQ ) gsumg ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) ) )
91		cnfldbas 19750	. . . . . . . . . . . . . . . . . 18 |- CC = ( Base ` ℂfld )
92		cnfldadd 19751	. . . . . . . . . . . . . . . . . 18 |- + = ( +g ` ℂfld )
93		cnfldex 19749	. . . . . . . . . . . . . . . . . . 19 |- ℂfld e. _V
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ℂfld e. _V )
95		fzfid 12772	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( 0 ... N ) e. Fin )
96		qsscn 11799	. . . . . . . . . . . . . . . . . . 19 |- QQ C_ CC
97	96	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> QQ C_ CC )
98		eqid 2622	. . . . . . . . . . . . . . . . . . 19 |- ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) = ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) )
99	77, 98	fmptd 6385	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) : ( 0 ... N ) --> QQ )
100		0z 11388	. . . . . . . . . . . . . . . . . . . 20 |- 0 e. ZZ
101		zq 11794	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 e. ZZ -> 0 e. QQ )
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- 0 e. QQ
103	102	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> 0 e. QQ )
104		addid2 10219	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. CC -> ( 0 + x ) = x )
105		addid1 10216	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. CC -> ( x + 0 ) = x )
106	104, 105	jca 554	. . . . . . . . . . . . . . . . . . 19 |- ( x e. CC -> ( ( 0 + x ) = x /\ ( x + 0 ) = x ) )
107	106	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ x e. CC ) -> ( ( 0 + x ) = x /\ ( x + 0 ) = x ) )
108	91, 92, 20, 94, 95, 97, 99, 103, 107	gsumress 17276	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> (ℂfld gsumg ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) = ( (ℂfld ↾s QQ ) gsumg ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) )
109		simplr 792	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> w : ( 0 ... N ) --> QQ )
110		qcn 11802	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( w ` k ) e. QQ -> ( w ` k ) e. CC )
111	54, 110	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( w : ( 0 ... N ) --> QQ /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. CC )
112	109, 111	sylan 488	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. CC )
113		qcn 11802	. . . . . . . . . . . . . . . . . . . . . 22 |- ( C e. QQ -> C e. CC )
114	11, 113	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> C e. CC )
115	114	an32s 846	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> C e. CC )
116	115	adantllr 755	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> C e. CC )
117	112, 116	mulcld 10060	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. C ) e. CC )
118	95, 117	gsumfsum 19813	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> (ℂfld gsumg ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
119	108, 118	eqtr3d 2658	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( (ℂfld ↾s QQ ) gsumg ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
120	119	mpteq2dva 4744	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( n e. ( 1 ... N ) |-> ( (ℂfld ↾s QQ ) gsumg ( k e. ( 0 ... N ) |-> ( ( w ` k ) x. C ) ) ) ) = ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) )
121	70, 90, 120	3eqtrd 2660	. . . . . . . . . . . . . 14 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) )
122		qaddcl 11804	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. QQ /\ y e. QQ ) -> ( x + y ) e. QQ )
123	122	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( x + y ) e. QQ )
124	97, 123, 95, 77, 103	fsumcllem 14463	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) e. QQ )
125		eqid 2622	. . . . . . . . . . . . . . . 16 |- ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) = ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
126	124, 125	fmptd 6385	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) : ( 1 ... N ) --> QQ )
127	14, 15	elmap 7886	. . . . . . . . . . . . . . 15 |- ( ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) e. ( QQ ^m ( 1 ... N ) ) <-> ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) : ( 1 ... N ) --> QQ )
128	126, 127	sylibr 224	. . . . . . . . . . . . . 14 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) e. ( QQ ^m ( 1 ... N ) ) )
129	121, 128	eqeltrd 2701	. . . . . . . . . . . . 13 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) e. ( QQ ^m ( 1 ... N ) ) )
130		elmapi 7879	. . . . . . . . . . . . 13 |- ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) e. ( QQ ^m ( 1 ... N ) ) -> ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) : ( 1 ... N ) --> QQ )
131		ffn 6045	. . . . . . . . . . . . 13 |- ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) : ( 1 ... N ) --> QQ -> ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) Fn ( 1 ... N ) )
132	129, 130, 131	3syl 18	. . . . . . . . . . . 12 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) Fn ( 1 ... N ) )
133		c0ex 10034	. . . . . . . . . . . . 13 |- 0 e. _V
134		fnconstg 6093	. . . . . . . . . . . . 13 |- ( 0 e. _V -> ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N ) )
135	133, 134	ax-mp 5	. . . . . . . . . . . 12 |- ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N )
136		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ n ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) )
137		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ n gsumg
138		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ n w
139		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ n oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) )
140		nfcv 2764	. . . . . . . . . . . . . . . 16 |- F/_ n ( 0 ... N )
141		nfmpt1 4747	. . . . . . . . . . . . . . . 16 |- F/_ n ( n e. ( 1 ... N ) |-> C )
142	140, 141	nfmpt 4746	. . . . . . . . . . . . . . 15 |- F/_ n ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
143	138, 139, 142	nfov 6676	. . . . . . . . . . . . . 14 |- F/_ n ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) )
144	136, 137, 143	nfov 6676	. . . . . . . . . . . . 13 |- F/_ n ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) )
145		nfcv 2764	. . . . . . . . . . . . 13 |- F/_ n ( ( 1 ... N ) X. { 0 } )
146	144, 145	eqfnfv2f 6315	. . . . . . . . . . . 12 |- ( ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) Fn ( 1 ... N ) /\ ( ( 1 ... N ) X. { 0 } ) Fn ( 1 ... N ) ) -> ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) <-> A. n e. ( 1 ... N ) ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) ) )
147	132, 135, 146	sylancl 694	. . . . . . . . . . 11 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) <-> A. n e. ( 1 ... N ) ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) ) )
148	121	fveq1d 6193	. . . . . . . . . . . . . 14 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = ( ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) ` n ) )
149		sumex 14418	. . . . . . . . . . . . . . 15 |- sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) e. _V
150	125	fvmpt2 6291	. . . . . . . . . . . . . . 15 |- ( ( n e. ( 1 ... N ) /\ sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) e. _V ) -> ( ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) ` n ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
151	149, 150	mpan2 707	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... N ) -> ( ( n e. ( 1 ... N ) |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) ) ` n ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
152	148, 151	sylan9eq 2676	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) )
153	133	fvconst2 6469	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { 0 } ) ` n ) = 0 )
154	153	adantl 482	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1 ... N ) X. { 0 } ) ` n ) = 0 )
155	152, 154	eqeq12d 2637	. . . . . . . . . . . 12 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) <-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
156	155	ralbidva 2985	. . . . . . . . . . 11 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( A. n e. ( 1 ... N ) ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) ` n ) = ( ( ( 1 ... N ) X. { 0 } ) ` n ) <-> A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
157	147, 156	bitrd 268	. . . . . . . . . 10 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) <-> A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
158	157	imbi1d 331	. . . . . . . . 9 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
159	44, 158	sylan2 491	. . . . . . . 8 |- ( ( ph /\ w e. ( QQ ^m ( 0 ... N ) ) ) -> ( ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
160	159	ralbidva 2985	. . . . . . 7 |- ( ph -> ( A. w e. ( QQ ^m ( 0 ... N ) ) ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) gsumg ( w oF ( .s ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) ) = ( ( 1 ... N ) X. { 0 } ) -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
161	43, 160	bitrd 268	. . . . . 6 |- ( ph -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) ) )
162		drngnzr 19262	. . . . . . . . 9 |- ( (ℂfld ↾s QQ ) e. DivRing -> (ℂfld ↾s QQ ) e. NzRing )
163	21, 162	ax-mp 5	. . . . . . . 8 |- (ℂfld ↾s QQ ) e. NzRing
164	33	islindf3 20165	. . . . . . . 8 |- ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LMod /\ (ℂfld ↾s QQ ) e. NzRing ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) <-> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) ) )
165	27, 163, 164	mp2an 708	. . . . . . 7 |- ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) <-> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) )
166	47, 18	dmmpti 6023	. . . . . . . . 9 |- dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) = ( 0 ... N )
167		f1eq2 6097	. . . . . . . . 9 |- ( dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) = ( 0 ... N ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -1-1-> _V <-> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V ) )
168	166, 167	ax-mp 5	. . . . . . . 8 |- ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -1-1-> _V <-> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V )
169	168	anbi1i 731	. . . . . . 7 |- ( ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : dom ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) <-> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) )
170	165, 169	bitri 264	. . . . . 6 |- ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) LIndF ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) <-> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) )
171		con34b 306	. . . . . . . . 9 |- ( ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> ( -. w = ( ( 0 ... N ) X. { 0 } ) -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
172		df-nel 2898	. . . . . . . . . . 11 |- ( w e/ { ( ( 0 ... N ) X. { 0 } ) } <-> -. w e. { ( ( 0 ... N ) X. { 0 } ) } )
173		velsn 4193	. . . . . . . . . . 11 |- ( w e. { ( ( 0 ... N ) X. { 0 } ) } <-> w = ( ( 0 ... N ) X. { 0 } ) )
174	172, 173	xchbinx 324	. . . . . . . . . 10 |- ( w e/ { ( ( 0 ... N ) X. { 0 } ) } <-> -. w = ( ( 0 ... N ) X. { 0 } ) )
175	174	imbi1i 339	. . . . . . . . 9 |- ( ( w e/ { ( ( 0 ... N ) X. { 0 } ) } -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) <-> ( -. w = ( ( 0 ... N ) X. { 0 } ) -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
176	171, 175	bitr4i 267	. . . . . . . 8 |- ( ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> ( w e/ { ( ( 0 ... N ) X. { 0 } ) } -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
177	176	ralbii 2980	. . . . . . 7 |- ( A. w e. ( QQ ^m ( 0 ... N ) ) ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> A. w e. ( QQ ^m ( 0 ... N ) ) ( w e/ { ( ( 0 ... N ) X. { 0 } ) } -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
178		raldifb 3750	. . . . . . 7 |- ( A. w e. ( QQ ^m ( 0 ... N ) ) ( w e/ { ( ( 0 ... N ) X. { 0 } ) } -> -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) <-> A. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
179		ralnex 2992	. . . . . . 7 |- ( A. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) -. A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 <-> -. E. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
180	177, 178, 179	3bitri 286	. . . . . 6 |- ( A. w e. ( QQ ^m ( 0 ... N ) ) ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> w = ( ( 0 ... N ) X. { 0 } ) ) <-> -. E. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
181	161, 170, 180	3bitr3g 302	. . . . 5 |- ( ph -> ( ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) <-> -. E. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
182		eqid 2622	. . . . . . . . . . . . 13 |- ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) = ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) )
183	31, 182	lssmre 18966	. . . . . . . . . . . 12 |- ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LMod -> ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) e. (Moore ` ( QQ ^m ( 1 ... N ) ) ) )
184	27, 183	ax-mp 5	. . . . . . . . . . 11 |- ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) e. (Moore ` ( QQ ^m ( 1 ... N ) ) )
185	184	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) e. (Moore ` ( QQ ^m ( 1 ... N ) ) ) )
186		eqid 2622	. . . . . . . . . . . 12 |- ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) = ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) )
187		eqid 2622	. . . . . . . . . . . 12 |- (mrCls ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) = (mrCls ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) )
188	182, 186, 187	mrclsp 18989	. . . . . . . . . . 11 |- ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LMod -> ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) = (mrCls ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) )
189	27, 188	ax-mp 5	. . . . . . . . . 10 |- ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) = (mrCls ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) )
190		eqid 2622	. . . . . . . . . 10 |- (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) = (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) )
191	33	islvec 19104	. . . . . . . . . . . . 13 |- ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LVec <-> ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LMod /\ (ℂfld ↾s QQ ) e. DivRing ) )
192	27, 21, 191	mpbir2an 955	. . . . . . . . . . . 12 |- ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LVec
193	182, 189, 31	lssacsex 19144	. . . . . . . . . . . . 13 |- ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LVec -> ( ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) e. (ACS ` ( QQ ^m ( 1 ... N ) ) ) /\ A. z e. ~P ( QQ ^m ( 1 ... N ) ) A. x e. ( QQ ^m ( 1 ... N ) ) A. y e. ( ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { x } ) ) \ ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` z ) ) x e. ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { y } ) ) ) )
194	193	simprd 479	. . . . . . . . . . . 12 |- ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LVec -> A. z e. ~P ( QQ ^m ( 1 ... N ) ) A. x e. ( QQ ^m ( 1 ... N ) ) A. y e. ( ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { x } ) ) \ ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` z ) ) x e. ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { y } ) ) )
195	192, 194	ax-mp 5	. . . . . . . . . . 11 |- A. z e. ~P ( QQ ^m ( 1 ... N ) ) A. x e. ( QQ ^m ( 1 ... N ) ) A. y e. ( ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { x } ) ) \ ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` z ) ) x e. ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { y } ) )
196	195	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) -> A. z e. ~P ( QQ ^m ( 1 ... N ) ) A. x e. ( QQ ^m ( 1 ... N ) ) A. y e. ( ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { x } ) ) \ ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` z ) ) x e. ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( z u. { y } ) ) )
197		frn 6053	. . . . . . . . . . . . 13 |- ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) --> ( QQ ^m ( 1 ... N ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( QQ ^m ( 1 ... N ) ) )
198	19, 197	syl 17	. . . . . . . . . . . 12 |- ( ph -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( QQ ^m ( 1 ... N ) ) )
199		dif0 3950	. . . . . . . . . . . 12 |- ( ( QQ ^m ( 1 ... N ) ) \ (/) ) = ( QQ ^m ( 1 ... N ) )
200	198, 199	syl6sseqr 3652	. . . . . . . . . . 11 |- ( ph -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( ( QQ ^m ( 1 ... N ) ) \ (/) ) )
201	200	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( ( QQ ^m ( 1 ... N ) ) \ (/) ) )
202		eqid 2622	. . . . . . . . . . . . . . 15 |- ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) = ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) )
203	202, 25, 31	uvcff 20130	. . . . . . . . . . . . . 14 |- ( ( (ℂfld ↾s QQ ) e. Ring /\ ( 1 ... N ) e. Fin ) -> ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) : ( 1 ... N ) --> ( QQ ^m ( 1 ... N ) ) )
204	23, 24, 203	mp2an 708	. . . . . . . . . . . . 13 |- ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) : ( 1 ... N ) --> ( QQ ^m ( 1 ... N ) )
205		frn 6053	. . . . . . . . . . . . 13 |- ( ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) : ( 1 ... N ) --> ( QQ ^m ( 1 ... N ) ) -> ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) C_ ( QQ ^m ( 1 ... N ) ) )
206	204, 205	ax-mp 5	. . . . . . . . . . . 12 |- ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) C_ ( QQ ^m ( 1 ... N ) )
207	206, 199	sseqtr4i 3638	. . . . . . . . . . 11 |- ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) C_ ( ( QQ ^m ( 1 ... N ) ) \ (/) )
208	207	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) C_ ( ( QQ ^m ( 1 ... N ) ) \ (/) ) )
209		un0 3967	. . . . . . . . . . . . . 14 |- ( ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) u. (/) ) = ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) )
210	209	fveq2i 6194	. . . . . . . . . . . . 13 |- ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) u. (/) ) ) = ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) )
211		eqid 2622	. . . . . . . . . . . . . . . 16 |- (LBasis ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) = (LBasis ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) )
212	25, 202, 211	frlmlbs 20136	. . . . . . . . . . . . . . 15 |- ( ( (ℂfld ↾s QQ ) e. Ring /\ ( 1 ... N ) e. Fin ) -> ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) e. (LBasis ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) )
213	23, 24, 212	mp2an 708	. . . . . . . . . . . . . 14 |- ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) e. (LBasis ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) )
214	31, 211, 186	lbssp 19079	. . . . . . . . . . . . . 14 |- ( ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) e. (LBasis ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) -> ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ) = ( QQ ^m ( 1 ... N ) ) )
215	213, 214	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ) = ( QQ ^m ( 1 ... N ) )
216	210, 215	eqtri 2644	. . . . . . . . . . . 12 |- ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) u. (/) ) ) = ( QQ ^m ( 1 ... N ) )
217	198, 216	syl6sseqr 3652	. . . . . . . . . . 11 |- ( ph -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) u. (/) ) ) )
218	217	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) u. (/) ) ) )
219		un0 3967	. . . . . . . . . . 11 |- ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) u. (/) ) = ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) )
220	27, 163	pm3.2i 471	. . . . . . . . . . . . . 14 |- ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LMod /\ (ℂfld ↾s QQ ) e. NzRing )
221	186, 33	lindsind2 20158	. . . . . . . . . . . . . 14 |- ( ( ( ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) e. LMod /\ (ℂfld ↾s QQ ) e. NzRing ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) /\ x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) -> -. x e. ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) )
222	220, 221	mp3an1 1411	. . . . . . . . . . . . 13 |- ( ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) /\ x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ) -> -. x e. ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) )
223	222	ralrimiva 2966	. . . . . . . . . . . 12 |- ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) -> A. x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -. x e. ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) )
224	189, 190	ismri2 16292	. . . . . . . . . . . . . 14 |- ( ( ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) e. (Moore ` ( QQ ^m ( 1 ... N ) ) ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) C_ ( QQ ^m ( 1 ... N ) ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) <-> A. x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -. x e. ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) ) )
225	184, 198, 224	sylancr 695	. . . . . . . . . . . . 13 |- ( ph -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) <-> A. x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -. x e. ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) ) )
226	225	biimpar 502	. . . . . . . . . . . 12 |- ( ( ph /\ A. x e. ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -. x e. ( ( LSpan ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ` ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) \ { x } ) ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) )
227	223, 226	sylan2 491	. . . . . . . . . . 11 |- ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) )
228	219, 227	syl5eqel 2705	. . . . . . . . . 10 |- ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) u. (/) ) e. (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) )
229		mptfi 8265	. . . . . . . . . . . . 13 |- ( ( 0 ... N ) e. Fin -> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin )
230		rnfi 8249	. . . . . . . . . . . . 13 |- ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin )
231	28, 229, 230	mp2b 10	. . . . . . . . . . . 12 |- ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin
232	231	orci 405	. . . . . . . . . . 11 |- ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin \/ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) e. Fin )
233	232	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. Fin \/ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) e. Fin ) )
234	185, 189, 190, 196, 201, 208, 218, 228, 233	mreexexd 16308	. . . . . . . . 9 |- ( ( ph /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) -> E. v e. ~P ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v /\ ( v u. (/) ) e. (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) ) )
235	234	ex 450	. . . . . . . 8 |- ( ph -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) -> E. v e. ~P ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v /\ ( v u. (/) ) e. (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) ) ) )
236		ovex 6678	. . . . . . . . . . . . 13 |- ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) e. _V
237	236	rnex 7100	. . . . . . . . . . . 12 |- ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) e. _V
238		elpwi 4168	. . . . . . . . . . . 12 |- ( v e. ~P ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) -> v C_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) )
239		ssdomg 8001	. . . . . . . . . . . 12 |- ( ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) e. _V -> ( v C_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) -> v ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ) )
240	237, 238, 239	mpsyl 68	. . . . . . . . . . 11 |- ( v e. ~P ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) -> v ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) )
241		endomtr 8014	. . . . . . . . . . . . . 14 |- ( ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v /\ v ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) )
242	241	ancoms 469	. . . . . . . . . . . . 13 |- ( ( v ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v ) -> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) )
243		f1f1orn 6148	. . . . . . . . . . . . . . . 16 |- ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-onto-> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) )
244		ovex 6678	. . . . . . . . . . . . . . . . 17 |- ( 0 ... N ) e. _V
245	244	f1oen 7976	. . . . . . . . . . . . . . . 16 |- ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-onto-> ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -> ( 0 ... N ) ~~ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) )
246	243, 245	syl 17	. . . . . . . . . . . . . . 15 |- ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( 0 ... N ) ~~ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) )
247		endomtr 8014	. . . . . . . . . . . . . . . . 17 |- ( ( ( 0 ... N ) ~~ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ) -> ( 0 ... N ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) )
248	202	uvcendim 20186	. . . . . . . . . . . . . . . . . . . 20 |- ( ( (ℂfld ↾s QQ ) e. NzRing /\ ( 1 ... N ) e. Fin ) -> ( 1 ... N ) ~~ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) )
249	163, 24, 248	mp2an 708	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ... N ) ~~ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) )
250	249	ensymi 8006	. . . . . . . . . . . . . . . . . 18 |- ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ~~ ( 1 ... N )
251		domentr 8015	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 0 ... N ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) /\ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ~~ ( 1 ... N ) ) -> ( 0 ... N ) ~<_ ( 1 ... N ) )
252		hashdom 13168	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 0 ... N ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( # ` ( 0 ... N ) ) <_ ( # ` ( 1 ... N ) ) <-> ( 0 ... N ) ~<_ ( 1 ... N ) ) )
253	28, 24, 252	mp2an 708	. . . . . . . . . . . . . . . . . . . 20 |- ( ( # ` ( 0 ... N ) ) <_ ( # ` ( 1 ... N ) ) <-> ( 0 ... N ) ~<_ ( 1 ... N ) )
254		hashfz0 13219	. . . . . . . . . . . . . . . . . . . . . 22 |- ( N e. NN0 -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
255	2, 254	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
256		hashfz1 13134	. . . . . . . . . . . . . . . . . . . . . 22 |- ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
257	2, 256	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( # ` ( 1 ... N ) ) = N )
258	255, 257	breq12d 4666	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( # ` ( 0 ... N ) ) <_ ( # ` ( 1 ... N ) ) <-> ( N + 1 ) <_ N ) )
259	253, 258	syl5bbr 274	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 0 ... N ) ~<_ ( 1 ... N ) <-> ( N + 1 ) <_ N ) )
260	251, 259	syl5ib 234	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( ( 0 ... N ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) /\ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ~~ ( 1 ... N ) ) -> ( N + 1 ) <_ N ) )
261	250, 260	mpan2i 713	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 0 ... N ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) -> ( N + 1 ) <_ N ) )
262	247, 261	syl5 34	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( 0 ... N ) ~~ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ) -> ( N + 1 ) <_ N ) )
263	262	expd 452	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 0 ... N ) ~~ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) -> ( N + 1 ) <_ N ) ) )
264	246, 263	syl5 34	. . . . . . . . . . . . . 14 |- ( ph -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) -> ( N + 1 ) <_ N ) ) )
265	264	com23 86	. . . . . . . . . . . . 13 |- ( ph -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
266	242, 265	syl5 34	. . . . . . . . . . . 12 |- ( ph -> ( ( v ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
267	266	expdimp 453	. . . . . . . . . . 11 |- ( ( ph /\ v ~<_ ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
268	240, 267	sylan2 491	. . . . . . . . . 10 |- ( ( ph /\ v e. ~P ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ) -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
269	268	adantrd 484	. . . . . . . . 9 |- ( ( ph /\ v e. ~P ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ) -> ( ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v /\ ( v u. (/) ) e. (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
270	269	rexlimdva 3031	. . . . . . . 8 |- ( ph -> ( E. v e. ~P ran ( (ℂfld ↾s QQ ) unitVec ( 1 ... N ) ) ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) ~~ v /\ ( v u. (/) ) e. (mrInd ` ( LSubSp ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
271	235, 270	syld 47	. . . . . . 7 |- ( ph -> ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) -> ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V -> ( N + 1 ) <_ N ) ) )
272	271	impd 447	. . . . . 6 |- ( ph -> ( ( ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) /\ ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V ) -> ( N + 1 ) <_ N ) )
273	272	ancomsd 470	. . . . 5 |- ( ph -> ( ( ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) : ( 0 ... N ) -1-1-> _V /\ ran ( k e. ( 0 ... N ) |-> ( n e. ( 1 ... N ) |-> C ) ) e. (LIndS ` ( (ℂfld ↾s QQ ) freeLMod ( 1 ... N ) ) ) ) -> ( N + 1 ) <_ N ) )
274	181, 273	sylbird 250	. . . 4 |- ( ph -> ( -. E. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 -> ( N + 1 ) <_ N ) )
275	9, 274	mt3d 140	. . 3 |- ( ph -> E. w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
276		eldifsn 4317	. . . . 5 |- ( w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) <-> ( w e. ( QQ ^m ( 0 ... N ) ) /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) )
277	44	anim1i 592	. . . . 5 |- ( ( w e. ( QQ ^m ( 0 ... N ) ) /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) -> ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) )
278	276, 277	sylbi 207	. . . 4 |- ( w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) -> ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) )
279	96	a1i 11	. . . . . . . . 9 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> QQ C_ CC )
280	2	adantr 481	. . . . . . . . 9 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> N e. NN0 )
281	279, 280, 55	elplyd 23958	. . . . . . . 8 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. (Poly ` QQ ) )
282	281	adantrr 753	. . . . . . 7 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. (Poly ` QQ ) )
283		uzdisj 12413	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 ... ( ( N + 1 ) - 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)
284	2	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> N e. CC )
285		pncan1 10454	. . . . . . . . . . . . . . . . . . . . 21 |- ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
286	284, 285	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( N + 1 ) - 1 ) = N )
287	286	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 0 ... ( ( N + 1 ) - 1 ) ) = ( 0 ... N ) )
288	287	ineq1d 3813	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 0 ... ( ( N + 1 ) - 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
289	283, 288	syl5eqr 2670	. . . . . . . . . . . . . . . . 17 |- ( ph -> (/) = ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) )
290	289	eqcomd 2628	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) )
291	133	fconst 6091	. . . . . . . . . . . . . . . . . 18 |- ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> { 0 }
292		snssi 4339	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 e. QQ -> { 0 } C_ QQ )
293	100, 101, 292	mp2b 10	. . . . . . . . . . . . . . . . . . 19 |- { 0 } C_ QQ
294	293, 96	sstri 3612	. . . . . . . . . . . . . . . . . 18 |- { 0 } C_ CC
295		fss 6056	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> { 0 } /\ { 0 } C_ CC ) -> ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> CC )
296	291, 294, 295	mp2an 708	. . . . . . . . . . . . . . . . 17 |- ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> CC
297		fun 6066	. . . . . . . . . . . . . . . . 17 |- ( ( ( w : ( 0 ... N ) --> QQ /\ ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> CC ) /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) -> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) )
298	296, 297	mpanl2 717	. . . . . . . . . . . . . . . 16 |- ( ( w : ( 0 ... N ) --> QQ /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) -> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) )
299	290, 298	sylan2 491	. . . . . . . . . . . . . . 15 |- ( ( w : ( 0 ... N ) --> QQ /\ ph ) -> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) )
300	299	ancoms 469	. . . . . . . . . . . . . 14 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) )
301		nn0uz 11722	. . . . . . . . . . . . . . . . . 18 |- NN0 = ( ZZ>= ` 0 )
302	6, 301	syl6eleq 2711	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
303		uzsplit 12412	. . . . . . . . . . . . . . . . . . 19 |- ( ( N + 1 ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
304	302, 303	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
305	301, 304	syl5eq 2668	. . . . . . . . . . . . . . . . 17 |- ( ph -> NN0 = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
306	287	uneq1d 3766	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
307	305, 306	eqtr2d 2657	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) = NN0 )
308		ssequn1 3783	. . . . . . . . . . . . . . . . . 18 |- ( QQ C_ CC <-> ( QQ u. CC ) = CC )
309	96, 308	mpbi 220	. . . . . . . . . . . . . . . . 17 |- ( QQ u. CC ) = CC
310	309	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( QQ u. CC ) = CC )
311	307, 310	feq23d 6040	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) <-> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : NN0 --> CC ) )
312	311	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) --> ( QQ u. CC ) <-> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : NN0 --> CC ) )
313	300, 312	mpbid 222	. . . . . . . . . . . . 13 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) : NN0 --> CC )
314		ffn 6045	. . . . . . . . . . . . . . . 16 |- ( w : ( 0 ... N ) --> QQ -> w Fn ( 0 ... N ) )
315		fnimadisj 6012	. . . . . . . . . . . . . . . 16 |- ( ( w Fn ( 0 ... N ) /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) -> ( w " ( ZZ>= ` ( N + 1 ) ) ) = (/) )
316	314, 290, 315	syl2anr 495	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w " ( ZZ>= ` ( N + 1 ) ) ) = (/) )
317	2	nn0zd 11480	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> N e. ZZ )
318	317	peano2zd 11485	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( N + 1 ) e. ZZ )
319		uzid 11702	. . . . . . . . . . . . . . . . . . 19 |- ( ( N + 1 ) e. ZZ -> ( N + 1 ) e. ( ZZ>= ` ( N + 1 ) ) )
320		ne0i 3921	. . . . . . . . . . . . . . . . . . 19 |- ( ( N + 1 ) e. ( ZZ>= ` ( N + 1 ) ) -> ( ZZ>= ` ( N + 1 ) ) =/= (/) )
321	318, 319, 320	3syl 18	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ZZ>= ` ( N + 1 ) ) =/= (/) )
322		inidm 3822	. . . . . . . . . . . . . . . . . . 19 |- ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) = ( ZZ>= ` ( N + 1 ) )
323	322	neeq1i 2858	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) =/= (/) <-> ( ZZ>= ` ( N + 1 ) ) =/= (/) )
324	321, 323	sylibr 224	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) =/= (/) )
325		xpima2 5578	. . . . . . . . . . . . . . . . 17 |- ( ( ( ZZ>= ` ( N + 1 ) ) i^i ( ZZ>= ` ( N + 1 ) ) ) =/= (/) -> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
326	324, 325	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
327	326	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
328	316, 327	uneq12d 3768	. . . . . . . . . . . . . 14 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( w " ( ZZ>= ` ( N + 1 ) ) ) u. ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) " ( ZZ>= ` ( N + 1 ) ) ) ) = ( (/) u. { 0 } ) )
329		imaundir 5546	. . . . . . . . . . . . . 14 |- ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) " ( ZZ>= ` ( N + 1 ) ) ) = ( ( w " ( ZZ>= ` ( N + 1 ) ) ) u. ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) " ( ZZ>= ` ( N + 1 ) ) ) )
330		uncom 3757	. . . . . . . . . . . . . . 15 |- ( (/) u. { 0 } ) = ( { 0 } u. (/) )
331		un0 3967	. . . . . . . . . . . . . . 15 |- ( { 0 } u. (/) ) = { 0 }
332	330, 331	eqtr2i 2645	. . . . . . . . . . . . . 14 |- { 0 } = ( (/) u. { 0 } )
333	328, 329, 332	3eqtr4g 2681	. . . . . . . . . . . . 13 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
334	290, 314	anim12ci 591	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w Fn ( 0 ... N ) /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) )
335		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . 21 |- ( 0 e. _V -> ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) Fn ( ZZ>= ` ( N + 1 ) ) )
336	133, 335	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) Fn ( ZZ>= ` ( N + 1 ) )
337		fvun1 6269	. . . . . . . . . . . . . . . . . . . 20 |- ( ( w Fn ( 0 ... N ) /\ ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) Fn ( ZZ>= ` ( N + 1 ) ) /\ ( ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) /\ k e. ( 0 ... N ) ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) = ( w ` k ) )
338	336, 337	mp3an2 1412	. . . . . . . . . . . . . . . . . . 19 |- ( ( w Fn ( 0 ... N ) /\ ( ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) /\ k e. ( 0 ... N ) ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) = ( w ` k ) )
339	338	anassrs 680	. . . . . . . . . . . . . . . . . 18 |- ( ( ( w Fn ( 0 ... N ) /\ ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) /\ k e. ( 0 ... N ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) = ( w ` k ) )
340	334, 339	sylan 488	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) = ( w ` k ) )
341	340	eqcomd 2628	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) = ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) )
342	341	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. ( y ^ k ) ) = ( ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) x. ( y ^ k ) ) )
343	342	sumeq2dv 14433	. . . . . . . . . . . . . 14 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) x. ( y ^ k ) ) )
344	343	mpteq2dv 4745	. . . . . . . . . . . . 13 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) = ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) ` k ) x. ( y ^ k ) ) ) )
345	281, 280, 313, 333, 344	coeeq 23983	. . . . . . . . . . . 12 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) = ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) )
346	345	reseq1d 5395	. . . . . . . . . . 11 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) |` ( 0 ... N ) ) )
347		res0 5400	. . . . . . . . . . . . . 14 |- ( w |` (/) ) = (/)
348	289	reseq2d 5396	. . . . . . . . . . . . . 14 |- ( ph -> ( w |` (/) ) = ( w |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
349		res0 5400	. . . . . . . . . . . . . . 15 |- ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` (/) ) = (/)
350	289	reseq2d 5396	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` (/) ) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
351	349, 350	syl5eqr 2670	. . . . . . . . . . . . . 14 |- ( ph -> (/) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
352	347, 348, 351	3eqtr3a 2680	. . . . . . . . . . . . 13 |- ( ph -> ( w |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) )
353		fss 6056	. . . . . . . . . . . . . . 15 |- ( ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> { 0 } /\ { 0 } C_ QQ ) -> ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> QQ )
354	291, 293, 353	mp2an 708	. . . . . . . . . . . . . 14 |- ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> QQ
355		fresaunres1 6077	. . . . . . . . . . . . . 14 |- ( ( w : ( 0 ... N ) --> QQ /\ ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) : ( ZZ>= ` ( N + 1 ) ) --> QQ /\ ( w |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) |` ( 0 ... N ) ) = w )
356	354, 355	mp3an2 1412	. . . . . . . . . . . . 13 |- ( ( w : ( 0 ... N ) --> QQ /\ ( w |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) |` ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) ) ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) |` ( 0 ... N ) ) = w )
357	352, 356	sylan2 491	. . . . . . . . . . . 12 |- ( ( w : ( 0 ... N ) --> QQ /\ ph ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) |` ( 0 ... N ) ) = w )
358	357	ancoms 469	. . . . . . . . . . 11 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( w u. ( ( ZZ>= ` ( N + 1 ) ) X. { 0 } ) ) |` ( 0 ... N ) ) = w )
359	346, 358	eqtrd 2656	. . . . . . . . . 10 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = w )
360		fveq2 6191	. . . . . . . . . . 11 |- ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) = 0p -> (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) = (coeff ` 0p ) )
361	360	reseq1d 5395	. . . . . . . . . 10 |- ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) = 0p -> ( (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = ( (coeff ` 0p ) |` ( 0 ... N ) ) )
362		eqtr2 2642	. . . . . . . . . . . 12 |- ( ( ( (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = w /\ ( (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = ( (coeff ` 0p ) |` ( 0 ... N ) ) ) -> w = ( (coeff ` 0p ) |` ( 0 ... N ) ) )
363		coe0 24012	. . . . . . . . . . . . . 14 |- (coeff ` 0p ) = ( NN0 X. { 0 } )
364	363	reseq1i 5392	. . . . . . . . . . . . 13 |- ( (coeff ` 0p ) |` ( 0 ... N ) ) = ( ( NN0 X. { 0 } ) |` ( 0 ... N ) )
365		elfznn0 12433	. . . . . . . . . . . . . . 15 |- ( x e. ( 0 ... N ) -> x e. NN0 )
366	365	ssriv 3607	. . . . . . . . . . . . . 14 |- ( 0 ... N ) C_ NN0
367		xpssres 5434	. . . . . . . . . . . . . 14 |- ( ( 0 ... N ) C_ NN0 -> ( ( NN0 X. { 0 } ) |` ( 0 ... N ) ) = ( ( 0 ... N ) X. { 0 } ) )
368	366, 367	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( NN0 X. { 0 } ) |` ( 0 ... N ) ) = ( ( 0 ... N ) X. { 0 } )
369	364, 368	eqtri 2644	. . . . . . . . . . . 12 |- ( (coeff ` 0p ) |` ( 0 ... N ) ) = ( ( 0 ... N ) X. { 0 } )
370	362, 369	syl6eq 2672	. . . . . . . . . . 11 |- ( ( ( (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = w /\ ( (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = ( (coeff ` 0p ) |` ( 0 ... N ) ) ) -> w = ( ( 0 ... N ) X. { 0 } ) )
371	370	ex 450	. . . . . . . . . 10 |- ( ( (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = w -> ( ( (coeff ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ) |` ( 0 ... N ) ) = ( (coeff ` 0p ) |` ( 0 ... N ) ) -> w = ( ( 0 ... N ) X. { 0 } ) ) )
372	359, 361, 371	syl2im 40	. . . . . . . . 9 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) = 0p -> w = ( ( 0 ... N ) X. { 0 } ) ) )
373	372	necon3d 2815	. . . . . . . 8 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> ( w =/= ( ( 0 ... N ) X. { 0 } ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) =/= 0p ) )
374	373	impr 649	. . . . . . 7 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) =/= 0p )
375		eldifsn 4317	. . . . . . 7 |- ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( (Poly ` QQ ) \ { 0p } ) <-> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. (Poly ` QQ ) /\ ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) =/= 0p ) )
376	282, 374, 375	sylanbrc 698	. . . . . 6 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( (Poly ` QQ ) \ { 0p } ) )
377	376	adantrr 753	. . . . 5 |- ( ( ph /\ ( ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( (Poly ` QQ ) \ { 0p } ) )
378		oveq1 6657	. . . . . . . . . . . 12 |- ( y = A -> ( y ^ k ) = ( A ^ k ) )
379	378	oveq2d 6666	. . . . . . . . . . 11 |- ( y = A -> ( ( w ` k ) x. ( y ^ k ) ) = ( ( w ` k ) x. ( A ^ k ) ) )
380	379	sumeq2sdv 14435	. . . . . . . . . 10 |- ( y = A -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) )
381		eqid 2622	. . . . . . . . . 10 |- ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) = ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) )
382		sumex 14418	. . . . . . . . . 10 |- sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) e. _V
383	380, 381, 382	fvmpt 6282	. . . . . . . . 9 |- ( A e. CC -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) )
384	1, 383	syl 17	. . . . . . . 8 |- ( ph -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) )
385	384	adantr 481	. . . . . . 7 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) )
386	111	adantll 750	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( w ` k ) e. CC )
387		aacllem.2	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... N ) ) -> X e. CC )
388	387	adantlr 751	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> X e. CC )
389	114, 388	mulcld 10060	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( C x. X ) e. CC )
390	389	adantllr 755	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( C x. X ) e. CC )
391	53, 386, 390	fsummulc2 14516	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. sum_ n e. ( 1 ... N ) ( C x. X ) ) = sum_ n e. ( 1 ... N ) ( ( w ` k ) x. ( C x. X ) ) )
392		aacllem.4	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ^ k ) = sum_ n e. ( 1 ... N ) ( C x. X ) )
393	392	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. ( A ^ k ) ) = ( ( w ` k ) x. sum_ n e. ( 1 ... N ) ( C x. X ) ) )
394	393	adantlr 751	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. ( A ^ k ) ) = ( ( w ` k ) x. sum_ n e. ( 1 ... N ) ( C x. X ) ) )
395	386	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( w ` k ) e. CC )
396	114	adantllr 755	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> C e. CC )
397		simpll 790	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ph )
398	397, 387	sylan 488	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> X e. CC )
399	395, 396, 398	mulassd 10063	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( w ` k ) x. C ) x. X ) = ( ( w ` k ) x. ( C x. X ) ) )
400	399	sumeq2dv 14433	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> sum_ n e. ( 1 ... N ) ( ( ( w ` k ) x. C ) x. X ) = sum_ n e. ( 1 ... N ) ( ( w ` k ) x. ( C x. X ) ) )
401	391, 394, 400	3eqtr4d 2666	. . . . . . . . . . . 12 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ k e. ( 0 ... N ) ) -> ( ( w ` k ) x. ( A ^ k ) ) = sum_ n e. ( 1 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
402	401	sumeq2dv 14433	. . . . . . . . . . 11 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) = sum_ k e. ( 0 ... N ) sum_ n e. ( 1 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
403	111	ad2ant2lr 784	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> ( w ` k ) e. CC )
404	114	anasss 679	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> C e. CC )
405	404	adantlr 751	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> C e. CC )
406	403, 405	mulcld 10060	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> ( ( w ` k ) x. C ) e. CC )
407	387	ad2ant2rl 785	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> X e. CC )
408	406, 407	mulcld 10060	. . . . . . . . . . . 12 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ ( k e. ( 0 ... N ) /\ n e. ( 1 ... N ) ) ) -> ( ( ( w ` k ) x. C ) x. X ) e. CC )
409	45, 71, 408	fsumcom 14507	. . . . . . . . . . 11 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> sum_ k e. ( 0 ... N ) sum_ n e. ( 1 ... N ) ( ( ( w ` k ) x. C ) x. X ) = sum_ n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
410	402, 409	eqtrd 2656	. . . . . . . . . 10 |- ( ( ph /\ w : ( 0 ... N ) --> QQ ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) = sum_ n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
411	410	adantrr 753	. . . . . . . . 9 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) = sum_ n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
412		nfv 1843	. . . . . . . . . . . 12 |- F/ n ph
413		nfv 1843	. . . . . . . . . . . . 13 |- F/ n w : ( 0 ... N ) --> QQ
414		nfra1 2941	. . . . . . . . . . . . 13 |- F/ n A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0
415	413, 414	nfan 1828	. . . . . . . . . . . 12 |- F/ n ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
416	412, 415	nfan 1828	. . . . . . . . . . 11 |- F/ n ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) )
417		rspa 2930	. . . . . . . . . . . . . . . 16 |- ( ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 /\ n e. ( 1 ... N ) ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 )
418	417	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( ( A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 /\ n e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) x. X ) = ( 0 x. X ) )
419	418	adantll 750	. . . . . . . . . . . . . 14 |- ( ( ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) /\ n e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) x. X ) = ( 0 x. X ) )
420	419	adantll 750	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) x. X ) = ( 0 x. X ) )
421	387	adantlr 751	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> X e. CC )
422	95, 421, 117	fsummulc1 14517	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w : ( 0 ... N ) --> QQ ) /\ n e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) x. X ) = sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
423	422	adantlrr 757	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) x. X ) = sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) )
424	387	mul02d 10234	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( 0 x. X ) = 0 )
425	424	adantlr 751	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> ( 0 x. X ) = 0 )
426	420, 423, 425	3eqtr3d 2664	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) /\ n e. ( 1 ... N ) ) -> sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) = 0 )
427	426	ex 450	. . . . . . . . . . 11 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> ( n e. ( 1 ... N ) -> sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) = 0 ) )
428	416, 427	ralrimi 2957	. . . . . . . . . 10 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) = 0 )
429	428	sumeq2d 14432	. . . . . . . . 9 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> sum_ n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( ( w ` k ) x. C ) x. X ) = sum_ n e. ( 1 ... N ) 0 )
430	411, 429	eqtrd 2656	. . . . . . . 8 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) = sum_ n e. ( 1 ... N ) 0 )
431	24	olci 406	. . . . . . . . 9 |- ( ( 1 ... N ) C_ ( ZZ>= ` B ) \/ ( 1 ... N ) e. Fin )
432		sumz 14453	. . . . . . . . 9 |- ( ( ( 1 ... N ) C_ ( ZZ>= ` B ) \/ ( 1 ... N ) e. Fin ) -> sum_ n e. ( 1 ... N ) 0 = 0 )
433	431, 432	ax-mp 5	. . . . . . . 8 |- sum_ n e. ( 1 ... N ) 0 = 0
434	430, 433	syl6eq 2672	. . . . . . 7 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( A ^ k ) ) = 0 )
435	385, 434	eqtrd 2656	. . . . . 6 |- ( ( ph /\ ( w : ( 0 ... N ) --> QQ /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = 0 )
436	435	adantrlr 759	. . . . 5 |- ( ( ph /\ ( ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = 0 )
437		fveq1 6190	. . . . . . 7 |- ( x = ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) -> ( x ` A ) = ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) )
438	437	eqeq1d 2624	. . . . . 6 |- ( x = ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) -> ( ( x ` A ) = 0 <-> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = 0 ) )
439	438	rspcev 3309	. . . . 5 |- ( ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) e. ( (Poly ` QQ ) \ { 0p } ) /\ ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( w ` k ) x. ( y ^ k ) ) ) ` A ) = 0 ) -> E. x e. ( (Poly ` QQ ) \ { 0p } ) ( x ` A ) = 0 )
440	377, 436, 439	syl2anc 693	. . . 4 |- ( ( ph /\ ( ( w : ( 0 ... N ) --> QQ /\ w =/= ( ( 0 ... N ) X. { 0 } ) ) /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> E. x e. ( (Poly ` QQ ) \ { 0p } ) ( x ` A ) = 0 )
441	278, 440	sylanr1 684	. . 3 |- ( ( ph /\ ( w e. ( ( QQ ^m ( 0 ... N ) ) \ { ( ( 0 ... N ) X. { 0 } ) } ) /\ A. n e. ( 1 ... N ) sum_ k e. ( 0 ... N ) ( ( w ` k ) x. C ) = 0 ) ) -> E. x e. ( (Poly ` QQ ) \ { 0p } ) ( x ` A ) = 0 )
442	275, 441	rexlimddv 3035	. 2 |- ( ph -> E. x e. ( (Poly ` QQ ) \ { 0p } ) ( x ` A ) = 0 )
443		elqaa 24077	. 2 |- ( A e. AA <-> ( A e. CC /\ E. x e. ( (Poly ` QQ ) \ { 0p } ) ( x ` A ) = 0 ) )
444	1, 442, 443	sylanbrc 698	1 |- ( ph -> A e. AA )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   e/ wnel 2897   A.wral 2912   E.wrex 2913   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   ran crn 5115   |` cres 5116   "cima 5117   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   oFcof 6895   ^m cmap 7857   ~~ cen 7952   ~<_ cdom 7953   Fincfn 7955   CCcc 9934   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   QQcq 11788   ...cfz 12326   ^cexp 12860   #chash 13117   sum_csu 14416   Basecbs 15857   ↾_s cress 15858   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   0gc0g 16100   gsum_g cgsu 16101  Moorecmre 16242  mrClscmrc 16243  mrIndcmri 16244  ACScacs 16245   Ringcrg 18547   DivRingcdr 18747   LModclmod 18863   LSubSpclss 18932   LSpanclspn 18971  LBasisclbs 19074   LVecclvec 19102  NzRingcnzr 19257  ℂ_fldccnfld 19746   freeLMod cfrlm 20090   unitVec cuvc 20121   LIndF clindf 20143  LIndSclinds 20144   0pc0p 23436  Polycply 23940  coeffccoe 23942   AAcaa 24069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-sum 14417  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-0g 16102  df-gsum 16103  df-prds 16108  df-pws 16110  df-mre 16246  df-mrc 16247  df-mri 16248  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-ghm 17658  df-cntz 17750  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-oppr 18623  df-dvdsr 18641  df-unit 18642  df-invr 18672  df-dvr 18683  df-drng 18749  df-subrg 18778  df-lmod 18865  df-lss 18933  df-lsp 18972  df-lmhm 19022  df-lbs 19075  df-lvec 19103  df-sra 19172  df-rgmod 19173  df-nzr 19258  df-cnfld 19747  df-dsmm 20076  df-frlm 20091  df-uvc 20122  df-lindf 20145  df-linds 20146  df-0p 23437  df-ply 23944  df-coe 23946  df-dgr 23947  df-aa 24070

This theorem is referenced by: (None)