Theorem aacllem 51219

Description: Lemma for other theorems about 𝔸. (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	⊢ (𝜑 → 𝐴 ∈ ℂ)
aacllem.1	⊢ (𝜑 → 𝑁 ∈ ℕ0)
aacllem.2	⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
aacllem.3	⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
aacllem.4	⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))

Assertion

Ref	Expression
aacllem	⊢ (𝜑 → 𝐴 ∈ 𝔸)

Distinct variable groups:   𝐴,𝑘,𝑛   𝑘,𝑁,𝑛   𝑘,𝑋   𝜑,𝑘,𝑛

Allowed substitution hints:   𝐶(𝑘, 𝑛)   𝑋(𝑛)

Proof of Theorem aacllem

Dummy variables 𝑤 𝑥 𝑦 𝐵 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		aacllem.0	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		aacllem.1	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
3	2	nn0red 12695	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
4	3	ltp1d 12274	. . . . 5 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
5		peano2nn0 12673	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
6	2, 5	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ0)
7	6	nn0red 12695	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
8	3, 7	ltnled 11484	. . . . 5 ⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁))
9	4, 8	mpbid 235	. . . 4 ⊢ (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁)
10		aacllem.3	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
11	10	3expa 1136	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
12	11	fmpttd 7139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
13		qex 13115	. . . . . . . . . . 11 ⊢ ℚ ∈ V
14		ovex 7476	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ V
15	13, 14	elmap 8927	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
16	12, 15	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)))
17	16	fmpttd 7139	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁)))
18		eqid 2763	. . . . . . . . . . . 12 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ)
19	18	qdrng 27977	. . . . . . . . . . 11 ⊢ (ℂfld ↾s ℚ) ∈ DivRing
20		drngring 21017	. . . . . . . . . . 11 ⊢ ((ℂfld ↾s ℚ) ∈ DivRing → (ℂfld ↾s ℚ) ∈ Ring)
21	19, 20	ax-mp 5	. . . . . . . . . 10 ⊢ (ℂfld ↾s ℚ) ∈ Ring
22		fzfi 14142	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
23		eqid 2763	. . . . . . . . . . 11 ⊢ ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) = ((ℂfld ↾s ℚ) freeLMod (1...𝑁))
24	23	frlmlmod 22085	. . . . . . . . . 10 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod)
25	21, 22, 24	mp2an 705	. . . . . . . . 9 ⊢ ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod
26		fzfi 14142	. . . . . . . . 9 ⊢ (0...𝑁) ∈ Fin
27	18	qrngbas 27976	. . . . . . . . . . . 12 ⊢ ℚ = (Base‘(ℂfld ↾s ℚ))
28	23, 27	frlmfibas 22098	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℚ ↑m (1...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
29	19, 22, 28	mp2an 705	. . . . . . . . . 10 ⊢ (ℚ ↑m (1...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
30	23	frlmsca 22089	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℂfld ↾s ℚ) = (Scalar‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
31	19, 22, 30	mp2an 705	. . . . . . . . . 10 ⊢ (ℂfld ↾s ℚ) = (Scalar‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
32		eqid 2763	. . . . . . . . . 10 ⊢ ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
33	18	qrng0 27978	. . . . . . . . . . . 12 ⊢ 0 = (0g‘(ℂfld ↾s ℚ))
34	23, 33	frlm0 22090	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) × {0}) = (0g‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
35	21, 22, 34	mp2an 705	. . . . . . . . . 10 ⊢ ((1...𝑁) × {0}) = (0g‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
36		eqid 2763	. . . . . . . . . . . 12 ⊢ ((ℂfld ↾s ℚ) freeLMod (0...𝑁)) = ((ℂfld ↾s ℚ) freeLMod (0...𝑁))
37	36, 27	frlmfibas 22098	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ DivRing ∧ (0...𝑁) ∈ Fin) → (ℚ ↑m (0...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (0...𝑁))))
38	19, 26, 37	mp2an 705	. . . . . . . . . 10 ⊢ (ℚ ↑m (0...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (0...𝑁)))
39	29, 31, 32, 35, 33, 38	islindf4 22174	. . . . . . . . 9 ⊢ ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (0...𝑁) ∈ Fin ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
40	25, 26, 39	mp3an12 1481	. . . . . . . 8 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
41	17, 40	syl 18	. . . . . . 7 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
42		elmapi 8897	. . . . . . . . 9 ⊢ (𝑤 ∈ (ℚ ↑m (0...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
43		fzfid 14143	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (0...𝑁) ∈ Fin)
44		fvexd 6923	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ V)
45	14	mptex 7252	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V
46	45	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V)
47		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤:(0...𝑁)⟶ℚ)
48	47	feqmptd 6976	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤 = (𝑘 ∈ (0...𝑁) ↦ (𝑤‘𝑘)))
49		eqidd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
50	43, 44, 46, 48, 49	offval2 7737	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))))
51		fzfid 14143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
52		ffvelcdm 7105	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
53	52	adantll 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
54	16	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)))
55		cnfldmul 21716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ · = (.r‘ℂfld)
56	18, 55	ressmulr 17507	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℚ ∈ V → · = (.r‘(ℂfld ↾s ℚ)))
57	13, 56	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ · = (.r‘(ℂfld ↾s ℚ))
58	23, 29, 27, 51, 53, 54, 32, 57	frlmvscafval 22102	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (((1...𝑁) × {(𝑤‘𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
59		fvexd 6923	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ V)
60	11	adantllr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
61		fconstmpt 5717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘))
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘)))
63		eqidd 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶))
64	51, 59, 60, 62, 63	offval2 7737	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (((1...𝑁) × {(𝑤‘𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
65	58, 64	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
66	65	mpteq2dva 5201	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
67	50, 66	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
68	67	oveq2d 7459	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))))
69		fzfid 14143	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (1...𝑁) ∈ Fin)
70	21	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (ℂfld ↾s ℚ) ∈ Ring)
71	53	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
72	11	an32s 665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
73	72	adantllr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
74		qmulcl 13122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤‘𝑘) ∈ ℚ ∧ 𝐶 ∈ ℚ) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
75	71, 73, 74	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
76	75	an32s 665	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
77	76	fmpttd 7139	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
78	13, 14	elmap 8927	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
79	77, 78	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)))
80		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
81	14	mptex 7252	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V)
83		snex 5401	. . . . . . . . . . . . . . . . . . 19 ⊢ {0} ∈ V
84	14, 83	xpex 7791	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) × {0}) ∈ V
85	84	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((1...𝑁) × {0}) ∈ V)
86	80, 43, 82, 85	fsuppmptdm 9395	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) finSupp ((1...𝑁) × {0}))
87	23, 29, 35, 69, 43, 70, 79, 86	frlmgsum 22108	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))))
88		cnfldbas 21712	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ = (Base‘ℂfld)
89		cnfldadd 21714	. . . . . . . . . . . . . . . . . 18 ⊢ + = (+g‘ℂfld)
90		cnfldex 21711	. . . . . . . . . . . . . . . . . . 19 ⊢ ℂfld ∈ V
91	90	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℂfld ∈ V)
92		fzfid 14143	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (0...𝑁) ∈ Fin)
93		qsscn 13114	. . . . . . . . . . . . . . . . . . 19 ⊢ ℚ ⊆ ℂ
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℚ ⊆ ℂ)
95	75	fmpttd 7139	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(0...𝑁)⟶ℚ)
96		0z 12731	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℤ
97		zq 13108	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℤ → 0 ∈ ℚ)
98	96, 97	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℚ
99	98	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 0 ∈ ℚ)
100		addlid 11520	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℂ → (0 + 𝑥) = 𝑥)
101		addrid 11517	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℂ → (𝑥 + 0) = 𝑥)
102	100, 101	jca 521	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
103	102	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ ℂ) → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
104	88, 89, 18, 91, 92, 94, 95, 99, 103	gsumress 18900	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
105		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
106		qcn 13117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤‘𝑘) ∈ ℚ → (𝑤‘𝑘) ∈ ℂ)
107	52, 106	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
108	105, 107	sylan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
109		qcn 13117	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 ∈ ℚ → 𝐶 ∈ ℂ)
110	11, 109	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
111	110	an32s 665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
112	111	adantllr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
113	108, 112	mulcld 11356	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ)
114	92, 113	gsumfsum 21770	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
115	104, 114	eqtr3d 2800	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
116	115	mpteq2dva 5201	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)))
117	68, 87, 116	3eqtrd 2802	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)))
118		qaddcl 13120	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 + 𝑦) ∈ ℚ)
119	118	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) ∈ ℚ)
120	94, 119, 92, 75, 99	fsumcllem 15927	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ ℚ)
121	120	fmpttd 7139	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
122	13, 14	elmap 8927	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
123	121, 122	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)))
124	117, 123	eqeltrd 2864	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑m (1...𝑁)))
125		elmapi 8897	. . . . . . . . . . . . 13 ⊢ ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑m (1...𝑁)) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ)
126		ffn 6731	. . . . . . . . . . . . 13 ⊢ ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
127	124, 125, 126	3syl 19	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
128		c0ex 11327	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
129		fnconstg 6792	. . . . . . . . . . . . 13 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
130	128, 129	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((1...𝑁) × {0}) Fn (1...𝑁)
131		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛((ℂfld ↾s ℚ) freeLMod (1...𝑁))
132		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛 Σg
133		nfcv 2926	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛𝑤
134		nfcv 2926	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
135		nfcv 2926	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛(0...𝑁)
136		nfmpt1 5207	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐶)
137	135, 136	nfmpt 5206	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
138	133, 134, 137	nfov 7473	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
139	131, 132, 138	nfov 7473	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))
140		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛((1...𝑁) × {0})
141	139, 140	eqfnfv2f 7056	. . . . . . . . . . . 12 ⊢ (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
142	127, 130, 141	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
143	117	fveq1d 6910	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛))
144		sumex 15884	. . . . . . . . . . . . . . 15 ⊢ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V
145		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
146	145	fvmpt2 7028	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ∧ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
147	144, 146	mpan2 704	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
148	143, 147	sylan9eq 2818	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
149	128	fvconst2 7233	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
150	149	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
151	148, 150	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
152	151	ralbidva 3187	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (∀𝑛 ∈ (1...𝑁)((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
153	142, 152	bitrd 282	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
154	153	imbi1d 344	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
155	42, 154	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ℚ ↑m (0...𝑁))) → (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
156	155	ralbidva 3187	. . . . . . 7 ⊢ (𝜑 → (∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
157	41, 156	bitrd 282	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
158		drngnzr 21032	. . . . . . . . 9 ⊢ ((ℂfld ↾s ℚ) ∈ DivRing → (ℂfld ↾s ℚ) ∈ NzRing)
159	19, 158	ax-mp 5	. . . . . . . 8 ⊢ (ℂfld ↾s ℚ) ∈ NzRing
160	31	islindf3 22162	. . . . . . . 8 ⊢ ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂfld ↾s ℚ) ∈ NzRing) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))⟶1-1V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))))
161	25, 159, 160	mp2an 705	. . . . . . 7 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))⟶1-1V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
162		eqid 2763	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
163	45, 162	dmmpti 6705	. . . . . . . . 9 ⊢ dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁)
164		f1eq2 6796	. . . . . . . . 9 ⊢ (dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))⟶1-1V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V))
165	163, 164	ax-mp 5	. . . . . . . 8 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))⟶1-1V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V)
166	165	anbi1i 636	. . . . . . 7 ⊢ (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))⟶1-1V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
167	161, 166	bitri 278	. . . . . 6 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
168		con34b 319	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
169		df-nel 3066	. . . . . . . . . . 11 ⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 ∈ {((0...𝑁) × {0})})
170		velsn 4600	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {((0...𝑁) × {0})} ↔ 𝑤 = ((0...𝑁) × {0}))
171	169, 170	xchbinx 337	. . . . . . . . . 10 ⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 = ((0...𝑁) × {0}))
172	171	imbi1i 352	. . . . . . . . 9 ⊢ ((𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
173	168, 172	bitr4i 281	. . . . . . . 8 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
174	173	ralbii 3112	. . . . . . 7 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
175		raldifb 4088	. . . . . . 7 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ ∀𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
176		ralnex 3092	. . . . . . 7 ⊢ (∀𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
177	174, 175, 176	3bitri 300	. . . . . 6 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
178	157, 167, 177	3bitr3g 316	. . . . 5 ⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
179		eqid 2763	. . . . . . . . . . . . 13 ⊢ (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
180	29, 179	lssmre 21271	. . . . . . . . . . . 12 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod → (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁))))
181	25, 180	ax-mp 5	. . . . . . . . . . 11 ⊢ (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁)))
182	181	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁))))
183		eqid 2763	. . . . . . . . . . . 12 ⊢ (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
184		eqid 2763	. . . . . . . . . . . 12 ⊢ (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) = (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
185	179, 183, 184	mrclsp 21294	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod → (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
186	25, 185	ax-mp 5	. . . . . . . . . 10 ⊢ (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
187		eqid 2763	. . . . . . . . . 10 ⊢ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) = (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
188	31	islvec 21409	. . . . . . . . . . . . 13 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec ↔ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂfld ↾s ℚ) ∈ DivRing))
189	25, 19, 188	mpbir2an 724	. . . . . . . . . . . 12 ⊢ ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec
190	179, 186, 29	lssacsex 21452	. . . . . . . . . . . . 13 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec → ((LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∈ (ACS‘(ℚ ↑m (1...𝑁))) ∧ ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))))
191	190	simprd 501	. . . . . . . . . . . 12 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec → ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))
192	189, 191	ax-mp 5	. . . . . . . . . . 11 ⊢ ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))
193	192	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))
194	17	frnd 6740	. . . . . . . . . . . 12 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑m (1...𝑁)))
195		dif0 4330	. . . . . . . . . . . 12 ⊢ ((ℚ ↑m (1...𝑁)) ∖ ∅) = (ℚ ↑m (1...𝑁))
196	194, 195	sseqtrrdi 3954	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
197	196	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
198		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)) = ((ℂfld ↾s ℚ) unitVec (1...𝑁))
199	198, 23, 29	uvcff 22127	. . . . . . . . . . . . . 14 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁)))
200	21, 22, 199	mp2an 705	. . . . . . . . . . . . 13 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁))
201		frn 6739	. . . . . . . . . . . . 13 ⊢ (((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁)) → ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ (ℚ ↑m (1...𝑁)))
202	200, 201	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ (ℚ ↑m (1...𝑁))
203	202, 195	sseqtrri 3962	. . . . . . . . . . 11 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅)
204	203	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
205		un0 4347	. . . . . . . . . . . . . 14 ⊢ (ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅) = ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))
206	205	fveq2i 6911	. . . . . . . . . . . . 13 ⊢ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) = ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
207		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
208	23, 198, 207	frlmlbs 22133	. . . . . . . . . . . . . . 15 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
209	21, 22, 208	mp2an 705	. . . . . . . . . . . . . 14 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
210	29, 207, 183	lbssp 21384	. . . . . . . . . . . . . 14 ⊢ (ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) = (ℚ ↑m (1...𝑁)))
211	209, 210	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) = (ℚ ↑m (1...𝑁))
212	206, 211	eqtri 2786	. . . . . . . . . . . 12 ⊢ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) = (ℚ ↑m (1...𝑁))
213	194, 212	sseqtrrdi 3954	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)))
214	213	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)))
215		un0 4347	. . . . . . . . . . 11 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) = ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
216	25, 159	pm3.2i 476	. . . . . . . . . . . . . 14 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂfld ↾s ℚ) ∈ NzRing)
217	183, 31	lindsind2 22155	. . . . . . . . . . . . . 14 ⊢ (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂfld ↾s ℚ) ∈ NzRing) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
218	216, 217	mp3an1 1478	. . . . . . . . . . . . 13 ⊢ ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
219	218	ralrimiva 3158	. . . . . . . . . . . 12 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
220	186, 187	ismri2 17835	. . . . . . . . . . . . . 14 ⊢ (((LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁))) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑m (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
221	181, 194, 220	sylancr 599	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
222	221	biimpar 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
223	219, 222	sylan2 605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
224	215, 223	eqeltrid 2868	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
225		mptfi 9368	. . . . . . . . . . . . 13 ⊢ ((0...𝑁) ∈ Fin → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
226		rnfi 9357	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
227	26, 225, 226	mp2b 10	. . . . . . . . . . . 12 ⊢ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin
228	227	orci 879	. . . . . . . . . . 11 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ Fin)
229	228	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ Fin))
230	182, 186, 187, 193, 197, 204, 214, 224, 229	mreexexd 17851	. . . . . . . . 9 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ∃𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))))
231	230	ex 418	. . . . . . . 8 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ∃𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))))
232		ovex 7476	. . . . . . . . . . . . 13 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V
233	232	rnex 7946	. . . . . . . . . . . 12 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V
234		elpwi 4567	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ⊆ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
235		ssdomg 9055	. . . . . . . . . . . 12 ⊢ (ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V → (𝑣 ⊆ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))))
236	233, 234, 235	mpsyl 69	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
237		endomtr 9067	. . . . . . . . . . . . . 14 ⊢ ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
238	237	ancoms 464	. . . . . . . . . . . . 13 ⊢ ((𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
239		f1f1orn 6858	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1ontoran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
240		ovex 7476	. . . . . . . . . . . . . . . . 17 ⊢ (0...𝑁) ∈ V
241	240	f1oen 9027	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1ontoran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
242	239, 241	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
243		endomtr 9067	. . . . . . . . . . . . . . . . 17 ⊢ (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
244	198	uvcendim 22183	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℂfld ↾s ℚ) ∈ NzRing ∧ (1...𝑁) ∈ Fin) → (1...𝑁) ≈ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
245	159, 22, 244	mp2an 705	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ≈ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))
246	245	ensymi 9059	. . . . . . . . . . . . . . . . . 18 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)
247		domentr 9068	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (0...𝑁) ≼ (1...𝑁))
248		hashdom 14550	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁)))
249	26, 22, 248	mp2an 705	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁))
250		hashfz0 14604	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ0 → (♯‘(0...𝑁)) = (𝑁 + 1))
251	2, 250	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1))
252		hashfz1 14517	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
253	2, 252	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
254	251, 253	breq12d 5119	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (𝑁 + 1) ≤ 𝑁))
255	249, 254	bitr3id 288	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0...𝑁) ≼ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
256	247, 255	imbitrid 247	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
257	246, 256	mpan2i 710	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
258	243, 257	syl5 35	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (𝑁 + 1) ≤ 𝑁))
259	258	expd 421	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
260	242, 259	syl5 35	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
261	260	com23 87	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V → (𝑁 + 1) ≤ 𝑁)))
262	238, 261	syl5 35	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V → (𝑁 + 1) ≤ 𝑁)))
263	262	expdimp 458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V → (𝑁 + 1) ≤ 𝑁)))
264	236, 263	sylan2 605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V → (𝑁 + 1) ≤ 𝑁)))
265	264	adantrd 497	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V → (𝑁 + 1) ≤ 𝑁)))
266	265	rexlimdva 3167	. . . . . . . 8 ⊢ (𝜑 → (∃𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V → (𝑁 + 1) ≤ 𝑁)))
267	231, 266	syld 48	. . . . . . 7 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V → (𝑁 + 1) ≤ 𝑁)))
268	267	impd 416	. . . . . 6 ⊢ (𝜑 → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V) → (𝑁 + 1) ≤ 𝑁))
269	268	ancomsd 471	. . . . 5 ⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶1-1V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (𝑁 + 1) ≤ 𝑁))
270	178, 269	sylbird 263	. . . 4 ⊢ (𝜑 → (¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → (𝑁 + 1) ≤ 𝑁))
271	9, 270	mt3d 149	. . 3 ⊢ (𝜑 → ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
272		eldifsn 4748	. . . . 5 ⊢ (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ↔ (𝑤 ∈ (ℚ ↑m (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})))
273	42	anim1i 627	. . . . 5 ⊢ ((𝑤 ∈ (ℚ ↑m (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
274	272, 273	sylbi 220	. . . 4 ⊢ (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
275	93	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ℚ ⊆ ℂ)
276	2	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑁 ∈ ℕ0)
277	275, 276, 53	elplyd 26550	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ))
278	277	adantrr 730	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ))
279		uzdisj 13758	. . . . . . . . . . . . . . . . . 18 ⊢ ((0...((𝑁 + 1) − 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ∅
280	2	nn0cnd 12696	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℂ)
281		pncan1 11767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
282	280, 281	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
283	282	oveq2d 7459	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
284	283	ineq1d 4119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))
285	279, 284	eqtr3id 2812	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ = ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))
286	285	eqcomd 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅)
287	128	fconst 6790	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0}
288		snssi 4746	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℚ → {0} ⊆ ℚ)
289	96, 97, 288	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ {0} ⊆ ℚ
290	289, 93	sstri 3922	. . . . . . . . . . . . . . . . . 18 ⊢ {0} ⊆ ℂ
291		fss 6748	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℂ) → ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ)
292	287, 290, 291	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ
293		fun 6766	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
294	292, 293	mpanl2 714	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
295	286, 294	sylan2 605	. . . . . . . . . . . . . . 15 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
296	295	ancoms 464	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
297		nn0uz 13030	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 = (ℤ≥‘0)
298	6, 297	eleqtrdi 2874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ≥‘0))
299		uzsplit 13757	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘0) → (ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
300	298, 299	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
301	297, 300	eqtrid 2810	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℕ0 = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
302	283	uneq1d 4169	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))))
303	301, 302	eqtr2d 2799	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))) = ℕ0)
304		ssequn1 4187	. . . . . . . . . . . . . . . . . 18 ⊢ (ℚ ⊆ ℂ ↔ (ℚ ∪ ℂ) = ℂ)
305	93, 304	mpbi 233	. . . . . . . . . . . . . . . . 17 ⊢ (ℚ ∪ ℂ) = ℂ
306	305	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℚ ∪ ℂ) = ℂ)
307	303, 306	feq23d 6726	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ))
308	307	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ))
309	296, 308	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ)
310		ffn 6731	. . . . . . . . . . . . . . . 16 ⊢ (𝑤:(0...𝑁)⟶ℚ → 𝑤 Fn (0...𝑁))
311		fnimadisj 6693	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 “ (ℤ≥‘(𝑁 + 1))) = ∅)
312	310, 286, 311	syl2anr 609	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 “ (ℤ≥‘(𝑁 + 1))) = ∅)
313	2	nn0zd 12745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℤ)
314	313	peano2zd 12833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
315		uzid 13007	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ ℤ → (𝑁 + 1) ∈ (ℤ≥‘(𝑁 + 1)))
316		ne0i 4290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘(𝑁 + 1)) → (ℤ≥‘(𝑁 + 1)) ≠ ∅)
317	314, 315, 316	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ≥‘(𝑁 + 1)) ≠ ∅)
318		inidm 4126	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) = (ℤ≥‘(𝑁 + 1))
319	318	neeq1i 3023	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) ≠ ∅ ↔ (ℤ≥‘(𝑁 + 1)) ≠ ∅)
320	317, 319	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) ≠ ∅)
321		xpima2 6188	. . . . . . . . . . . . . . . . 17 ⊢ (((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) ≠ ∅ → (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))) = {0})
322	320, 321	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))) = {0})
323	322	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))) = {0})
324	312, 323	uneq12d 4171	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 “ (ℤ≥‘(𝑁 + 1))) ∪ (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1)))) = (∅ ∪ {0}))
325		imaundir 6154	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) “ (ℤ≥‘(𝑁 + 1))) = ((𝑤 “ (ℤ≥‘(𝑁 + 1))) ∪ (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))))
326		uncom 4160	. . . . . . . . . . . . . . 15 ⊢ (∅ ∪ {0}) = ({0} ∪ ∅)
327		un0 4347	. . . . . . . . . . . . . . 15 ⊢ ({0} ∪ ∅) = {0}
328	326, 327	eqtr2i 2787	. . . . . . . . . . . . . 14 ⊢ {0} = (∅ ∪ {0})
329	324, 325, 328	3eqtr4g 2823	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) “ (ℤ≥‘(𝑁 + 1))) = {0})
330	286, 310	anim12ci 626	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅))
331		fnconstg 6792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1)))
332	128, 331	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1))
333		fvun1 6999	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 Fn (0...𝑁) ∧ ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1)) ∧ (((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
334	332, 333	mp3an2 1479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
335	334	anassrs 473	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
336	330, 335	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
337	336	eqcomd 2769	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘))
338	337	oveq1d 7458	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝑦↑𝑘)) = (((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))
339	338	sumeq2dv 15898	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))
340	339	mpteq2dv 5202	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘))))
341	277, 276, 309, 329, 340	coeeq 26576	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})))
342	341	reseq1d 5980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)))
343		res0 5985	. . . . . . . . . . . . . 14 ⊢ (𝑤 ↾ ∅) = ∅
344	285	reseq2d 5981	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ↾ ∅) = (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
345		res0 5985	. . . . . . . . . . . . . . 15 ⊢ (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) = ∅
346	285	reseq2d 5981	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
347	345, 346	eqtr3id 2812	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∅ = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
348	343, 344, 347	3eqtr3a 2822	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
349		fss 6748	. . . . . . . . . . . . . . 15 ⊢ ((((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℚ) → ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ)
350	287, 289, 349	mp2an 705	. . . . . . . . . . . . . 14 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ
351		fresaunres1 6777	. . . . . . . . . . . . . 14 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
352	350, 351	mp3an2 1479	. . . . . . . . . . . . 13 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
353	348, 352	sylan2 605	. . . . . . . . . . . 12 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
354	353	ancoms 464	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
355	342, 354	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤)
356		fveq2 6908	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (coeff‘0𝑝))
357	356	reseq1d 5980	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)))
358		eqtr2 2784	. . . . . . . . . . . 12 ⊢ ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((coeff‘0𝑝) ↾ (0...𝑁)))
359		coe0 26605	. . . . . . . . . . . . . 14 ⊢ (coeff‘0𝑝) = (ℕ0 × {0})
360	359	reseq1i 5977	. . . . . . . . . . . . 13 ⊢ ((coeff‘0𝑝) ↾ (0...𝑁)) = ((ℕ0 × {0}) ↾ (0...𝑁))
361		elfznn0 13781	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ0)
362	361	ssriv 3917	. . . . . . . . . . . . . 14 ⊢ (0...𝑁) ⊆ ℕ0
363		xpssres 6019	. . . . . . . . . . . . . 14 ⊢ ((0...𝑁) ⊆ ℕ0 → ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0}))
364	362, 363	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0})
365	360, 364	eqtri 2786	. . . . . . . . . . . 12 ⊢ ((coeff‘0𝑝) ↾ (0...𝑁)) = ((0...𝑁) × {0})
366	358, 365	eqtrdi 2814	. . . . . . . . . . 11 ⊢ ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((0...𝑁) × {0}))
367	366	ex 418	. . . . . . . . . 10 ⊢ (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 → (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)) → 𝑤 = ((0...𝑁) × {0})))
368	355, 357, 367	syl2im 41	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → 𝑤 = ((0...𝑁) × {0})))
369	368	necon3d 2980	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ≠ ((0...𝑁) × {0}) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝))
370	369	impr 460	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝)
371		eldifsn 4748	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}) ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ) ∧ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝))
372	278, 370, 371	sylanbrc 595	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}))
373	372	adantrr 730	. . . . 5 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}))
374		oveq1 7450	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐴 → (𝑦↑𝑘) = (𝐴↑𝑘))
375	374	oveq2d 7459	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐴 → ((𝑤‘𝑘) · (𝑦↑𝑘)) = ((𝑤‘𝑘) · (𝐴↑𝑘)))
376	375	sumeq2sdv 15899	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
377		eqid 2763	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))
378		sumex 15884	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) ∈ V
379	376, 377, 378	fvmpt 7016	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
380	1, 379	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
381	380	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
382	107	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
383		aacllem.2	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
384	383	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
385	110, 384	mulcld 11356	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
386	385	adantllr 732	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
387	51, 382, 386	fsummulc2 15979	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋)))
388		aacllem.4	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))
389	388	oveq2d 7459	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
390	389	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
391	382	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
392	110	adantllr 732	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
393		simpll 779	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → 𝜑)
394	393, 383	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
395	391, 392, 394	mulassd 11359	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑤‘𝑘) · 𝐶) · 𝑋) = ((𝑤‘𝑘) · (𝐶 · 𝑋)))
396	395	sumeq2dv 15898	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋)))
397	387, 390, 396	3eqtr4d 2808	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
398	397	sumeq2dv 15898	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
399	107	ad2ant2lr 761	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (𝑤‘𝑘) ∈ ℂ)
400	110	anasss 472	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
401	400	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
402	399, 401	mulcld 11356	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ)
403	383	ad2ant2rl 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝑋 ∈ ℂ)
404	402, 403	mulcld 11356	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (((𝑤‘𝑘) · 𝐶) · 𝑋) ∈ ℂ)
405	43, 69, 404	fsumcom 15970	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
406	398, 405	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
407	406	adantrr 730	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
408		nfv 1949	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝜑
409		nfv 1949	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛 𝑤:(0...𝑁)⟶ℚ
410		nfra1 3290	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0
411	409, 410	nfan 1934	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
412	408, 411	nfan 1934	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
413		rspa 3255	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
414	413	oveq1d 7458	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
415	414	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
416	415	adantll 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
417	383	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
418	92, 417, 113	fsummulc1 15980	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
419	418	adantlrr 734	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
420	383	mul02d 11535	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
421	420	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
422	416, 419, 421	3eqtr3d 2806	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)
423	422	ex 418	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑛 ∈ (1...𝑁) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0))
424	412, 423	ralrimi 3264	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)
425	424	sumeq2d 15897	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)0)
426	407, 425	eqtrd 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)0)
427	22	olci 880	. . . . . . . . 9 ⊢ ((1...𝑁) ⊆ (ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin)
428		sumz 15917	. . . . . . . . 9 ⊢ (((1...𝑁) ⊆ (ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin) → Σ𝑛 ∈ (1...𝑁)0 = 0)
429	427, 428	ax-mp 5	. . . . . . . 8 ⊢ Σ𝑛 ∈ (1...𝑁)0 = 0
430	426, 429	eqtrdi 2814	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = 0)
431	381, 430	eqtrd 2798	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)
432	431	adantrlr 736	. . . . 5 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)
433		fveq1 6907	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → (𝑥‘𝐴) = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴))
434	433	eqeq1d 2765	. . . . . 6 ⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → ((𝑥‘𝐴) = 0 ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0))
435	434	rspcev 3580	. . . . 5 ⊢ (((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}) ∧ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
436	373, 432, 435	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
437	274, 436	sylanr1 695	. . 3 ⊢ ((𝜑 ∧ (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
438	271, 437	rexlimddv 3173	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
439		elqaa 26675	. 2 ⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0))
440	1, 438, 439	sylanbrc 595	1 ⊢ (𝜑 → 𝐴 ∈ 𝔸)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959   ∉ wnel 3065  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  𝒫 cpw 4560  {csn 4588   class class class wbr 5106   ↦ cmpt 5189   × cxp 5653  dom cdm 5655  ran crn 5656   ↾ cres 5657   “ cima 5658   Fn wfn 6553  ⟶wf 6554  ⟶1-1wf1 6555  ⟶1-1ontowf1o 6557  ‘cfv 6558  (class class class)co 7443   ∘_f cof 7715   ↑_m cmap 8875   ≈ cen 8998   ≼ cdom 8999  Fincfn 9001  ℂcc 11225  0cc0 11227  1c1 11228   + caddc 11230   · cmul 11232   < clt 11370   ≤ cle 11371   − cmin 11568  ℕ₀cn0 12633  ℤcz 12720  ℤ_≥cuz 12992  ℚcq 13102  ...cfz 13666  ↑cexp 14231  ♯chash 14501  Σcsu 15882  Basecbs 17416   ↾_s cress 17437  ._rcmulr 17458  Scalarcsca 17460   ·_𝑠 cvsca 17461  0_gc0g 17639   Σ_g cgsu 17640  Moorecmre 17781  mrClscmrc 17782  mrIndcmri 17783  ACScacs 17784  Ringcrg 20489  NzRingcnzr 20792  DivRingcdr 21010  LModclmod 21165  LSubSpclss 21236  LSpanclspn 21276  LBasisclbs 21379  LVecclvec 21407  ℂ_fldccnfld 21708   freeLMod cfrlm 22082   unitVec cuvc 22118   LIndF clindf 22140  LIndSclinds 22141  0_𝑝c0p 26020  Polycply 26532  coeffccoe 26534  𝔸caa 26667

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-inf2 9669  ax-cnex 11283  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304  ax-pre-sup 11305  ax-addf 11306  ax-mulf 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-isom 6567  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-of 7717  df-om 7902  df-1st 8025  df-2nd 8026  df-supp 8205  df-tpos 8271  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-1o 8504  df-2o 8505  df-oadd 8508  df-er 8745  df-map 8877  df-pm 8878  df-ixp 8954  df-en 9002  df-dom 9003  df-sdom 9004  df-fin 9005  df-fsupp 9382  df-sup 9461  df-inf 9462  df-oi 9531  df-card 10047  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-div 12001  df-nn 12363  df-2 12432  df-3 12433  df-4 12434  df-5 12435  df-6 12436  df-7 12437  df-8 12438  df-9 12439  df-n0 12634  df-xnn0 12707  df-z 12721  df-dec 12842  df-uz 12993  df-q 13103  df-rp 13148  df-fz 13667  df-fzo 13816  df-fl 13959  df-mod 14037  df-seq 14172  df-exp 14232  df-hash 14502  df-cj 15295  df-re 15296  df-im 15297  df-sqrt 15431  df-abs 15432  df-clim 15684  df-rlim 15685  df-sum 15883  df-struct 17354  df-sets 17371  df-slot 17389  df-ndx 17401  df-base 17417  df-ress 17438  df-plusg 17470  df-mulr 17471  df-starv 17472  df-sca 17473  df-vsca 17474  df-ip 17475  df-tset 17476  df-ple 17477  df-ds 17479  df-unif 17480  df-hom 17481  df-cco 17482  df-0g 17641  df-gsum 17642  df-prds 17647  df-pws 17649  df-mre 17785  df-mrc 17786  df-mri 17787  df-acs 17788  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-mhm 19007  df-submnd 19008  df-grp 19176  df-minusg 19177  df-sbg 19178  df-mulg 19307  df-subg 19362  df-ghm 19457  df-cntz 19561  df-cmn 20026  df-abl 20027  df-mgp 20391  df-rng 20405  df-ur 20438  df-ring 20491  df-cring 20492  df-oppr 20597  df-dvdsr 20617  df-unit 20618  df-invr 20648  df-dvr 20661  df-nzr 20793  df-subrng 20828  df-subrg 20852  df-drng 21012  df-lmod 21167  df-lss 21237  df-lsp 21277  df-lmhm 21327  df-lbs 21380  df-lvec 21408  df-sra 21478  df-rgmod 21479  df-cnfld 21709  df-dsmm 22068  df-frlm 22083  df-uvc 22119  df-lindf 22142  df-linds 22143  df-0p 26021  df-ply 26536  df-coe 26538  df-dgr 26539  df-aa 26668

This theorem is used by: (None)