aacllem

	Ref	Expression
Hypotheses	aacllem.0	$⊢ φ \to A \in ℂ$
	aacllem.1	$⊢ φ \to N \in ℕ_{0}$
	aacllem.2	$⊢ (φ \land n \in (1 \dots N)) \to X \in ℂ$
	aacllem.3	$⊢ (φ \land k \in (0 \dots N) \land n \in (1 \dots N)) \to C \in ℚ$
	aacllem.4	$⊢ (φ \land k \in (0 \dots N)) \to A^{k} = \sum_{n = 1}^{N} C X$
Assertion	aacllem	$⊢ φ \to A \in 𝔸$

Proof

Step	Hyp	Ref	Expression
1		aacllem.0	$⊢ φ \to A \in ℂ$
2		aacllem.1	$⊢ φ \to N \in ℕ_{0}$
3		aacllem.2	$⊢ (φ \land n \in (1 \dots N)) \to X \in ℂ$
4		aacllem.3	$⊢ (φ \land k \in (0 \dots N) \land n \in (1 \dots N)) \to C \in ℚ$
5		aacllem.4	$⊢ (φ \land k \in (0 \dots N)) \to A^{k} = \sum_{n = 1}^{N} C X$
6	2	nn0red	$⊢ φ \to N \in ℝ$
7	6	ltp1d	$⊢ φ \to N < N + 1$
8		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
9	2 8	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
10	9	nn0red	$⊢ φ \to N + 1 \in ℝ$
11	6 10	ltnled	$⊢ φ \to (N < N + 1 \leftrightarrow \neg N + 1 \leq N)$
12	7 11	mpbid	$⊢ φ \to \neg N + 1 \leq N$
13	4	3expa	$⊢ ((φ \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to C \in ℚ$
14	13	fmpttd	$⊢ (φ \land k \in (0 \dots N)) \to (n \in (1 \dots N) ⟼ C) : (1 \dots N) ⟶ ℚ$
15		qex	$⊢ ℚ \in V$
16		ovex	$⊢ (1 \dots N) \in V$
17	15 16	elmap	$⊢ (n \in (1 \dots N) ⟼ C) \in (ℚ^{(1 \dots N)}) \leftrightarrow (n \in (1 \dots N) ⟼ C) : (1 \dots N) ⟶ ℚ$
18	14 17	sylibr	$⊢ (φ \land k \in (0 \dots N)) \to (n \in (1 \dots N) ⟼ C) \in (ℚ^{(1 \dots N)})$
19	18	fmpttd	$⊢ φ \to (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) ⟶ ℚ^{(1 \dots N)}$
20		eqid	$⊢ ℂ_{fld} ↾_{𝑠} ℚ = ℂ_{fld} ↾_{𝑠} ℚ$
21	20	qdrng	$⊢ ℂ_{fld} ↾_{𝑠} ℚ \in DivRing$
22		drngring	$⊢ ℂ_{fld} ↾_{𝑠} ℚ \in DivRing \to ℂ_{fld} ↾_{𝑠} ℚ \in Ring$
23	21 22	ax-mp	$⊢ ℂ_{fld} ↾_{𝑠} ℚ \in Ring$
24		fzfi	$⊢ (1 \dots N) \in Fin$
25		eqid	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) = (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)$
26	25	frlmlmod	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ \in Ring \land (1 \dots N) \in Fin) \to (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LMod$
27	23 24 26	mp2an	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LMod$
28		fzfi	$⊢ (0 \dots N) \in Fin$
29	20	qrngbas	$⊢ ℚ = {Base}_{(ℂ_{fld} ↾_{𝑠} ℚ)}$
30	25 29	frlmfibas	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ \in DivRing \land (1 \dots N) \in Fin) \to ℚ^{(1 \dots N)} = {Base}_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}$
31	21 24 30	mp2an	$⊢ ℚ^{(1 \dots N)} = {Base}_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}$
32	25	frlmsca	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ \in DivRing \land (1 \dots N) \in Fin) \to ℂ_{fld} ↾_{𝑠} ℚ = Scalar ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))$
33	21 24 32	mp2an	$⊢ ℂ_{fld} ↾_{𝑠} ℚ = Scalar ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))$
34		eqid	$⊢ \cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))} = \cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}$
35	20	qrng0	$⊢ 0 = 0_{(ℂ_{fld} ↾_{𝑠} ℚ)}$
36	25 35	frlm0	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ \in Ring \land (1 \dots N) \in Fin) \to (1 \dots N) \times \{0\} = 0_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}$
37	23 24 36	mp2an	$⊢ (1 \dots N) \times \{0\} = 0_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}$
38		eqid	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (0 \dots N) = (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (0 \dots N)$
39	38 29	frlmfibas	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ \in DivRing \land (0 \dots N) \in Fin) \to ℚ^{(0 \dots N)} = {Base}_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (0 \dots N))}$
40	21 28 39	mp2an	$⊢ ℚ^{(0 \dots N)} = {Base}_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (0 \dots N))}$
41	31 33 34 37 35 40	islindf4	$⊢ ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LMod \land (0 \dots N) \in Fin \land (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) ⟶ ℚ^{(1 \dots N)}) \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) LIndF ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \leftrightarrow \forall w \in (ℚ^{(0 \dots N)}) (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = (1 \dots N) \times \{0\} \to w = (0 \dots N) \times \{0\}))$
42	27 28 41	mp3an12	$⊢ (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) ⟶ ℚ^{(1 \dots N)} \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) LIndF ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \leftrightarrow \forall w \in (ℚ^{(0 \dots N)}) (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = (1 \dots N) \times \{0\} \to w = (0 \dots N) \times \{0\}))$
43	19 42	syl	$⊢ φ \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) LIndF ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \leftrightarrow \forall w \in (ℚ^{(0 \dots N)}) (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = (1 \dots N) \times \{0\} \to w = (0 \dots N) \times \{0\}))$
44		elmapi	$⊢ w \in (ℚ^{(0 \dots N)}) \to w : (0 \dots N) ⟶ ℚ$
45		fzfid	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (0 \dots N) \in Fin$
46		fvexd	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to w (k) \in V$
47	16	mptex	$⊢ (n \in (1 \dots N) ⟼ C) \in V$
48	47	a1i	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to (n \in (1 \dots N) ⟼ C) \in V$
49		simpr	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to w : (0 \dots N) ⟶ ℚ$
50	49	feqmptd	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to w = (k \in (0 \dots N) ⟼ w (k))$
51		eqidd	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) = (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))$
52	45 46 48 50 51	offval2	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) = (k \in (0 \dots N) ⟼ w (k) \cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))} (n \in (1 \dots N) ⟼ C))$
53		fzfid	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to (1 \dots N) \in Fin$
54		ffvelrn	$⊢ (w : (0 \dots N) ⟶ ℚ \land k \in (0 \dots N)) \to w (k) \in ℚ$
55	54	adantll	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to w (k) \in ℚ$
56	18	adantlr	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to (n \in (1 \dots N) ⟼ C) \in (ℚ^{(1 \dots N)})$
57		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
58	20 57	ressmulr	$⊢ ℚ \in V \to \times = \cdot_{(ℂ_{fld} ↾_{𝑠} ℚ)}$
59	15 58	ax-mp	$⊢ \times = \cdot_{(ℂ_{fld} ↾_{𝑠} ℚ)}$
60	25 31 29 53 55 56 34 59	frlmvscafval	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to w (k) \cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))} (n \in (1 \dots N) ⟼ C) = ((1 \dots N) \times \{w (k)\}) \times_{f} (n \in (1 \dots N) ⟼ C)$
61		fvexd	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to w (k) \in V$
62	13	adantllr	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to C \in ℚ$
63		fconstmpt	$⊢ (1 \dots N) \times \{w (k)\} = (n \in (1 \dots N) ⟼ w (k))$
64	63	a1i	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to (1 \dots N) \times \{w (k)\} = (n \in (1 \dots N) ⟼ w (k))$
65		eqidd	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to (n \in (1 \dots N) ⟼ C) = (n \in (1 \dots N) ⟼ C)$
66	53 61 62 64 65	offval2	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to ((1 \dots N) \times \{w (k)\}) \times_{f} (n \in (1 \dots N) ⟼ C) = (n \in (1 \dots N) ⟼ w (k) C)$
67	60 66	eqtrd	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to w (k) \cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))} (n \in (1 \dots N) ⟼ C) = (n \in (1 \dots N) ⟼ w (k) C)$
68	67	mpteq2dva	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (k \in (0 \dots N) ⟼ w (k) \cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))} (n \in (1 \dots N) ⟼ C)) = (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ w (k) C))$
69	52 68	eqtrd	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) = (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ w (k) C))$
70	69	oveq2d	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to \sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = {\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}}_{k = 0}^{N} (n \in (1 \dots N) ⟼ w (k) C)$
71		fzfid	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (1 \dots N) \in Fin$
72	23	a1i	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to ℂ_{fld} ↾_{𝑠} ℚ \in Ring$
73	55	adantlr	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \land k \in (0 \dots N)) \to w (k) \in ℚ$
74	13	an32s	$⊢ ((φ \land n \in (1 \dots N)) \land k \in (0 \dots N)) \to C \in ℚ$
75	74	adantllr	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \land k \in (0 \dots N)) \to C \in ℚ$
76		qmulcl	$⊢ (w (k) \in ℚ \land C \in ℚ) \to w (k) C \in ℚ$
77	73 75 76	syl2anc	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \land k \in (0 \dots N)) \to w (k) C \in ℚ$
78	77	an32s	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to w (k) C \in ℚ$
79	78	fmpttd	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to (n \in (1 \dots N) ⟼ w (k) C) : (1 \dots N) ⟶ ℚ$
80	15 16	elmap	$⊢ (n \in (1 \dots N) ⟼ w (k) C) \in (ℚ^{(1 \dots N)}) \leftrightarrow (n \in (1 \dots N) ⟼ w (k) C) : (1 \dots N) ⟶ ℚ$
81	79 80	sylibr	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to (n \in (1 \dots N) ⟼ w (k) C) \in (ℚ^{(1 \dots N)})$
82		eqid	$⊢ (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ w (k) C)) = (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ w (k) C))$
83	16	mptex	$⊢ (n \in (1 \dots N) ⟼ w (k) C) \in V$
84	83	a1i	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to (n \in (1 \dots N) ⟼ w (k) C) \in V$
85		snex	$⊢ \{0\} \in V$
86	16 85	xpex	$⊢ (1 \dots N) \times \{0\} \in V$
87	86	a1i	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (1 \dots N) \times \{0\} \in V$
88	82 45 84 87	fsuppmptdm	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to {finSupp}_{((1 \dots N) \times \{0\})} ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ w (k) C)))$
89	25 31 37 71 45 72 81 88	frlmgsum	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to {\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}}_{k = 0}^{N} (n \in (1 \dots N) ⟼ w (k) C) = (n \in (1 \dots N) ⟼ {\sum_{ℂ_{fld} ↾_{𝑠} ℚ}}_{k = 0}^{N} w (k) C)$
90		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
91		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
92		cnfldex	$⊢ ℂ_{fld} \in V$
93	92	a1i	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to ℂ_{fld} \in V$
94		fzfid	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to (0 \dots N) \in Fin$
95		qsscn	$⊢ ℚ \subseteq ℂ$
96	95	a1i	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to ℚ \subseteq ℂ$
97	77	fmpttd	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to (k \in (0 \dots N) ⟼ w (k) C) : (0 \dots N) ⟶ ℚ$
98		0z	$⊢ 0 \in ℤ$
99		zq	$⊢ 0 \in ℤ \to 0 \in ℚ$
100	98 99	ax-mp	$⊢ 0 \in ℚ$
101	100	a1i	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to 0 \in ℚ$
102		addid2	$⊢ x \in ℂ \to 0 + x = x$
103		addid1	$⊢ x \in ℂ \to x + 0 = x$
104	102 103	jca	$⊢ x \in ℂ \to (0 + x = x \land x + 0 = x)$
105	104	adantl	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \land x \in ℂ) \to (0 + x = x \land x + 0 = x)$
106	90 91 20 93 94 96 97 101 105	gsumress	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to {\sum_{ℂ_{fld}}}_{k = 0}^{N} w (k) C = {\sum_{ℂ_{fld} ↾_{𝑠} ℚ}}_{k = 0}^{N} w (k) C$
107		simplr	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to w : (0 \dots N) ⟶ ℚ$
108		qcn	$⊢ w (k) \in ℚ \to w (k) \in ℂ$
109	54 108	syl	$⊢ (w : (0 \dots N) ⟶ ℚ \land k \in (0 \dots N)) \to w (k) \in ℂ$
110	107 109	sylan	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \land k \in (0 \dots N)) \to w (k) \in ℂ$
111		qcn	$⊢ C \in ℚ \to C \in ℂ$
112	13 111	syl	$⊢ ((φ \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to C \in ℂ$
113	112	an32s	$⊢ ((φ \land n \in (1 \dots N)) \land k \in (0 \dots N)) \to C \in ℂ$
114	113	adantllr	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \land k \in (0 \dots N)) \to C \in ℂ$
115	110 114	mulcld	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \land k \in (0 \dots N)) \to w (k) C \in ℂ$
116	94 115	gsumfsum	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to {\sum_{ℂ_{fld}}}_{k = 0}^{N} w (k) C = \sum_{k = 0}^{N} w (k) C$
117	106 116	eqtr3d	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to {\sum_{ℂ_{fld} ↾_{𝑠} ℚ}}_{k = 0}^{N} w (k) C = \sum_{k = 0}^{N} w (k) C$
118	117	mpteq2dva	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (n \in (1 \dots N) ⟼ {\sum_{ℂ_{fld} ↾_{𝑠} ℚ}}_{k = 0}^{N} w (k) C) = (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C)$
119	70 89 118	3eqtrd	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to \sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C)$
120		qaddcl	$⊢ (x \in ℚ \land y \in ℚ) \to x + y \in ℚ$
121	120	adantl	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \land (x \in ℚ \land y \in ℚ)) \to x + y \in ℚ$
122	96 121 94 77 101	fsumcllem	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to \sum_{k = 0}^{N} w (k) C \in ℚ$
123	122	fmpttd	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C) : (1 \dots N) ⟶ ℚ$
124	15 16	elmap	$⊢ (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C) \in (ℚ^{(1 \dots N)}) \leftrightarrow (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C) : (1 \dots N) ⟶ ℚ$
125	123 124	sylibr	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C) \in (ℚ^{(1 \dots N)})$
126	119 125	eqeltrd	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to \sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) \in (ℚ^{(1 \dots N)})$
127		elmapi	$⊢ \sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) \in (ℚ^{(1 \dots N)}) \to (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) : (1 \dots N) ⟶ ℚ$
128		ffn	$⊢ (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) : (1 \dots N) ⟶ ℚ \to (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) Fn (1 \dots N)$
129	126 127 128	3syl	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) Fn (1 \dots N)$
130		c0ex	$⊢ 0 \in V$
131		fnconstg	$⊢ 0 \in V \to ((1 \dots N) \times \{0\}) Fn (1 \dots N)$
132	130 131	ax-mp	$⊢ ((1 \dots N) \times \{0\}) Fn (1 \dots N)$
133		nfcv	$⊢ \underline{Ⅎ} n ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))$
134		nfcv	$⊢ \underline{Ⅎ} n Σ_{𝑔}$
135		nfcv	$⊢ \underline{Ⅎ} n w$
136		nfcv	$⊢ \underline{Ⅎ} n \circ_{f} \cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}$
137		nfcv	$⊢ \underline{Ⅎ} n (0 \dots N)$
138		nfmpt1	$⊢ \underline{Ⅎ} n (n \in (1 \dots N) ⟼ C)$
139	137 138	nfmpt	$⊢ \underline{Ⅎ} n (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))$
140	135 136 139	nfov	$⊢ \underline{Ⅎ} n (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))$
141	133 134 140	nfov	$⊢ \underline{Ⅎ} n (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))))$
142		nfcv	$⊢ \underline{Ⅎ} n ((1 \dots N) \times \{0\})$
143	141 142	eqfnfv2f	$⊢ ((\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) Fn (1 \dots N) \land ((1 \dots N) \times \{0\}) Fn (1 \dots N)) \to (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = (1 \dots N) \times \{0\} \leftrightarrow \forall n \in (1 \dots N) (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) (n) = ((1 \dots N) \times \{0\}) (n))$
144	129 132 143	sylancl	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = (1 \dots N) \times \{0\} \leftrightarrow \forall n \in (1 \dots N) (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) (n) = ((1 \dots N) \times \{0\}) (n))$
145	119	fveq1d	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) (n) = (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C) (n)$
146		sumex	$⊢ \sum_{k = 0}^{N} w (k) C \in V$
147		eqid	$⊢ (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C) = (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C)$
148	147	fvmpt2	$⊢ (n \in (1 \dots N) \land \sum_{k = 0}^{N} w (k) C \in V) \to (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C) (n) = \sum_{k = 0}^{N} w (k) C$
149	146 148	mpan2	$⊢ n \in (1 \dots N) \to (n \in (1 \dots N) ⟼ \sum_{k = 0}^{N} w (k) C) (n) = \sum_{k = 0}^{N} w (k) C$
150	145 149	sylan9eq	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) (n) = \sum_{k = 0}^{N} w (k) C$
151	130	fvconst2	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{0\}) (n) = 0$
152	151	adantl	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to ((1 \dots N) \times \{0\}) (n) = 0$
153	150 152	eqeq12d	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to ((\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) (n) = ((1 \dots N) \times \{0\}) (n) \leftrightarrow \sum_{k = 0}^{N} w (k) C = 0)$
154	153	ralbidva	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (\forall n \in (1 \dots N) (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)}, (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)))) (n) = ((1 \dots N) \times \{0\}) (n) \leftrightarrow \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)$
155	144 154	bitrd	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = (1 \dots N) \times \{0\} \leftrightarrow \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)$
156	155	imbi1d	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to ((\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = (1 \dots N) \times \{0\} \to w = (0 \dots N) \times \{0\}) \leftrightarrow (\forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \to w = (0 \dots N) \times \{0\}))$
157	44 156	sylan2	$⊢ (φ \land w \in (ℚ^{(0 \dots N)})) \to ((\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = (1 \dots N) \times \{0\} \to w = (0 \dots N) \times \{0\}) \leftrightarrow (\forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \to w = (0 \dots N) \times \{0\}))$
158	157	ralbidva	$⊢ φ \to (\forall w \in (ℚ^{(0 \dots N)}) (\sum_{(ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)} (w {\cdot_{((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))}}_{f} (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) = (1 \dots N) \times \{0\} \to w = (0 \dots N) \times \{0\}) \leftrightarrow \forall w \in (ℚ^{(0 \dots N)}) (\forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \to w = (0 \dots N) \times \{0\}))$
159	43 158	bitrd	$⊢ φ \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) LIndF ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \leftrightarrow \forall w \in (ℚ^{(0 \dots N)}) (\forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \to w = (0 \dots N) \times \{0\}))$
160		drngnzr	$⊢ ℂ_{fld} ↾_{𝑠} ℚ \in DivRing \to ℂ_{fld} ↾_{𝑠} ℚ \in NzRing$
161	21 160	ax-mp	$⊢ ℂ_{fld} ↾_{𝑠} ℚ \in NzRing$
162	33	islindf3	$⊢ ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LMod \land ℂ_{fld} ↾_{𝑠} ℚ \in NzRing) \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) LIndF ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \leftrightarrow ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : dom (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \underset{1-1}{⟶} V \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))))$
163	27 161 162	mp2an	$⊢ (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) LIndF ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \leftrightarrow ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : dom (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \underset{1-1}{⟶} V \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))$
164		eqid	$⊢ (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) = (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))$
165	47 164	dmmpti	$⊢ dom (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) = (0 \dots N)$
166		f1eq2	$⊢ dom (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) = (0 \dots N) \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : dom (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \underset{1-1}{⟶} V \leftrightarrow (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V)$
167	165 166	ax-mp	$⊢ (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : dom (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \underset{1-1}{⟶} V \leftrightarrow (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V$
168	167	anbi1i	$⊢ ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : dom (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \underset{1-1}{⟶} V \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \leftrightarrow ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))$
169	163 168	bitri	$⊢ (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) LIndF ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \leftrightarrow ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))$
170		con34b	$⊢ (\forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \to w = (0 \dots N) \times \{0\}) \leftrightarrow (\neg w = (0 \dots N) \times \{0\} \to \neg \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)$
171		df-nel	$⊢ w \notin \{(0 \dots N) \times \{0\}\} \leftrightarrow \neg w \in \{(0 \dots N) \times \{0\}\}$
172		velsn	$⊢ w \in \{(0 \dots N) \times \{0\}\} \leftrightarrow w = (0 \dots N) \times \{0\}$
173	171 172	xchbinx	$⊢ w \notin \{(0 \dots N) \times \{0\}\} \leftrightarrow \neg w = (0 \dots N) \times \{0\}$
174	173	imbi1i	$⊢ (w \notin \{(0 \dots N) \times \{0\}\} \to \neg \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0) \leftrightarrow (\neg w = (0 \dots N) \times \{0\} \to \neg \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)$
175	170 174	bitr4i	$⊢ (\forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \to w = (0 \dots N) \times \{0\}) \leftrightarrow (w \notin \{(0 \dots N) \times \{0\}\} \to \neg \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)$
176	175	ralbii	$⊢ \forall w \in (ℚ^{(0 \dots N)}) (\forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \to w = (0 \dots N) \times \{0\}) \leftrightarrow \forall w \in (ℚ^{(0 \dots N)}) (w \notin \{(0 \dots N) \times \{0\}\} \to \neg \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)$
177		raldifb	$⊢ \forall w \in (ℚ^{(0 \dots N)}) (w \notin \{(0 \dots N) \times \{0\}\} \to \neg \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0) \leftrightarrow \forall w \in ((ℚ^{(0 \dots N)}) ∖ \{(0 \dots N) \times \{0\}\}) \neg \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0$
178		ralnex	$⊢ \forall w \in ((ℚ^{(0 \dots N)}) ∖ \{(0 \dots N) \times \{0\}\}) \neg \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \leftrightarrow \neg \exists w \in ((ℚ^{(0 \dots N)}) ∖ \{(0 \dots N) \times \{0\}\}) \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0$
179	176 177 178	3bitri	$⊢ \forall w \in (ℚ^{(0 \dots N)}) (\forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \to w = (0 \dots N) \times \{0\}) \leftrightarrow \neg \exists w \in ((ℚ^{(0 \dots N)}) ∖ \{(0 \dots N) \times \{0\}\}) \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0$
180	159 169 179	3bitr3g	$⊢ φ \to (((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \leftrightarrow \neg \exists w \in ((ℚ^{(0 \dots N)}) ∖ \{(0 \dots N) \times \{0\}\}) \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)$
181		eqid	$⊢ LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) = LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))$
182	31 181	lssmre	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LMod \to LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \in Moore (ℚ^{(1 \dots N)})$
183	27 182	ax-mp	$⊢ LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \in Moore (ℚ^{(1 \dots N)})$
184	183	a1i	$⊢ (φ \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \to LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \in Moore (ℚ^{(1 \dots N)})$
185		eqid	$⊢ LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) = LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))$
186		eqid	$⊢ mrCls (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) = mrCls (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))$
187	181 185 186	mrclsp	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LMod \to LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) = mrCls (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))$
188	27 187	ax-mp	$⊢ LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) = mrCls (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))$
189		eqid	$⊢ mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) = mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))$
190	33	islvec	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LVec \leftrightarrow ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LMod \land ℂ_{fld} ↾_{𝑠} ℚ \in DivRing)$
191	27 21 190	mpbir2an	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LVec$
192	181 188 31	lssacsex	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LVec \to (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \in ACS (ℚ^{(1 \dots N)}) \land \forall z \in 𝒫 (ℚ^{(1 \dots N)}) \forall x \in (ℚ^{(1 \dots N)}) \forall y \in (LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z \cup \{x\}) ∖ LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z)) x \in LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z \cup \{y\}))$
193	192	simprd	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LVec \to \forall z \in 𝒫 (ℚ^{(1 \dots N)}) \forall x \in (ℚ^{(1 \dots N)}) \forall y \in (LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z \cup \{x\}) ∖ LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z)) x \in LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z \cup \{y\})$
194	191 193	ax-mp	$⊢ \forall z \in 𝒫 (ℚ^{(1 \dots N)}) \forall x \in (ℚ^{(1 \dots N)}) \forall y \in (LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z \cup \{x\}) ∖ LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z)) x \in LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z \cup \{y\})$
195	194	a1i	$⊢ (φ \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \to \forall z \in 𝒫 (ℚ^{(1 \dots N)}) \forall x \in (ℚ^{(1 \dots N)}) \forall y \in (LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z \cup \{x\}) ∖ LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z)) x \in LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (z \cup \{y\})$
196	19	frnd	$⊢ φ \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \subseteq ℚ^{(1 \dots N)}$
197		dif0	$⊢ (ℚ^{(1 \dots N)}) ∖ \emptyset = ℚ^{(1 \dots N)}$
198	196 197	sseqtrrdi	$⊢ φ \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \subseteq (ℚ^{(1 \dots N)}) ∖ \emptyset$
199	198	adantr	$⊢ (φ \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \subseteq (ℚ^{(1 \dots N)}) ∖ \emptyset$
200		eqid	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N) = (ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)$
201	200 25 31	uvcff	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ \in Ring \land (1 \dots N) \in Fin) \to ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) : (1 \dots N) ⟶ ℚ^{(1 \dots N)}$
202	23 24 201	mp2an	$⊢ ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) : (1 \dots N) ⟶ ℚ^{(1 \dots N)}$
203		frn	$⊢ ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) : (1 \dots N) ⟶ ℚ^{(1 \dots N)} \to ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \subseteq ℚ^{(1 \dots N)}$
204	202 203	ax-mp	$⊢ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \subseteq ℚ^{(1 \dots N)}$
205	204 197	sseqtrri	$⊢ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \subseteq (ℚ^{(1 \dots N)}) ∖ \emptyset$
206	205	a1i	$⊢ (φ \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \to ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \subseteq (ℚ^{(1 \dots N)}) ∖ \emptyset$
207		un0	$⊢ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \cup \emptyset = ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))$
208	207	fveq2i	$⊢ LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \cup \emptyset) = LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)))$
209		eqid	$⊢ LBasis ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) = LBasis ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))$
210	25 200 209	frlmlbs	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ \in Ring \land (1 \dots N) \in Fin) \to ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \in LBasis ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))$
211	23 24 210	mp2an	$⊢ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \in LBasis ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))$
212	31 209 185	lbssp	$⊢ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \in LBasis ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \to LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))) = ℚ^{(1 \dots N)}$
213	211 212	ax-mp	$⊢ LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))) = ℚ^{(1 \dots N)}$
214	208 213	eqtri	$⊢ LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \cup \emptyset) = ℚ^{(1 \dots N)}$
215	196 214	sseqtrrdi	$⊢ φ \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \subseteq LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \cup \emptyset)$
216	215	adantr	$⊢ (φ \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \subseteq LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \cup \emptyset)$
217		un0	$⊢ ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \cup \emptyset = ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))$
218	27 161	pm3.2i	$⊢ ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LMod \land ℂ_{fld} ↾_{𝑠} ℚ \in NzRing)$
219	185 33	lindsind2	$⊢ (((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N) \in LMod \land ℂ_{fld} ↾_{𝑠} ℚ \in NzRing) \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \land x \in ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) \to \neg x \in LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ∖ \{x\})$
220	218 219	mp3an1	$⊢ (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \land x \in ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))) \to \neg x \in LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ∖ \{x\})$
221	220	ralrimiva	$⊢ ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \to \forall x \in ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \neg x \in LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ∖ \{x\})$
222	188 189	ismri2	$⊢ (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \in Moore (ℚ^{(1 \dots N)}) \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \subseteq ℚ^{(1 \dots N)}) \to (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \leftrightarrow \forall x \in ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \neg x \in LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ∖ \{x\}))$
223	183 196 222	sylancr	$⊢ φ \to (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \leftrightarrow \forall x \in ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \neg x \in LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ∖ \{x\}))$
224	223	biimpar	$⊢ (φ \land \forall x \in ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \neg x \in LSpan ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ∖ \{x\})) \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))$
225	221 224	sylan2	$⊢ (φ \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))$
226	217 225	eqeltrid	$⊢ (φ \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \cup \emptyset \in mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))$
227		mptfi	$⊢ (0 \dots N) \in Fin \to (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in Fin$
228		rnfi	$⊢ (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in Fin \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in Fin$
229	28 227 228	mp2b	$⊢ ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in Fin$
230	229	orci	$⊢ (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in Fin \lor ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \in Fin)$
231	230	a1i	$⊢ (φ \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \to (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in Fin \lor ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \in Fin)$
232	184 188 189 195 199 206 216 226 231	mreexexd	$⊢ (φ \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \to \exists v \in 𝒫 ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \approx v \land v \cup \emptyset \in mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))))$
233	232	ex	$⊢ φ \to (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \to \exists v \in 𝒫 ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \approx v \land v \cup \emptyset \in mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))))$
234		ovex	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N) \in V$
235	234	rnex	$⊢ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \in V$
236		elpwi	$⊢ v \in 𝒫 ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \to v \subseteq ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))$
237		ssdomg	$⊢ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \in V \to (v \subseteq ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \to v ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)))$
238	235 236 237	mpsyl	$⊢ v \in 𝒫 ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \to v ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))$
239		endomtr	$⊢ (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \approx v \land v ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))) \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))$
240	239	ancoms	$⊢ (v ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \approx v) \to ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))$
241		f1f1orn	$⊢ (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \to (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1 onto}{⟶} ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))$
242		ovex	$⊢ (0 \dots N) \in V$
243	242	f1oen	$⊢ (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1 onto}{⟶} ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \to (0 \dots N) \approx ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))$
244	241 243	syl	$⊢ (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \to (0 \dots N) \approx ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C))$
245		endomtr	$⊢ ((0 \dots N) \approx ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))) \to (0 \dots N) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))$
246	200	uvcendim	$⊢ (ℂ_{fld} ↾_{𝑠} ℚ \in NzRing \land (1 \dots N) \in Fin) \to (1 \dots N) \approx ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))$
247	161 24 246	mp2an	$⊢ (1 \dots N) \approx ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))$
248	247	ensymi	$⊢ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \approx (1 \dots N)$
249		domentr	$⊢ ((0 \dots N) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \land ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \approx (1 \dots N)) \to (0 \dots N) ≼ (1 \dots N)$
250		hashdom	$⊢ ((0 \dots N) \in Fin \land (1 \dots N) \in Fin) \to (\|(0 \dots N)\| \leq \|(1 \dots N)\| \leftrightarrow (0 \dots N) ≼ (1 \dots N))$
251	28 24 250	mp2an	$⊢ \|(0 \dots N)\| \leq \|(1 \dots N)\| \leftrightarrow (0 \dots N) ≼ (1 \dots N)$
252		hashfz0	$⊢ N \in ℕ_{0} \to \|(0 \dots N)\| = N + 1$
253	2 252	syl	$⊢ φ \to \|(0 \dots N)\| = N + 1$
254		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
255	2 254	syl	$⊢ φ \to \|(1 \dots N)\| = N$
256	253 255	breq12d	$⊢ φ \to (\|(0 \dots N)\| \leq \|(1 \dots N)\| \leftrightarrow N + 1 \leq N)$
257	251 256	bitr3id	$⊢ φ \to ((0 \dots N) ≼ (1 \dots N) \leftrightarrow N + 1 \leq N)$
258	249 257	syl5ib	$⊢ φ \to (((0 \dots N) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \land ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \approx (1 \dots N)) \to N + 1 \leq N)$
259	248 258	mpan2i	$⊢ φ \to ((0 \dots N) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \to N + 1 \leq N)$
260	245 259	syl5	$⊢ φ \to (((0 \dots N) \approx ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))) \to N + 1 \leq N)$
261	260	expd	$⊢ φ \to ((0 \dots N) \approx ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \to (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \to N + 1 \leq N))$
262	244 261	syl5	$⊢ φ \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \to (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \to N + 1 \leq N))$
263	262	com23	$⊢ φ \to (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \to N + 1 \leq N))$
264	240 263	syl5	$⊢ φ \to ((v ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \approx v) \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \to N + 1 \leq N))$
265	264	expdimp	$⊢ (φ \land v ≼ ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))) \to (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \approx v \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \to N + 1 \leq N))$
266	238 265	sylan2	$⊢ (φ \land v \in 𝒫 ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))) \to (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \approx v \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \to N + 1 \leq N))$
267	266	adantrd	$⊢ (φ \land v \in 𝒫 ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N))) \to ((ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \approx v \land v \cup \emptyset \in mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))) \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \to N + 1 \leq N))$
268	267	rexlimdva	$⊢ φ \to (\exists v \in 𝒫 ran ((ℂ_{fld} ↾_{𝑠} ℚ) unitVec (1 \dots N)) (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \approx v \land v \cup \emptyset \in mrInd (LSubSp ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)))) \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \to N + 1 \leq N))$
269	233 268	syld	$⊢ φ \to (ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \to ((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \to N + 1 \leq N))$
270	269	impd	$⊢ φ \to ((ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N)) \land (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V) \to N + 1 \leq N)$
271	270	ancomsd	$⊢ φ \to (((k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) : (0 \dots N) \underset{1-1}{⟶} V \land ran (k \in (0 \dots N) ⟼ (n \in (1 \dots N) ⟼ C)) \in LIndS ((ℂ_{fld} ↾_{𝑠} ℚ) freeLMod (1 \dots N))) \to N + 1 \leq N)$
272	180 271	sylbird	$⊢ φ \to (\neg \exists w \in ((ℚ^{(0 \dots N)}) ∖ \{(0 \dots N) \times \{0\}\}) \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \to N + 1 \leq N)$
273	12 272	mt3d	$⊢ φ \to \exists w \in ((ℚ^{(0 \dots N)}) ∖ \{(0 \dots N) \times \{0\}\}) \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0$
274		eldifsn	$⊢ w \in ((ℚ^{(0 \dots N)}) ∖ \{(0 \dots N) \times \{0\}\}) \leftrightarrow (w \in (ℚ^{(0 \dots N)}) \land w \neq (0 \dots N) \times \{0\})$
275	44	anim1i	$⊢ (w \in (ℚ^{(0 \dots N)}) \land w \neq (0 \dots N) \times \{0\}) \to (w : (0 \dots N) ⟶ ℚ \land w \neq (0 \dots N) \times \{0\})$
276	274 275	sylbi	$⊢ w \in ((ℚ^{(0 \dots N)}) ∖ \{(0 \dots N) \times \{0\}\}) \to (w : (0 \dots N) ⟶ ℚ \land w \neq (0 \dots N) \times \{0\})$
277	95	a1i	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to ℚ \subseteq ℂ$
278	2	adantr	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to N \in ℕ_{0}$
279	277 278 55	elplyd	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \in Poly (ℚ)$
280	279	adantrr	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land w \neq (0 \dots N) \times \{0\})) \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \in Poly (ℚ)$
281		uzdisj	$⊢ (0 \dots N + 1 - 1) \cap ℤ_{\geq (N + 1)} = \emptyset$
282	2	nn0cnd	$⊢ φ \to N \in ℂ$
283		pncan1	$⊢ N \in ℂ \to N + 1 - 1 = N$
284	282 283	syl	$⊢ φ \to N + 1 - 1 = N$
285	284	oveq2d	$⊢ φ \to (0 \dots N + 1 - 1) = (0 \dots N)$
286	285	ineq1d	$⊢ φ \to (0 \dots N + 1 - 1) \cap ℤ_{\geq (N + 1)} = (0 \dots N) \cap ℤ_{\geq (N + 1)}$
287	281 286	eqtr3id	$⊢ φ \to \emptyset = (0 \dots N) \cap ℤ_{\geq (N + 1)}$
288	287	eqcomd	$⊢ φ \to (0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset$
289	130	fconst	$⊢ (ℤ_{\geq (N + 1)} \times \{0\}) : ℤ_{\geq (N + 1)} ⟶ \{0\}$
290		snssi	$⊢ 0 \in ℚ \to \{0\} \subseteq ℚ$
291	98 99 290	mp2b	$⊢ \{0\} \subseteq ℚ$
292	291 95	sstri	$⊢ \{0\} \subseteq ℂ$
293		fss	$⊢ ((ℤ_{\geq (N + 1)} \times \{0\}) : ℤ_{\geq (N + 1)} ⟶ \{0\} \land \{0\} \subseteq ℂ) \to (ℤ_{\geq (N + 1)} \times \{0\}) : ℤ_{\geq (N + 1)} ⟶ ℂ$
294	289 292 293	mp2an	$⊢ (ℤ_{\geq (N + 1)} \times \{0\}) : ℤ_{\geq (N + 1)} ⟶ ℂ$
295		fun	$⊢ ((w : (0 \dots N) ⟶ ℚ \land (ℤ_{\geq (N + 1)} \times \{0\}) : ℤ_{\geq (N + 1)} ⟶ ℂ) \land (0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset) \to (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) : (0 \dots N) \cup ℤ_{\geq (N + 1)} ⟶ ℚ \cup ℂ$
296	294 295	mpanl2	$⊢ (w : (0 \dots N) ⟶ ℚ \land (0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset) \to (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) : (0 \dots N) \cup ℤ_{\geq (N + 1)} ⟶ ℚ \cup ℂ$
297	288 296	sylan2	$⊢ (w : (0 \dots N) ⟶ ℚ \land φ) \to (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) : (0 \dots N) \cup ℤ_{\geq (N + 1)} ⟶ ℚ \cup ℂ$
298	297	ancoms	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) : (0 \dots N) \cup ℤ_{\geq (N + 1)} ⟶ ℚ \cup ℂ$
299		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
300	9 299	eleqtrdi	$⊢ φ \to N + 1 \in ℤ_{\geq 0}$
301		uzsplit	$⊢ N + 1 \in ℤ_{\geq 0} \to ℤ_{\geq 0} = (0 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)}$
302	300 301	syl	$⊢ φ \to ℤ_{\geq 0} = (0 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)}$
303	299 302	eqtrid	$⊢ φ \to ℕ_{0} = (0 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)}$
304	285	uneq1d	$⊢ φ \to (0 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)} = (0 \dots N) \cup ℤ_{\geq (N + 1)}$
305	303 304	eqtr2d	$⊢ φ \to (0 \dots N) \cup ℤ_{\geq (N + 1)} = ℕ_{0}$
306		ssequn1	$⊢ ℚ \subseteq ℂ \leftrightarrow ℚ \cup ℂ = ℂ$
307	95 306	mpbi	$⊢ ℚ \cup ℂ = ℂ$
308	307	a1i	$⊢ φ \to ℚ \cup ℂ = ℂ$
309	305 308	feq23d	$⊢ φ \to ((w \cup (ℤ_{\geq (N + 1)} \times \{0\})) : (0 \dots N) \cup ℤ_{\geq (N + 1)} ⟶ ℚ \cup ℂ \leftrightarrow (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) : ℕ_{0} ⟶ ℂ)$
310	309	adantr	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to ((w \cup (ℤ_{\geq (N + 1)} \times \{0\})) : (0 \dots N) \cup ℤ_{\geq (N + 1)} ⟶ ℚ \cup ℂ \leftrightarrow (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) : ℕ_{0} ⟶ ℂ)$
311	298 310	mpbid	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) : ℕ_{0} ⟶ ℂ$
312		ffn	$⊢ w : (0 \dots N) ⟶ ℚ \to w Fn (0 \dots N)$
313		fnimadisj	$⊢ (w Fn (0 \dots N) \land (0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset) \to w [ℤ_{\geq (N + 1)}] = \emptyset$
314	312 288 313	syl2anr	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to w [ℤ_{\geq (N + 1)}] = \emptyset$
315	2	nn0zd	$⊢ φ \to N \in ℤ$
316	315	peano2zd	$⊢ φ \to N + 1 \in ℤ$
317		uzid	$⊢ N + 1 \in ℤ \to N + 1 \in ℤ_{\geq (N + 1)}$
318		ne0i	$⊢ N + 1 \in ℤ_{\geq (N + 1)} \to ℤ_{\geq (N + 1)} \neq \emptyset$
319	316 317 318	3syl	$⊢ φ \to ℤ_{\geq (N + 1)} \neq \emptyset$
320		inidm	$⊢ ℤ_{\geq (N + 1)} \cap ℤ_{\geq (N + 1)} = ℤ_{\geq (N + 1)}$
321	320	neeq1i	$⊢ ℤ_{\geq (N + 1)} \cap ℤ_{\geq (N + 1)} \neq \emptyset \leftrightarrow ℤ_{\geq (N + 1)} \neq \emptyset$
322	319 321	sylibr	$⊢ φ \to ℤ_{\geq (N + 1)} \cap ℤ_{\geq (N + 1)} \neq \emptyset$
323		xpima2	$⊢ ℤ_{\geq (N + 1)} \cap ℤ_{\geq (N + 1)} \neq \emptyset \to (ℤ_{\geq (N + 1)} \times \{0\}) [ℤ_{\geq (N + 1)}] = \{0\}$
324	322 323	syl	$⊢ φ \to (ℤ_{\geq (N + 1)} \times \{0\}) [ℤ_{\geq (N + 1)}] = \{0\}$
325	324	adantr	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (ℤ_{\geq (N + 1)} \times \{0\}) [ℤ_{\geq (N + 1)}] = \{0\}$
326	314 325	uneq12d	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to w [ℤ_{\geq (N + 1)}] \cup (ℤ_{\geq (N + 1)} \times \{0\}) [ℤ_{\geq (N + 1)}] = \emptyset \cup \{0\}$
327		imaundir	$⊢ (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) [ℤ_{\geq (N + 1)}] = w [ℤ_{\geq (N + 1)}] \cup (ℤ_{\geq (N + 1)} \times \{0\}) [ℤ_{\geq (N + 1)}]$
328		uncom	$⊢ \emptyset \cup \{0\} = \{0\} \cup \emptyset$
329		un0	$⊢ \{0\} \cup \emptyset = \{0\}$
330	328 329	eqtr2i	$⊢ \{0\} = \emptyset \cup \{0\}$
331	326 327 330	3eqtr4g	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) [ℤ_{\geq (N + 1)}] = \{0\}$
332	288 312	anim12ci	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (w Fn (0 \dots N) \land (0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset)$
333		fnconstg	$⊢ 0 \in V \to (ℤ_{\geq (N + 1)} \times \{0\}) Fn ℤ_{\geq (N + 1)}$
334	130 333	ax-mp	$⊢ (ℤ_{\geq (N + 1)} \times \{0\}) Fn ℤ_{\geq (N + 1)}$
335		fvun1	$⊢ (w Fn (0 \dots N) \land (ℤ_{\geq (N + 1)} \times \{0\}) Fn ℤ_{\geq (N + 1)} \land ((0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset \land k \in (0 \dots N))) \to (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) (k) = w (k)$
336	334 335	mp3an2	$⊢ (w Fn (0 \dots N) \land ((0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset \land k \in (0 \dots N))) \to (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) (k) = w (k)$
337	336	anassrs	$⊢ ((w Fn (0 \dots N) \land (0 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset) \land k \in (0 \dots N)) \to (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) (k) = w (k)$
338	332 337	sylan	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) (k) = w (k)$
339	338	eqcomd	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to w (k) = (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) (k)$
340	339	oveq1d	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to w (k) y^{k} = (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) (k) y^{k}$
341	340	sumeq2dv	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to \sum_{k = 0}^{N} w (k) y^{k} = \sum_{k = 0}^{N} (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) (k) y^{k}$
342	341	mpteq2dv	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) = (y \in ℂ ⟼ \sum_{k = 0}^{N} (w \cup (ℤ_{\geq (N + 1)} \times \{0\})) (k) y^{k})$
343	279 278 311 331 342	coeeq	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) = w \cup (ℤ_{\geq (N + 1)} \times \{0\})$
344	343	reseq1d	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to {coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) ↾}_{(0 \dots N)} = {(w \cup (ℤ_{\geq (N + 1)} \times \{0\})) ↾}_{(0 \dots N)}$
345		res0	$⊢ {w ↾}_{\emptyset} = \emptyset$
346	287	reseq2d	$⊢ φ \to {w ↾}_{\emptyset} = {w ↾}_{((0 \dots N) \cap ℤ_{\geq (N + 1)})}$
347		res0	$⊢ {(ℤ_{\geq (N + 1)} \times \{0\}) ↾}_{\emptyset} = \emptyset$
348	287	reseq2d	$⊢ φ \to {(ℤ_{\geq (N + 1)} \times \{0\}) ↾}_{\emptyset} = {(ℤ_{\geq (N + 1)} \times \{0\}) ↾}_{((0 \dots N) \cap ℤ_{\geq (N + 1)})}$
349	347 348	eqtr3id	$⊢ φ \to \emptyset = {(ℤ_{\geq (N + 1)} \times \{0\}) ↾}_{((0 \dots N) \cap ℤ_{\geq (N + 1)})}$
350	345 346 349	3eqtr3a	$⊢ φ \to {w ↾}_{((0 \dots N) \cap ℤ_{\geq (N + 1)})} = {(ℤ_{\geq (N + 1)} \times \{0\}) ↾}_{((0 \dots N) \cap ℤ_{\geq (N + 1)})}$
351		fss	$⊢ ((ℤ_{\geq (N + 1)} \times \{0\}) : ℤ_{\geq (N + 1)} ⟶ \{0\} \land \{0\} \subseteq ℚ) \to (ℤ_{\geq (N + 1)} \times \{0\}) : ℤ_{\geq (N + 1)} ⟶ ℚ$
352	289 291 351	mp2an	$⊢ (ℤ_{\geq (N + 1)} \times \{0\}) : ℤ_{\geq (N + 1)} ⟶ ℚ$
353		fresaunres1	$⊢ (w : (0 \dots N) ⟶ ℚ \land (ℤ_{\geq (N + 1)} \times \{0\}) : ℤ_{\geq (N + 1)} ⟶ ℚ \land {w ↾}_{((0 \dots N) \cap ℤ_{\geq (N + 1)})} = {(ℤ_{\geq (N + 1)} \times \{0\}) ↾}_{((0 \dots N) \cap ℤ_{\geq (N + 1)})}) \to {(w \cup (ℤ_{\geq (N + 1)} \times \{0\})) ↾}_{(0 \dots N)} = w$
354	352 353	mp3an2	$⊢ (w : (0 \dots N) ⟶ ℚ \land {w ↾}_{((0 \dots N) \cap ℤ_{\geq (N + 1)})} = {(ℤ_{\geq (N + 1)} \times \{0\}) ↾}_{((0 \dots N) \cap ℤ_{\geq (N + 1)})}) \to {(w \cup (ℤ_{\geq (N + 1)} \times \{0\})) ↾}_{(0 \dots N)} = w$
355	350 354	sylan2	$⊢ (w : (0 \dots N) ⟶ ℚ \land φ) \to {(w \cup (ℤ_{\geq (N + 1)} \times \{0\})) ↾}_{(0 \dots N)} = w$
356	355	ancoms	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to {(w \cup (ℤ_{\geq (N + 1)} \times \{0\})) ↾}_{(0 \dots N)} = w$
357	344 356	eqtrd	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to {coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) ↾}_{(0 \dots N)} = w$
358		fveq2	$⊢ (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) = 0_{𝑝} \to coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) = coeff (0_{𝑝})$
359	358	reseq1d	$⊢ (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) = 0_{𝑝} \to {coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) ↾}_{(0 \dots N)} = {coeff (0_{𝑝}) ↾}_{(0 \dots N)}$
360		eqtr2	$⊢ ({coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) ↾}_{(0 \dots N)} = w \land {coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) ↾}_{(0 \dots N)} = {coeff (0_{𝑝}) ↾}_{(0 \dots N)}) \to w = {coeff (0_{𝑝}) ↾}_{(0 \dots N)}$
361		coe0	$⊢ coeff (0_{𝑝}) = ℕ_{0} \times \{0\}$
362	361	reseq1i	$⊢ {coeff (0_{𝑝}) ↾}_{(0 \dots N)} = {(ℕ_{0} \times \{0\}) ↾}_{(0 \dots N)}$
363		elfznn0	$⊢ x \in (0 \dots N) \to x \in ℕ_{0}$
364	363	ssriv	$⊢ (0 \dots N) \subseteq ℕ_{0}$
365		xpssres	$⊢ (0 \dots N) \subseteq ℕ_{0} \to {(ℕ_{0} \times \{0\}) ↾}_{(0 \dots N)} = (0 \dots N) \times \{0\}$
366	364 365	ax-mp	$⊢ {(ℕ_{0} \times \{0\}) ↾}_{(0 \dots N)} = (0 \dots N) \times \{0\}$
367	362 366	eqtri	$⊢ {coeff (0_{𝑝}) ↾}_{(0 \dots N)} = (0 \dots N) \times \{0\}$
368	360 367	eqtrdi	$⊢ ({coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) ↾}_{(0 \dots N)} = w \land {coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) ↾}_{(0 \dots N)} = {coeff (0_{𝑝}) ↾}_{(0 \dots N)}) \to w = (0 \dots N) \times \{0\}$
369	368	ex	$⊢ {coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) ↾}_{(0 \dots N)} = w \to ({coeff ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})) ↾}_{(0 \dots N)} = {coeff (0_{𝑝}) ↾}_{(0 \dots N)} \to w = (0 \dots N) \times \{0\})$
370	357 359 369	syl2im	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) = 0_{𝑝} \to w = (0 \dots N) \times \{0\})$
371	370	necon3d	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to (w \neq (0 \dots N) \times \{0\} \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \neq 0_{𝑝})$
372	371	impr	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land w \neq (0 \dots N) \times \{0\})) \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \neq 0_{𝑝}$
373		eldifsn	$⊢ (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \in (Poly (ℚ) ∖ \{0_{𝑝}\}) \leftrightarrow ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \in Poly (ℚ) \land (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \neq 0_{𝑝})$
374	280 372 373	sylanbrc	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land w \neq (0 \dots N) \times \{0\})) \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \in (Poly (ℚ) ∖ \{0_{𝑝}\})$
375	374	adantrr	$⊢ (φ \land ((w : (0 \dots N) ⟶ ℚ \land w \neq (0 \dots N) \times \{0\}) \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \in (Poly (ℚ) ∖ \{0_{𝑝}\})$
376		oveq1	$⊢ y = A \to y^{k} = A^{k}$
377	376	oveq2d	$⊢ y = A \to w (k) y^{k} = w (k) A^{k}$
378	377	sumeq2sdv	$⊢ y = A \to \sum_{k = 0}^{N} w (k) y^{k} = \sum_{k = 0}^{N} w (k) A^{k}$
379		eqid	$⊢ (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) = (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k})$
380		sumex	$⊢ \sum_{k = 0}^{N} w (k) A^{k} \in V$
381	378 379 380	fvmpt	$⊢ A \in ℂ \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) (A) = \sum_{k = 0}^{N} w (k) A^{k}$
382	1 381	syl	$⊢ φ \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) (A) = \sum_{k = 0}^{N} w (k) A^{k}$
383	382	adantr	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) (A) = \sum_{k = 0}^{N} w (k) A^{k}$
384	109	adantll	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to w (k) \in ℂ$
385	3	adantlr	$⊢ ((φ \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to X \in ℂ$
386	112 385	mulcld	$⊢ ((φ \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to C X \in ℂ$
387	386	adantllr	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to C X \in ℂ$
388	53 384 387	fsummulc2	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to w (k) \sum_{n = 1}^{N} C X = \sum_{n = 1}^{N} w (k) C X$
389	5	oveq2d	$⊢ (φ \land k \in (0 \dots N)) \to w (k) A^{k} = w (k) \sum_{n = 1}^{N} C X$
390	389	adantlr	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to w (k) A^{k} = w (k) \sum_{n = 1}^{N} C X$
391	384	adantr	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to w (k) \in ℂ$
392	112	adantllr	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to C \in ℂ$
393		simpll	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to φ$
394	393 3	sylan	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to X \in ℂ$
395	391 392 394	mulassd	$⊢ (((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \land n \in (1 \dots N)) \to w (k) C X = w (k) C X$
396	395	sumeq2dv	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to \sum_{n = 1}^{N} w (k) C X = \sum_{n = 1}^{N} w (k) C X$
397	388 390 396	3eqtr4d	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land k \in (0 \dots N)) \to w (k) A^{k} = \sum_{n = 1}^{N} w (k) C X$
398	397	sumeq2dv	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to \sum_{k = 0}^{N} w (k) A^{k} = \sum_{k = 0}^{N} \sum_{n = 1}^{N} w (k) C X$
399	109	ad2ant2lr	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land (k \in (0 \dots N) \land n \in (1 \dots N))) \to w (k) \in ℂ$
400	112	anasss	$⊢ (φ \land (k \in (0 \dots N) \land n \in (1 \dots N))) \to C \in ℂ$
401	400	adantlr	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land (k \in (0 \dots N) \land n \in (1 \dots N))) \to C \in ℂ$
402	399 401	mulcld	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land (k \in (0 \dots N) \land n \in (1 \dots N))) \to w (k) C \in ℂ$
403	3	ad2ant2rl	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land (k \in (0 \dots N) \land n \in (1 \dots N))) \to X \in ℂ$
404	402 403	mulcld	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land (k \in (0 \dots N) \land n \in (1 \dots N))) \to w (k) C X \in ℂ$
405	45 71 404	fsumcom	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to \sum_{k = 0}^{N} \sum_{n = 1}^{N} w (k) C X = \sum_{n = 1}^{N} \sum_{k = 0}^{N} w (k) C X$
406	398 405	eqtrd	$⊢ (φ \land w : (0 \dots N) ⟶ ℚ) \to \sum_{k = 0}^{N} w (k) A^{k} = \sum_{n = 1}^{N} \sum_{k = 0}^{N} w (k) C X$
407	406	adantrr	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to \sum_{k = 0}^{N} w (k) A^{k} = \sum_{n = 1}^{N} \sum_{k = 0}^{N} w (k) C X$
408		nfv	$⊢ Ⅎ n φ$
409		nfv	$⊢ Ⅎ n w : (0 \dots N) ⟶ ℚ$
410		nfra1	$⊢ Ⅎ n \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0$
411	409 410	nfan	$⊢ Ⅎ n (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)$
412	408 411	nfan	$⊢ Ⅎ n (φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0))$
413		rspa	$⊢ (\forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \land n \in (1 \dots N)) \to \sum_{k = 0}^{N} w (k) C = 0$
414	413	oveq1d	$⊢ (\forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0 \land n \in (1 \dots N)) \to \sum_{k = 0}^{N} w (k) C X = 0 \cdot X$
415	414	adantll	$⊢ ((w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0) \land n \in (1 \dots N)) \to \sum_{k = 0}^{N} w (k) C X = 0 \cdot X$
416	415	adantll	$⊢ ((φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \land n \in (1 \dots N)) \to \sum_{k = 0}^{N} w (k) C X = 0 \cdot X$
417	3	adantlr	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to X \in ℂ$
418	94 417 115	fsummulc1	$⊢ ((φ \land w : (0 \dots N) ⟶ ℚ) \land n \in (1 \dots N)) \to \sum_{k = 0}^{N} w (k) C X = \sum_{k = 0}^{N} w (k) C X$
419	418	adantlrr	$⊢ ((φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \land n \in (1 \dots N)) \to \sum_{k = 0}^{N} w (k) C X = \sum_{k = 0}^{N} w (k) C X$
420	3	mul02d	$⊢ (φ \land n \in (1 \dots N)) \to 0 \cdot X = 0$
421	420	adantlr	$⊢ ((φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \land n \in (1 \dots N)) \to 0 \cdot X = 0$
422	416 419 421	3eqtr3d	$⊢ ((φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \land n \in (1 \dots N)) \to \sum_{k = 0}^{N} w (k) C X = 0$
423	422	ex	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to (n \in (1 \dots N) \to \sum_{k = 0}^{N} w (k) C X = 0)$
424	412 423	ralrimi	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C X = 0$
425	424	sumeq2d	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to \sum_{n = 1}^{N} \sum_{k = 0}^{N} w (k) C X = \sum_{n = 1}^{N} 0$
426	407 425	eqtrd	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to \sum_{k = 0}^{N} w (k) A^{k} = \sum_{n = 1}^{N} 0$
427	24	olci	$⊢ ((1 \dots N) \subseteq ℤ_{\geq B} \lor (1 \dots N) \in Fin)$
428		sumz	$⊢ ((1 \dots N) \subseteq ℤ_{\geq B} \lor (1 \dots N) \in Fin) \to \sum_{n = 1}^{N} 0 = 0$
429	427 428	ax-mp	$⊢ \sum_{n = 1}^{N} 0 = 0$
430	426 429	eqtrdi	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to \sum_{k = 0}^{N} w (k) A^{k} = 0$
431	383 430	eqtrd	$⊢ (φ \land (w : (0 \dots N) ⟶ ℚ \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) (A) = 0$
432	431	adantrlr	$⊢ (φ \land ((w : (0 \dots N) ⟶ ℚ \land w \neq (0 \dots N) \times \{0\}) \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) (A) = 0$
433		fveq1	$⊢ x = (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \to x (A) = (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) (A)$
434	433	eqeq1d	$⊢ x = (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \to (x (A) = 0 \leftrightarrow (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) (A) = 0)$
435	434	rspcev	$⊢ ((y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) \in (Poly (ℚ) ∖ \{0_{𝑝}\}) \land (y \in ℂ ⟼ \sum_{k = 0}^{N} w (k) y^{k}) (A) = 0) \to \exists x \in (Poly (ℚ) ∖ \{0_{𝑝}\}) x (A) = 0$
436	375 432 435	syl2anc	$⊢ (φ \land ((w : (0 \dots N) ⟶ ℚ \land w \neq (0 \dots N) \times \{0\}) \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to \exists x \in (Poly (ℚ) ∖ \{0_{𝑝}\}) x (A) = 0$
437	276 436	sylanr1	$⊢ (φ \land (w \in ((ℚ^{(0 \dots N)}) ∖ \{(0 \dots N) \times \{0\}\}) \land \forall n \in (1 \dots N) \sum_{k = 0}^{N} w (k) C = 0)) \to \exists x \in (Poly (ℚ) ∖ \{0_{𝑝}\}) x (A) = 0$
438	273 437	rexlimddv	$⊢ φ \to \exists x \in (Poly (ℚ) ∖ \{0_{𝑝}\}) x (A) = 0$
439		elqaa	$⊢ A \in 𝔸 \leftrightarrow (A \in ℂ \land \exists x \in (Poly (ℚ) ∖ \{0_{𝑝}\}) x (A) = 0)$
440	1 438 439	sylanbrc	$⊢ φ \to A \in 𝔸$

Metamath Proof Explorer

Theorem aacllem

Proof